-
Notifications
You must be signed in to change notification settings - Fork 14
09 Architecture Decisions
This chapter records the architecturally significant decisions that shape Prism. Each decision is documented as an Architecture Decision Record (ADR) following the Nygard format: title, status, context, decision, consequences. ADRs are appended in chronological order as decisions are taken; an ADR is never deleted, only superseded by a later ADR that links back to it.
Status: Accepted.
Context: The architecture being specified must be named, and its realization in code must be identified. Two distinct concerns exist: the abstract system (what is being specified) and its concrete realization (what code conforms to the specification).
Decision: The system specified by this wiki is named Prism. Prism is
realized by exactly three Rust crates: uor-foundation, prism, and
prism-verify. Throughout this wiki, the system is referred to as
Prism; the crates are referred to by their published crate names with no
prose abbreviation.
Consequences: The wiki specifies Prism as a system; conformance is determined against the wiki, not against any of the three crates' current source. The three crates collectively realize Prism; they are accountable to the wiki, not the reverse. Future Prism realizations in other crate decompositions or other languages are admissible if and only if they satisfy this wiki’s specification.
Status: Accepted.
Context: Prism has cross-boundary behavior involving the application author, the application user, and the Rust toolchain. The set of guarantees Prism makes at this boundary determines what conformance means.
Decision: Six properties hold normatively at every Prism boundary, enumerated in section 2 (Architecture Constraints) as TC-01 through TC-06: (TC-01) zero-cost runtime, (TC-02) sealing of certified types, (TC-03) singularity of the principal data path, (TC-04) UORassembly bilateral compile-time enforcement, (TC-05) replayability without deciders or hashing, and (TC-06) no application-author infrastructure. Section 3 (Cross-boundary Properties) collapses TC-02 and TC-03 into a single Sealing property when listing the architectural commitments per boundary, because path-singularity is what gives the seal architectural meaning; this restatement does not weaken either constraint.
Consequences: A conforming implementation MUST satisfy all six. Implementations that satisfy five of the six are not Prism implementations; the wiki does not admit partial conformance.
Status: Accepted.
Context: The application user, having received an output and a
Trace from the application author, must be able to verify the output.
Two architectures admit verification: server-mediated (the user calls a
centralized service that re-derives the certificate) and local (the user
runs verification code on their own hardware).
Decision: Verification is local. prism-verify is a Rust crate the
user (or a third party they trust) imports into their own crate; the
verifier executable runs on the user’s hardware. The verifier MUST NOT
invoke the author’s deciders and MUST NOT invoke any cryptographic hash
function — the content fingerprint is data carried by the trace.
Consequences: There is no centralized verification authority. The user’s verification depends on no service operated by the application author or by any third party. Verification has the same shape as execution: local, on the user’s device, at full hardware speed. A trade-off is that the user must compile or obtain a verification executable themselves; Prism is silent on how that executable reaches the user, by symmetry with how it is silent on how the application’s executable reaches them (ADR-004).
Rejected alternative: A hosted verification service operated by the framework or by application authors. Rejected because it introduces a centralized infrastructure dependency that violates the no-author-infrastructure constraint (TC-06) and creates a single point of failure for verification.
Status: Accepted.
Context: The application author’s executable must reach the application user. The mechanism by which it reaches them is a real concern in the system context.
Decision: The distribution channel is external to Prism. Prism does not specify, require, or interact with any distribution mechanism. The author and user agree on a distribution channel of their choosing — a release page, a package registry, a peer-to-peer network, a signed Git repository, removable media, or any other mechanism. The channel does not appear as an actor in the Level 1 system context (section 3); it is acknowledged in prose but is not in the C4 diagram, because Prism has no boundary flow with it.
Consequences: Prism is silent on distribution. Applications built on Prism may select any distribution mechanism that suits their domain, including decentralized mechanisms, without the architecture imposing a centralized requirement. The cost is that distribution security, integrity, and availability are concerns the application author solves through whatever mechanism they select; Prism contributes nothing to these concerns.
Rejected alternative: Specifying distribution as part of Prism (e.g., requiring signed releases, specifying a registry format, requiring a content-addressable distribution mechanism). Rejected because distribution is orthogonal to the system properties Prism specifies; including it would constrain applications without architectural benefit.
Status: Accepted.
Context: Prism has three architecturally distinct concerns. (a) UOR vocabulary: the substrate, the type-declaration vocabulary, the four UOR-domain sealed types, the wire-format type definitions, the mint primitives. (b) Prism runtime: the pipeline, the three Prism-mechanism sealed types, the operation-declaration vocabulary, the standard type library. (c) Replay surface: a thin façade re-exporting the relevant subset for verification consumers. The three concerns have distinct consumers: the substrate is consumed by both the runtime and the replay surface; the runtime is consumed by the application author; the replay surface is consumed by the application user. Combining any two would conflate substrate vocabulary with runtime mechanism, or runtime mechanism with verification surface, and force users of any single concern to depend on the others.
Decision: Prism is realized by exactly three Rust crates:
uor-foundation, prism, and prism-verify. uor-foundation is the
substrate; prism is the Prism runtime (pipeline + Prism-mechanism
seals + operation-declaration vocabulary + standard type library) closed
under uor-foundation's vocabulary; prism-verify is the replay
surface — a thin façade re-exporting prism's certify_from_trace and
Certified, and uor-foundation's wire-format types. Each consumer
depends on the minimal subset of Prism’s machinery it needs.
Consequences: The application user, who runs only verification,
depends on prism-verify and transitively on prism (for
certify_from_trace) and uor-foundation (for wire-format types), but
not on the rest of prism's pipeline runtime that the user never
invokes. The application author depends on prism (which re-exports
uor-foundation's vocabulary so the author imports only one crate) and
transitively on uor-foundation, but not on prism-verify (which they
do not invoke during execution). The split keeps each consumer’s
compile-time and runtime dependency graphs minimal and makes the
boundary between substrate and runtime explicit.
Rejected alternative: A single uor-foundation crate with feature
flags for runtime and verify functionality. Rejected because
feature-flagged crates produce one Cargo dependency that both author and
user must depend on, with the user’s verify feature pulling in
pipeline machinery the user never invokes. Cargo’s feature unification
across the workspace makes this brittle; separate crates make the
boundaries explicit and the dependency direction unambiguous.
Status: Accepted.
Context: The UORassembly contract specifies type-level constraints any Rust source compiling to a Prism executable must satisfy (constraint TC-04). Two architectural choices determine how the contract is enforced: where the enforcement happens (compile time vs runtime) and on which sides of which boundaries (unilateral vs bilateral).
Decision: UORassembly is enforced exclusively at compile time,
exclusively through the Rust type system, and bilaterally — meaning it
holds across both the boundary between uor-foundation and prism and
the boundary between prism and the application author’s crate. prism
declares trait bounds, sealed types, and type-level constraints; both
uor-foundation and the author’s crate MUST satisfy them. If either
does not, rustc rejects the source.
Consequences: There is no runtime UORassembly check. The produced
executable contains no validation code, no assertion machinery, no
type-tag inspection — these would all violate constraint TC-01’s
zero-cost runtime requirement. The bilateral enforcement prevents drift
on either side: uor-foundation cannot drift from what prism requires
(foundation-side check), and the application author’s code cannot drift
from what prism exposes (author-side check). The cost is that
prism's bounds are part of its public API; changing them changes what
conforming foundations and conforming author crates look like, and is
therefore an architecturally significant decision that requires its own
ADR.
Rejected alternative 1: Runtime enforcement via assertions or panics. Rejected because it violates TC-01.
Rejected alternative 2: Unilateral enforcement (prism checks
author’s crate only, uor-foundation is trusted). Rejected because it
admits foundation drift — a future uor-foundation version could
diverge from what prism requires without being detected at compile
time, breaking conforming applications silently.
Rejected alternative 3: External tooling (a cargo-integrated
linter or static analyzer that runs UORassembly checks separately).
Rejected because it depends on tooling beyond the Rust toolchain itself;
compilation would succeed for non-conforming code, with violations
caught only by a separately-invoked tool. The Rust type system provides
the necessary expressive power to encode the contract directly; external
tooling adds dependencies without adding correctness.
ADR-007 — Substitution axes are allocated across the three crates: foundation defines, prism bounds, author selects
Status: Accepted.
Context: Prism has three substitution axes: HostTypes (host data
representations), HostBounds (every capacity bound that varies along
the principal data path: fingerprint output width range, trace
event-count ceiling, the bit-width ceiling for algebraic levels, and any
further capacity carried by sealed values), Hasher (content-addressing
function). Each axis must be substitutable by the application author,
must not introduce runtime variation, and must be enforceable at compile
time. Where each axis’s contract is defined, where its bounds are
declared, and where its implementation is selected determines whether
these properties hold.
Decision: Each substitution axis is allocated across the three crates in a fixed three-position pattern:
-
uor-foundationdefines the trait that names the axis (HostTypes,HostBounds,Hasher). The trait specifies the contract any implementation MUST satisfy. -
prismdeclares the bound the trait MUST satisfy, expressed against the trait the foundation defined. The bound is whatuor-foundationMUST conform to and what the application author’s selection MUST satisfy. -
The application author’s crate selects the implementation, by passing a concrete type (e.g.,
DefaultHostTypes, or a custom type the author provides) intoprism's bounded surface. The selection is the only point at which variation actually occurs.
The third position generalizes per ADR-030: the original Hasher trait
becomes one axis among many declared via the axis! SDK macro, and the
substitution-axis triple’s third position becomes A: AxisTuple — a
tuple of axis trait selections each impl’d on AxisExtension. Hasher
itself is declared by the prism-crypto standard-library sub-crate (per
ADR-031) as HashAxis, with concrete impls (Sha256Hasher, Blake3Hasher,
etc.) provided by the same sub-crate. ADR-036 strengthens the
third-position bound from A: AxisTuple to A: AxisTuple + Hasher (the
canonical hash axis bound is carried through the tuple so resolver-bound
substrate operations parameterized by H: Hasher can consume the
model’s canonical hash axis type-associatedly via
<A as Hasher>::initial()). ADR-036 also introduces a fourth
model-declaration substrate parameter R: ResolverTuple (defaulting to
NullResolverTuple) that parallels AxisTuple structurally but carries
per-value content provision (resolver instances threaded as a value
reference) rather than per-domain operation kernels (axis methods
invoked type-associatedly). The architectural commitment is the
three-axis substitution structure plus the fourth substrate parameter;
the AxisTuple’s specific arity and member impls + the ResolverTuple’s
specific resolver selections are application-side choices at the model
declaration site.
Consequences: An implementation of any axis can be substituted only
by the author and only at the author’s compile time. The foundation
cannot vary on the author’s behalf; prism cannot vary on the author’s
behalf; both are fixed at the architecture’s level. The author’s
selection is bounded by prism's declared bounds; a selection that does
not satisfy the bounds is a compile error in the author’s crate. This
makes substitution rigid in the right way: variation is structural (the
axis as a whole), not parametric (no per-application customization
beyond axis selection). The three-position pattern (foundation defines,
prism bounds, author selects) is structurally parallel to the
three-layer algebraic closure (substrate / prism / implementation;
ADR-024) but not identical: the three positions concern who specifies
which axis-related artifact, while the three closures concern which
operator set is closed at which level. Both patterns coexist; the
closures inherit the axis-position pattern’s parametric scaling, but the
closure boundaries are operator-set-defined rather than
axis-position-defined.
Rejected alternative 1: Define the axes in prism rather than
uor-foundation. Rejected because the dependency direction would
invert: uor-foundation's UOR-domain types and wire-format types
reference these axes in their own type signatures; if the axes were in
prism, uor-foundation could not specify these types without
depending on prism, which would make uor-foundation no longer the
substrate. The substrate is what defines the axis traits; the runtime is
what binds them.
Rejected alternative 2: A single substitution axis (a "host" trait
combining all three concerns). Rejected because the three axes have
distinct contracts: HostTypes is about data representation,
HostBounds is about capacity, Hasher is about content addressing.
Combining them would force an author who needs to substitute one to also
re-implement the other two; keeping them separate keeps each
substitution point minimal.
Status: Accepted.
Context: The trace’s wire format is the byte-level representation that crosses the boundary between the application author’s executable and the application user. Cross-implementation interoperability for replay verification depends on the format being stable.
Decision: The trace wire format is specified normatively in section
8 (Cross-cutting Concepts, Trace Wire Format). The format includes: the
format_version field (must equal TRACE_REPLAY_FORMAT_VERSION), the
sequence of TraceEvent values with length-prefixed payloads, the
ContentFingerprint carried by the trace, and the hasher_identifier.
The encoding is little-endian throughout, with length prefixes that
allow forward-compatible payload extension while preserving strict
variant validation. The wire format is defined (as data definitions)
in uor-foundation's bridge component; produced by prism's
pipeline; consumed by prism-verify's re-export of prism's
certify_from_trace.
Consequences: A non-Rust verifier implementation can be written
against the format specification without reading uor-foundation's
source code. The format is part of the architecture, not an
implementation choice; changing it is a normative architectural change
that requires its own ADR. The length-prefix-on-events discipline allows
new event payload data to be added in future format versions without
breaking existing verifiers, while still rejecting events with
unrecognized variant discriminants.
Rejected alternative: Specifying only the contract the format satisfies (replayability, no decider invocation, hasher-substrate independence) and treating the byte-level specifics as implementation discretion. Rejected because the contract alone does not give a non-Rust verifier implementation the information needed to interoperate; cross-implementation interop requires the byte-level format to be normatively specified.
Status: Accepted.
Context: The certificate format is the byte-level representation of
a Certificate value as it appears inside Certified<C>. Like the
trace wire format, cross-implementation interoperability depends on it.
Decision: The certificate wire format is specified normatively in
section 8 (Cross-cutting Concepts, Certificate Format). A Certificate
is a tuple of kind: CertificateKind and
addresses: Sequence<ContentAddress>. Each ContentAddress is
(ContentFingerprint, hasher_identifier: u32). The wire encoding is
little-endian, length-prefixed, variant-discriminator-prefixed. Like the
trace wire format (ADR-008), the certificate wire format is defined
in uor-foundation's bridge component; produced by prism's
pipeline at the certificate-emission stage; consumed by
prism-verify's re-export of prism's certify_from_trace.
Consequences: The certificate format is fixed across
implementations. Two Grounded<T> values produced by the same author
with different hasher selections produce different ContentAddress
values, which prevents cross-hasher fingerprint collisions from being
treated as equality. The format is forward-compatible by the same
length-prefix discipline as the trace.
Rejected alternative: Embedding the hasher identifier inside the
ContentFingerprint rather than carrying it as a sibling field of
ContentAddress. Rejected because the fingerprint’s bit-width is
variable within the byte-width range carried by the application’s
selected HostBounds; combining it with a fixed-width identifier in one
byte sequence would either fix the fingerprint width (collapsing one
substitution axis) or create an awkward variable-prefix encoding.
ADR-010 — Hashing substrate contract specifies determinism, fixed width, and idempotence under truncation
Status: Accepted.
Context: Hasher is one of the three substitution axes. The
contract any conforming Hasher impl must satisfy determines what kinds
of hash functions can be substituted and what guarantees the
foundation’s content addressing carries.
Decision: A conforming Hasher impl MUST satisfy four properties
(specified in section 8): output is a fixed number of bytes within the
byte-width range carried by the application’s selected HostBounds;
output is deterministic (no hidden state, no time, no randomness); the
impl carries a u32 identifier distinct from every other recognized
impl; the impl is idempotent under truncation (truncating output to a
prefix preserves a useful collision-resistance property at that width).
Consequences: BLAKE3, SHA-256, BLAKE2b, FNV-1a, and similar
implementations can be Hasher impls if they satisfy these properties;
cryptographic hash functions trivially do. The truncation-idempotence
property allows the foundation to specify content fingerprints at the
substituted width without requiring the hasher to know the width in
advance, which simplifies the substitution.
Rejected alternative: Specifying a single recommended hash function (e.g., requiring BLAKE3). Rejected because constraint TC-05 requires substrate-agnostic hashing; recommending one function would not affect substitution but would create the false impression that other functions are second-class.
Status: Accepted.
Context: Constraint TC-02 requires that the seven sealed types be
unconstructable by code outside their owning crate except through the
sanctioned paths. The mechanism by which "unconstructable" is enforced
determines whether the seal is bypassable. The seven types split across
two crates by their architectural role: the four UOR-domain types
(Datum, Triad, Derivation, FreeRank) live in uor-foundation
(substrate); the three Prism-mechanism types (Validated, Grounded,
Certified) live in prism (runtime).
Decision: Sealing is enforced exclusively by Rust’s visibility rules
in both crates, identically: each sealed type’s fields are pub(crate);
each sealed type’s constructor functions are pub(crate) fn. There is
no runtime sentinel, no token type, no checksum, no other mechanism. The
Rust compiler is the entire enforcement mechanism in both crates
(specified in section 8, Sealing Discipline).
For the four UOR-domain types in uor-foundation: the pub(crate)
constructors are callable only from within uor-foundation. Cross-crate
construction goes through uor-foundation's mint primitives component
(a separate cross-crate-public surface), which the architectural
commitment in ADR-016 reserves for prism's pipeline as the sole
sanctioned caller.
For the three Prism-mechanism types in prism: the pub(crate)
constructors are callable only from within prism. The only callers are
pipeline::run (along the principal data path) and certify_from_trace
(during verification, in prism's replay component, re-exported by
prism-verify). There is no cross-crate construction surface for this
group.
Consequences: The seal for each type cannot be bypassed except by
writing source code inside its owning crate. For the UOR-domain four,
the cross-crate construction surface (mint primitives) is pub for
Rust-language reasons; the architectural commitment in ADR-016 is what
makes the call-site enforcement of TC-02 cross-crate-meaningful. For the
Prism-mechanism three, no such commitment is needed because there is no
cross-crate construction at all. This is the strongest enforcement
mechanism Rust offers; it requires no runtime cost (consistent with
TC-01).
Rejected alternative 1: Runtime sentinel values inside sealed structs. Rejected because they introduce runtime cost (constraint TC-01 violation) and can be reconstructed by any code that knows the sentinel’s expected value.
Rejected alternative 2: Token-type sealing (a constructor that
requires a token only the owning crate can produce). Rejected because
tokens leak through Result and Option surfaces in subtle ways and
add a layer of indirection that does not strengthen the seal.
Rejected alternative 3: Sealing all seven types in the same crate.
Rejected because the four UOR-domain types belong to the substrate
(consumed by every Prism implementation regardless of which runtime is
producing values), and the three Prism-mechanism types belong to the
runtime (specific to prism's pipeline implementation). Co-locating
them would force the substrate to carry the runtime’s seal regime,
inverting the dependency direction.
Status: Accepted.
Context: The principal data path’s pipeline (pipeline::run) is the
function that consumes a Validated<CompileUnit, Phase> and produces a
Grounded<T> plus a Trace. Two architectural placements are
admissible: the pipeline lives in uor-foundation (the substrate that
defines the types it operates on) or the pipeline lives in prism (the
runtime that binds the substrate’s types into a working machine). The
choice determines which crate is the substrate (defining vocabulary
only) and which is the runtime (executing operations on the vocabulary).
Decision: The pipeline lives in prism. uor-foundation is purely
a substrate: it owns the type-declaration vocabulary, the four
UOR-domain sealed type definitions, the wire-format type definitions,
the kernel/primitives substrate, and the mint primitives. It does NOT
own a pipeline runtime. prism is the runtime: it owns the pipeline,
the three Prism-mechanism sealed types' seal regime, the replay
machinery, the operation-declaration vocabulary, and the standard type
library, all closed under uor-foundation's vocabulary (ADR-013).
Consequences: An alternative Prism runtime could in principle be
implemented as a different crate (prism-2) that consumes the same
uor-foundation substrate and produces values of the same UOR-domain
sealed types via the same mint primitives. The substrate is reusable;
the runtime is the variable layer. uor-foundation is also smaller as a
result — it carries only what every conceivable Prism runtime would
need, not the runtime mechanism itself. Application authors and
verification consumers do not perceive this split: the author imports
prism, which re-exports uor-foundation's vocabulary; the user
imports prism-verify, which re-exports prism's certify_from_trace
and Certified plus uor-foundation's wire-format types.
Rejected alternative 1: The pipeline lives in uor-foundation.
Rejected because it conflates substrate and runtime: the substrate’s job
is to define the vocabulary; the runtime’s job is to execute operations
on the vocabulary. Co-locating them in uor-foundation would prevent
the substrate from being reused by alternative Prism runtimes, and would
make uor-foundation carry runtime mechanism that consumers of the
substrate-only surface (e.g., a verification-only consumer) do not need.
Rejected alternative 2: The pipeline is split between
uor-foundation (the principal data path’s stages as inert types) and
prism (the orchestration). Rejected because it produces an awkward
boundary mid-pipeline; the pipeline is conceptually one function, and
splitting its implementation across two crates produces more brittle
boundaries than placing the entire pipeline in prism.
Status: Accepted.
Context: prism is the Prism runtime; it sits on top of
uor-foundation and produces sealed values consumable by the
application author. Two architectural choices determine prism's
relationship to uor-foundation: closure (every type and operation
prism exposes is derived from uor-foundation's vocabulary) versus
extension (prism may introduce primitive types or PrimitiveOp
discriminants of its own, independently of uor-foundation).
Decision: prism is closed under uor-foundation's vocabulary.
Every type prism exposes is derived from uor-foundation's
type-declaration vocabulary; every operation declaration prism's
vocabulary admits composes uor-foundation::PrimitiveOp discriminants.
prism introduces no primitive types and no primitive operations of its
own. The three Prism-mechanism sealed types (Validated, Grounded,
Certified) are seals over uor-foundation's types and the
trace/certificate wire-format types, not new primitive types — they wrap
and add invariants but do not introduce new domain content.
Consequences: A prism amendment that needs a new primitive type or
PrimitiveOp discriminant cannot proceed without first amending
uor-foundation. This is the primary maintenance coupling between the
two crates; it is captured as TR-08 (section 11). The benefit is that
UORassembly’s clauses are checkable by examining uor-foundation alone
— the substrate is the full primitive vocabulary, and prism cannot
smuggle in new primitives that would extend that vocabulary outside the
substrate. A second benefit is that alternative Prism runtimes (per
ADR-012) consuming uor-foundation are bounded by the same vocabulary;
the closure property is what makes substrate-shared, runtime-distinct
architectures coherent.
Substrate closure under foundation’s vocabulary (this ADR) is one of three architectural closures specified by ADR-024: substrate closure (this ADR + ADR-025’s operator-set commitment), prism closure (ADR-026’s operator-set commitment), and implementation closure (ADR-024’s verb-pattern commitment). The three closures compose: prism’s operator set takes substrate-closed operands; implementation verb sets compose prism operators applied to substrate primitives.
ADR-030 specifies the substrate-extension declaration mechanism (the
axis! SDK macro and the AxisTuple substitution-axis structure);
ADR-031 specifies that the prism crate is the standard library — a
façade re-exporting the architecture from uor-foundation plus the
standard-library Layer-3 sub-crates that contribute axis declarations
and verb declarations to the ecosystem. Together they extend ADR-013’s
substrate-closure framing to the universal-domain scope: any
application’s substrate-extension vocabulary (cryptographic primitives,
tensor operations, homomorphic computation, high-precision arithmetic,
etc.) is declared through the axis! mechanism and contributed by a
Layer-3 crate (standard-library or third-party); the closure discipline
applies per-axis at compile time. Axis declarations are not substrate
amendments — they extend the substrate-extension lane, not the
substrate itself.
Substrate amendments per TR-08 to date: ADR-032 extends
ConstrainedTypeShape with the CYCLE_SIZE: u64 associated const
(consumed by first_admit's measure-literal emission per ADR-026 G16);
ADR-033 adds Term::ProjectField (eleventh variant) for product-shape
field-access projection per ADR-029; the PrimitiveOp catalog has
extended through foundation 0.3.5 (adding Le/Lt/Ge/Gt/Concat);
ADR-022 D3 G3, ADR-026 G12, and ADR-029’s Term::Application fold-rule
reference the catalog as snapshot-specific. ADR-034 adds
Term::FirstAdmit (twelfth variant) for bounded search with structural
short-circuit and extends Term::Recurse's fold-rule with
iteration-counter binding via the foundation-fixed
RECURSE_IDX_NAME_INDEX.
ADR-035 adds nine ψ-chain Term variants (Nerve, ChainComplex,
HomologyGroups, Betti, CochainComplex, CohomologyGroups,
PostnikovTower, HomotopyGroups, KInvariants) bringing the Term
enum from twelve variants to twenty-one. Eight of the nine are
resolver-bound (consult the model’s R: ResolverTuple per ADR-036 at
evaluation time); one (Betti) is resolver-free. ADR-035 commits the
canonical k-invariants branch (ψ_1 → ψ_7 → ψ_8 → ψ_9) as the
canonical composition for the verifiability commitment and the
ψ-residuals discipline on verb-body terms (no Term::FirstAdmit, no
Term::AxisInvocation, no byte-comparison or byte-concat PrimitiveOp
emissions).
ADR-036 adds a fourth substrate parameter R: ResolverTuple (defaulting
to NullResolverTuple) and the supporting surface: the ResolverTuple
trait, the ResolverCategory enum, the eight resolver traits (each with
a uniform resolve method — writer-style
fn resolve(&self, input: &[u8], out: &mut [u8]) → Result<usize, ShapeViolation>
as ADR-036 committed it, amended by ADR-060 to return a TermValue
directly), the eight Has<Category>Resolver<H> marker traits, the
MAX_RESOLVER_TUPLE_ARITY const, the foundation-internal
RESOLVER_ABSENT_DISCRIMINATOR byte, and the eight Null* impls
satisfying NullResolverTuple.
Each new variant and surface is governed by TR-08; the closure
discipline applies — substrate constructs are emitted only by SDK macro
recognition (ψ-Term variants per G21-G29; resolver impls per
resolver!); ψ-residual emissions are rejected at proc-macro expansion.
ADR-037 reconciles the foundation-fixed capacity caps introduced through
this ADR’s substrate-amendment-via-foundation rule with ADR-018’s
commitment. Data-shape capacity caps are not substrate amendments in the
sense this ADR covers (primitive types and PrimitiveOp discriminants);
they are HostBounds associated constants per ADR-018. Type-system
tuple-impl-table caps (MAX_AXIS_TUPLE_ARITY,
MAX_RESOLVER_TUPLE_ARITY) stay foundation-vetted with explicit
Rust-language carve-out per ADR-037. The
substrate-amendment-via-foundation rule covers the catalog vocabulary;
the application-side data-shape capacity surface lives on HostBounds.
Substrate-amendment audit trail (ADR-038 through ADR-061). Each
subsequent ADR is classified per this ADR’s rule. The wire-format
version constant bumps for every entry marked Amends wire-format;
entries that touch only architectural reading or type-system surface
preserve the wire format.
| ADR | Substrate amendment? | Summary |
|---|---|---|
| ADR-038 | Yes — amends wire-format | Adds observable:AxisProjectionObservable as a new top-level Observable subclass. |
| ADR-039 | No | Verdict realization mapping for the canonical k-invariants branch; Grounded<Output> and Err(PipelineFailure) realize the ontology’s three-primitive inhabitance verdict structure without introducing new substrate primitives. |
| ADR-040 | Yes — amends wire-format | Commits a 7-individual BoundShape catalogue with type:LexicographicLessEqBound (byte-sequence comparison) and type:LessEqBound (integer-valued observables); each catalog primitive corresponds 1:1 to a foundation-published ObservablePredicate impl per ADR-049, with LexicographicLessEqBound realized by LexicographicLessEqThreshold under the observable:ValueThresholdObservable taxonomy subclass. |
| ADR-041 | No | Typed-coordinate resolver carriers — newtype views over the existing substrate’s byte buffers; no wire-format change. |
| ADR-042 | No | Typed verdict-envelope surfaces (accessor methods, dispatch helpers) over the existing substrate; no wire-format change. |
| ADR-043 | No | Iterative-resolution discipline canonicalizing the resolver-internal computational pattern (FreeRank protocol; convergence/exhaustion; impossibility-witness emission) over existing constructs (resolver traits per ADR-036, typed carriers per ADR-041, ConstrainedTypeShape::CYCLE_SIZE per ADR-032, ConstraintRef::Bound per ADR-040, proof:InhabitanceImpossibilityWitness per ADR-039). |
| ADR-044 | No | Amends ADR-033’s partition_product! emission shape to the split-const form on a foundation-declared PartitionProductFields trait; the wire format is unchanged. |
| ADR-045 | No | Adds the Grounded::tag::<NewTag>() consuming method for zero-cost application-domain Tag rebinding; the wire format is unchanged. |
| ADR-046 | No | Records the discipline-scope boundary between ADR-035’s verb-body ψ-residuals discipline and ADR-043’s resolver-body iterative-resolution discipline; structural reading only. |
| ADR-047 | No | Commits the σ-Projection Hardening Principle (U1–U6) as axioms qualifying Hasher impls per ADR-030; constrains qualification without altering the trait surface. |
| ADR-048 | Yes — amends wire-format | Adds the foundation-declared TypedCommitment trait, three built-in impls (EmptyCommitment, SingletonCommitment<P>, AndCommitment<A, B>), the TargetCommitment = SingletonCommitment<LexicographicLessEqThreshold> canonical search-cost commitment alias, and the fifth C: TypedCommitment model-declaration parameter on PrismModel extending the substrate parameter shape from <H, B, A, R> to <H, B, A, R, C>. Wire-format gains the CommitmentEvaluated trace event variant. |
| ADR-049 | Yes — amends wire-format | Adds the foundation-declared typed UOR observable primitives (Stratum<P>, WalshHadamardParity, UltrametricCloseTo<P>, AffineParity, LexicographicLessEqThreshold), the ObservablePredicate trait, the axis::cryptanalyze::<H: Hasher>(samples) → CryptanalysisReport substrate test primitive, and the Observable IRIs for the five primitives under the existing ADR-038 taxonomy (Stratum + AffineParity under StratumObservable; WalshHadamardParity under a new SpectralObservable subclass; UltrametricCloseTo under MetricObservable; LexicographicLessEqThreshold under a new ValueThresholdObservable subclass realizing the type:LexicographicLessEqBound catalog primitive per ADR-040). |
| ADR-050 | Wire-format bumps | Width-parametric evaluation discipline for the ring-axis and hypercube-axis arithmetic fold-rules at the full Witt tower; no new variants or discriminants, but traces emitted prior carry width-truncated results that differ structurally from post-ADR-050 emissions. |
| ADR-051 | Yes — amends wire-format | Widens Term::Literal's value carrier from u64 to TermValue (byte sequence sized to level.witt_length() / 8). Carrier shape amended by ADR-060 (source-polymorphic TermValue<'a, INLINE_BYTES>; the wide literal occupies the Inline variant). |
| ADR-052 | No | Amends the axis! SDK macro’s emission discipline to admit parametric impl types via a generic-form companion macro; the substrate’s AxisExtension trait and the catamorphism’s Term::AxisInvocation fold-rule are unchanged. |
| ADR-053 | Yes — amends wire-format | Extends the PrimitiveOp catalog with Div, Mod, Pow (catalog now 18 variants); foundation declares the three new discriminants, the per-variant fold-rules per ADR-050’s width-parametric discipline, the b = 0 shape-violation IRIs for Div/Mod, the three new GeometricCharacter individuals (Quotient, Remainder, IteratedScaling). The Lean corpus extends with DV_1..DV_4 (Euclidean division identities) and PW_1..PW_3 (exponentiation identities). |
| ADR-054 | No | Commits the Fold-Fusion Principle as a normative architectural reading over existing constructs (ADR-019’s catamorphism universal property + ADR-024’s three-layer closure + ADR-029’s per-variant fold-rules + ADR-031’s standard-library Layer-3 sub-crates + ADR-053’s folding-transformation criterion). ADR-054 RA2 (the standard-library-only scope of the canonical axis impl body discipline) is superseded by ADR-055. |
| ADR-055 | Yes — amends wire-format | Universalizes the substrate-Term verb body discipline across every AxisExtension impl (standard-library AND application-author custom) via the foundation-declared SubstrateTermBody supertrait bound on AxisExtension. The catamorphism’s Term::AxisInvocation fold-rule per ADR-029 extends to recursively fold the axis impl’s body_arena() static Term slice rather than calling an opaque kernel function; the axis! SDK macro per ADR-030 + ADR-052 extends with a normative body clause; ADR-010’s arbitrary-Rust Hasher carve-out is amended accordingly. The on-wire shape of Term::AxisInvocation is preserved; the version constant bumps for the new trait declaration. |
| ADR-056 | No | Refines ADR-035’s ψ-residuals discipline scope to the route body’s syntactic surface (the prism_model!-declared route function’s closure body), explicitly excluding compound verb bodies declared via verb! per ADR-024, axis impl bodies per ADR-055, and resolver bodies per ADR-046 from the discipline’s vocabulary restriction. Unblocks substrate-Term decomposition of canonical compound operations (SHA padding, HMAC, Merkle, tensor saturation) that require Concat / Le / Lt / Ge / Gt / Term::AxisInvocation internally. Substrate vocabulary unchanged; wire format unchanged; proc-macro discipline-walk scope is the only architectural change. ADR-035 RA7 scope is correspondingly refined. |
| ADR-057 | Yes — amends wire-format | Adds the foundation-declared ConstraintRef::Recurse { shape_iri, descent_bound } variant (and the LeafConstraintRef::Recurse parallel) for bounded recursive structural typing at the constraint-geometry level, the foundation shape_iri_registry module + register_shape! SDK macro for link-time shape-IRI registration, the ψ_1 NerveResolver evaluation extension that unrolls Recurse references against the registry up to the descent budget, the const-time path’s deferral of Recurse to runtime, the partition_coproduct! / partition_product! macro extension admitting recurse(<bound>):<T> operand markers, and the CYCLE_SIZE = u64::MAX saturation rule for shapes carrying Recurse constraints. The ConstraintRef wire-format type gains a Recurse variant tag carrying (shape_iri, descent_bound); wire-format version constant bumps. Unblocks bounded recursive structural typing for JSON, XML, code-module ASTs, S-expressions, protocol-message families, filesystem-like hierarchies, and categorical constructions without per-application const-eval-cycle-break invention. |
| ADR-058 | No | Commits κ-derivation as the framework’s compression operator under the structural reading: the eight-resolver ψ-pipeline composed with the ψ_9 σ-projection emits the unique minimum-information byte sequence distinguishing the input within its constraint geometry’s typed-distinction surface. Identity claim over existing constructs (ADR-019 + ADR-035 + ADR-043 + ADR-047). Introduces the three-tier closure-lossless taxonomy (T1 byte-identical, T2 κ-label-identical, T3 outcome-coarse-equivalent) as a typed equivalence vocabulary for application-level interoperability protocols. Cross-substrate compression universality is committed as a closure property; substrate-independence under compression is binary under TC-05. Conceptual-reading commitment; no new substrate trait declarations, no wire-format change. |
| ADR-059 | No | Commits the Atlas image inside E₈ as the codomain of κ-derivation in operator-geometry coordinates, with the Hopf convergence tower (R / C / H / O at algebra dimensions {1, 2, 4, 8}) per kernel::convergence as the coarse stratification and the exceptional algebraic structures (G₂ via product, F₄ via quotient, E₆ via filtration, E₇ via augmentation, E₈ via direct embedding) as finer-grained codomain typing. Universal factorization through the Atlas as initial object in ResGraph; cross-substrate codomain universality is provable as a categorical theorem under the joint commitments of ADR-058 + ADR-059. Application-level typed-commitment surfaces per ADR-048 gain a codomain-typed vocabulary (Atlas-image proximity, exceptional-group orbit membership, convergence-tower level-and-residual signature) for canonical-form admission predicates. Conceptual-reading over the existing kernel::convergence substrate vocabulary; no new substrate trait declarations, no wire-format change. |
| ADR-060 | No — wire format unchanged; public-API surface replaced wholesale | Supersedes ADR-037’s byte-width-cap family. Removes the 12 byte-width capacity constants from HostBounds (TERM_VALUE_MAX_BYTES, AXIS_OUTPUT_BYTES_MAX, ROUTE_INPUT_BUFFER_BYTES, ROUTE_OUTPUT_BUFFER_BYTES, and the 8 ψ-stage *_OUTPUT_BYTES_MAX ceilings) and removes DefaultHostBounds entirely (every application declares its own impl HostBounds). Replaces the fixed-buffer TermValue with a source-polymorphic TermValue<'a, const INLINE_BYTES: usize> enum (Inline / Borrowed / Stream); the Inline width is foundation-derived via carrier_inline_bytes::<B>() (the max over the application’s Witt-literal width, fingerprint width, and κ-label ASCII width — all mathematically/structurally grounded), Borrowed/Stream carriers have no byte-width ceiling, and Stream(&'a dyn ChunkSource) admits unbounded payloads. Per-ψ-stage carrier widths derive from foundation const fns (nerve_carrier_bytes::<B>() etc.) as structural-count × foundation-fixed per-element wire width. The 8 ψ-stage resolver traits return a TermValue directly rather than writing into a caller-supplied &mut [u8]; the streaming-σ-projection (chunk-folding at ψ_9) becomes a foundation-level surface. HostBounds drops from 26 to 14 associated constants (4 pre-ADR-018 + 10 retained migrated structural/Witt/catamorphism-trace constants). The κ-label, trace, and certificate wire formats are byte-identical (conformance vectors verify unchanged reference κ-labels); no #[deprecated] shim — the 0.5.0 surface is the only surface. The 14 retained constants and the type-system impl-table caps (MAX_AXIS_TUPLE_ARITY / MAX_RESOLVER_TUPLE_ARITY) per ADR-037 branch (2) are unaffected. |
| ADR-061 | No | Commits the operational κ-label composition surface (prism-runtime-level, building on ADR-058 + ADR-059): the five categorical operations on the Atlas image inside E₈ — product (G₂), quotient (F₄), filtration (E₆), augmentation (E₇), direct embedding (E₈) — are each a ConstrainedTypeShape in prism’s standard type library per ADR-031 (G2ProductShape<N> binary; F4QuotientShape<N> / E6FiltrationShape<N> / E7AugmentationShape<N> / E8EmbeddingShape<N> unary). A composition of N κ-labels under operation C is a typed-input value consumed by the existing ψ-pipeline; its canonicalize verb emits a canonical form whose σ-projection is the composed κ-label — itself a κ-label, recursively composable (closed under the Atlas per ADR-059). Arity ≤ 3 / depth ≤ 8 per the Categorical X regime split (ADR-025) and ADR-059’s H-/O-level bounds; wide compositions decompose via ConstraintRef::Recurse per ADR-057. σ-axis substitutability (ADR-047) and cross-substrate universality (ADR-058 + ADR-059) lift to compositions. No foundation or SDK change: TypedCommitment (ADR-048) and ObservablePredicate (ADR-049) closed sets retained; no new substrate trait, no wire-format change. Realization-layer canonicalize verbs (per shape) and Lean conformance follow the existing per-realization discipline. |
Rejected alternative 1: prism may introduce new primitive types
and operations. Rejected because it makes the substrate’s vocabulary
insufficient to characterize Prism implementations; UORassembly clauses
would have to enumerate primitives across both crates, and alternative
runtimes would each carry their own primitive extensions, defeating the
substrate-as-shared-vocabulary property.
Rejected alternative 2: prism re-exports uor-foundation's
vocabulary unchanged but its standard type library is allowed to
introduce new primitive types. Rejected because the standard type
library is, by definition, convenient pre-declared types built from
existing vocabulary; allowing it to introduce primitives would break the
convenience-vs-capability distinction (the standard library is
convenience; extension is capability that requires substrate amendment).
Status: Accepted.
Context: Application authors need to express domain-specific
operations: a particular shape’s validation rule, a particular
composition of primitives, a particular grounding logic. Two
architectural choices: prism ships operations (it provides a library
of pre-implemented operations the author selects from), or prism ships
only the vocabulary (the author declares operations as compositions of
uor-foundation::PrimitiveOp discriminants).
Decision: prism ships the vocabulary, not operations. Operations
are application-author declarations expressed in prism's
operation-declaration vocabulary, ultimately reducing to compositions of
uor-foundation::PrimitiveOp discriminants. The author writes the
declaration; prism provides combinators, type-level constraints, and
witnessing scaffolds; the Rust toolchain enforces the composition’s
well-typedness.
Consequences: Two applications using the same primitive set may
declare entirely different operation surfaces, each well-typed against
prism's vocabulary. The architecture is operation-extensible by
design: extension is the author’s act, not a prism release. prism
versions do not need to change to support new operations; they need to
change only when the vocabulary itself is extended (which requires
uor-foundation amendment per ADR-013). The cost is that authors who
want pre-built operations need to either compose them themselves or
import a third-party library that does so; the standard type library
(standardTypeLibraryComp) is the closest thing prism provides to
pre-built operations, and even it is built from existing vocabulary, not
from a different layer.
Rejected alternative: prism ships a library of pre-implemented
operations. Rejected because it would require prism to anticipate the
application domains its consumers work in, which is an open-ended
obligation; prism's release cadence would couple to domain-specific
operation requests, defeating the substrate-stability property.
Status: Accepted.
Context: The three crates that realize Prism need source
repositories. Two architectural choices: a single repository hosting all
three crates (monorepo), or a split where the substrate
(uor-foundation) lives in one repository and the runtime + replay
surface (prism, prism-verify) live in another.
Decision: uor-foundation is published from
UOR-Foundation/UOR-Framework. prism and prism-verify are published
from UOR-Foundation/Prism. The wiki (this repository) lives in
UOR-Framework alongside uor-foundation. All three crates are
published to crates.io; consumers see only crates.io and not the
repository split.
Consequences: The substrate (uor-foundation) and the runtime
(prism + prism-verify) have independent release cadences. A
uor-foundation amendment can be released without coordinating with the
prism repository; conversely, prism can iterate on the runtime
without a uor-foundation release. Cross-repo coordination is required
only when prism needs new substrate vocabulary (ADR-013); this
requires sequencing the uor-foundation release first, then a prism
repin, captured as TR-09 (section 11). Repository ownership and access
controls are separable: substrate maintainers and runtime maintainers
can be different teams without one team’s commits affecting the other’s
repository. Repo locality is invisible at build time: cargo resolves all
three from crates.io transparently.
Rejected alternative 1: Monorepo containing all three crates. Rejected because it couples release cadences and produces single-team ownership where two-team ownership is architecturally cleaner. The substrate is a long-lived layer that should change rarely; the runtime is a layer that may iterate more frequently.
Rejected alternative 2: Three separate repositories (one per crate).
Rejected because prism and prism-verify are tightly coupled (the
replay machinery is in prism; prism-verify is a thin façade
re-exporting it); separating them buys nothing and adds cross-repo
coordination overhead at every release.
Status: Accepted.
Context: ADR-011 records that sealing is enforced by Rust’s
visibility rules (pub(crate) constructors). For sealed types within a
crate (the three Prism-mechanism types in prism), pub(crate) is
sufficient: the type’s owning crate is the only crate that can construct
values of the type. For sealed types where construction must cross a
crate boundary (the four UOR-domain types in uor-foundation, which
prism's pipeline must construct), pub(crate) alone is insufficient:
prism cannot reach uor-foundation's pub(crate) constructors
directly. Some mechanism is required to bridge this gap.
Decision: uor-foundation exposes a set of pub mint primitives —
mint_datum, mint_triad, mint_derivation, mint_freerank,
mint_product_witness, mint_coproduct_witness,
mint_cartesian_witness — that take type-level-validated inputs and
internally call the pub(crate) constructors of the four UOR-domain
sealed types. The architectural commitment is that prism's pipeline is
the only sanctioned caller of these mint primitives. The commitment is
normative; it is not a Rust-language access restriction. A Prism
implementation in which any code other than prism's pipeline calls a
mint primitive is not a Prism implementation.
The three Prism-mechanism sealed types (Validated, Grounded,
Certified) are NOT exposed via cross-crate construction. They are
sealed in prism itself; the constructors are pub(crate) to prism
and the only callers are prism's pipeline (along the principal data
path) and prism's replay (during verification, re-exported by
prism-verify as certify_from_trace).
Consequences: TC-02 holds across both crates uniformly. For the four
UOR-domain types, the seal is mediated by uor-foundation's mint
primitives plus the architectural commitment in this ADR; for the three
Prism-mechanism types, the seal is mediated by prism's pub(crate)
constructors directly. Conformance to the architectural commitment is
observable: code that calls a mint primitive from outside prism's
pipeline is non-conforming. The primary risk is silent non-conformance:
a future contributor to prism could call a mint primitive from outside
the pipeline component; this would be a code-review concern, since the
language does not catch it. The mitigation is a code-level lint that can
be added to prism's CI to detect mint-primitive calls outside the
pipeline component; the wiki does not normatively require this lint,
only the architectural commitment.
Rejected alternative 1: A friend-module mechanism (granting prism
privileged access to uor-foundation's pub(crate) constructors).
Rejected because Rust has no friend-module mechanism. Implementing one
through unsafe transmutes or other tricks would be a runtime cost (TC-01
violation) and would remove the seal’s benefit by introducing a
maintenance hazard.
Rejected alternative 2: Move the four UOR-domain types into prism
so pub(crate) is sufficient. Rejected because the four UOR-domain
types belong to the substrate (every Prism implementation, including
alternative runtimes per ADR-012, would need them); moving them into
prism would couple the substrate’s vocabulary to the runtime’s
identity, breaking the substrate-as-shared-vocabulary property.
Rejected alternative 3: Token-type cross-crate seals (a constructor
that requires a token only the substrate would issue to a known
runtime). Rejected because tokens leak through generic Result/Option
surfaces (per ADR-011’s rejected alternative 2), and the architectural
commitment of this ADR is observable through code-level inspection
without the runtime cost or surface complication tokens introduce.
Status: Accepted.
Context: prism's standard library exposes pre-declared types built
from uor-foundation's vocabulary. Application authors and
schema-import tools target these types. For interoperability —
consistent traces, replayable certificates, schema-import tool stability
— values produced by different applications using the same standard type
must address identically in UOR.
Decision: Every type in prism's standard library is a canonical
UOR-address mapping for its shape. Each standard type’s UOR IRI is
content-deterministic in its constraint declaration (which composes
uor-foundation's vocabulary per ADR-013). Two applications using the
same prism standard type produce values with the same UOR IRI. The
standard library catalog — the specific named types prism ships — is
published in prism's crate documentation, not in this wiki; the wiki
commits to canonicality of the mappings, not to a specific catalog.
Consequences: The standard library is a canonical addressing
surface. Schema-import tools that emit prism::Bytes32 produce traces
and certificates that address consistently regardless of which
application runs them. Application authors who hand-declare a type with
the same constraints as a standard type produce the same UOR address
(closure makes IRIs derivative, not namespace-claimed). Authors are not
limited to the standard library: through prism's re-exports of
uor-foundation's type-declaration vocabulary (ConstrainedTypeShape,
Grounding, the shape proc-macros, the substitution-axis traits),
authors declare their own types and run them through the pipeline as
first-class Prism types. Author-declared types receive the same
content-deterministic IRIs, the same UORassembly enforcement, and the
same sealing properties as standard library types — the standard library
is convenience, not capability. The catalog evolves under prism's
release discipline; addition of new standard types is additive within a
major version. The wiki specifies the architectural commitment;
release-management discipline is operational.
Rejected alternative 1: prism claims a dedicated IRI namespace
(e.g., urn:uor:prism:…). Rejected because closure under
uor-foundation (ADR-013) makes IRIs content-deterministic from
constraints, not from a separate namespace; introducing a prism
namespace would either duplicate the closure-derived addressing or break
it.
Rejected alternative 2: Specify the standard library catalog in the
wiki. Rejected because the catalog is operational content — it grows as
application domains surface needs — and pinning it in the wiki would
force wiki revisions for every catalog addition. The wiki commits to
canonicality; the catalog lives in prism's crate documentation.
Status: Accepted. Refined by ADR-060 for byte widths. ADR-018’s
commitment — no capacity bound that varies along the principal data path
lives outside HostBounds — is honored more strictly after ADR-060:
byte-width carrier sizes are no longer application-declared
HostBounds constants but foundation-derived from the application’s
structural and Witt/crypto primitives (the source-polymorphic
TermValue carrier’s inline width via carrier_inline_bytes::<B>();
the per-ψ-stage carrier widths via foundation const fn). Bounded
carriers carry no application-policy byte-width ceiling, and unbounded
payloads flow through TermValue::Stream with no ceiling at all. The
structural counts and the catamorphism/trace bounds remain HostBounds
associated constants per ADR-037.
Context: ADR-007 allocates HostBounds as one of three substitution
axes and declares the axis’s contract is what prism requires. The
axis’s purpose is to admit per-application variation in capacity bounds
without runtime variation. For that purpose to be served, every capacity
bound that varies along the principal data path must flow through
HostBounds. A capacity bound that lives outside HostBounds (as a
free-standing constant or a closed enum of foundation-controlled
variants) collapses the substitution axis at that bound: the application
cannot vary the bound, regardless of which HostBounds it selects. The
architecture treats this as a defect, not a tradeoff.
Decision: HostBounds carries every capacity bound that varies
along the principal data path. The architectural surface admits no
capacity bound outside HostBounds. Specifically:
-
Fingerprint output width range. The byte-width range any selected
Hasherimpl produces, the wire format encodes, and the verifier validates against, is carried byHostBoundsas associated constants. No foundation-global constants establish the range. -
Trace event-count ceiling. The maximum number of
TraceEventvalues aTracemay carry is carried byHostBounds. No foundation-global constant establishes the ceiling. -
Algebraic level bit-width ceiling. The bit-width ceiling that bounds any algebraic level the principal data path computes against is carried by
HostBounds. No foundation-global constant or closed enum of foundation-controlled level variants establishes the ceiling. -
Any further capacity carried by sealed values along the principal data path. New capacity classes added in the future are added to
HostBounds; they do not appear as free-standing items in the foundation’s surface.
Every signature in prism's and uor-foundation's public API that
admits a value with a capacity-bounded width parameterizes that width
through the application’s selected HostBounds.
[u8; H::FINGERPRINT_MAX_BYTES] (or its equivalent) is the canonical
pattern; [u8; FINGERPRINT_MAX_BYTES] referring to a free-standing
constant is non-conforming.
Consequences: An application — for example, a content-addressing
consumer that requires specific bit-widths (256-bit fingerprints, a
specific algebraic level ceiling, a specific trace ceiling for its
operational regime) — selects those by providing a HostBounds impl
that declares them. The principal data path, the seal regime, the trace
wire format, the certificate wire format, and the replay surface are all
monomorphized against that selection at the application’s compile time.
The resulting executable is a structure-preserving compile-time
specialization of the abstract Prism architecture: every architectural
property (TC-01 through TC-06) holds, and every capacity is fitted to
the application’s needs without runtime variation.
The substrate’s role is to define the HostBounds trait surface and to
carry through the parameterization in every signature that touches a
capacity-bounded value. The substrate provides DefaultHostBounds as a
convenience for applications whose capacities match the default
selection; applications with different capacity needs provide their own
impl, which the bilateral compile-time UORassembly contract (TC-04)
verifies against prism's declared bounds.
ADR-037 completes this commitment for data-shape capacities. Fourteen
free-standing pub const usize data-shape capacity caps across the
foundation’s pipeline and enforcement components
(TERM_VALUE_MAX_BYTES, AXIS_OUTPUT_BYTES_CEILING,
FOLD_UNROLL_THRESHOLD, MAX_BETTI_DIMENSION, NERVE_CONSTRAINTS_CAP,
NERVE_SITES_CAP, JACOBIAN_MAX_SITES, RECURSION_TRACE_MAX_DEPTH,
MAX_OP_CHAIN_DEPTH, AFFINE_MAX_COEFFS, CONJUNCTION_MAX_TERMS,
ROUTE_INPUT_BUFFER_BYTES, ROUTE_OUTPUT_BUFFER_BYTES,
UNFOLD_MAX_ITERATIONS) plus the eight ψ-stage resolver output
byte-buffer ceilings — all 14 + 8 migrate to HostBounds associated
constants per ADR-037. Foundation’s DefaultHostBounds impl extends to
carry the prior fixed values as defaults; applications selecting
DefaultHostBounds see no observable change. Two type-system
tuple-impl-table caps (MAX_AXIS_TUPLE_ARITY,
MAX_RESOLVER_TUPLE_ARITY) stay foundation-vetted with explicit
Rust-language carve-out from this ADR’s discipline: they are
foundation’s per-arity macro-emission limits, structurally bound to
Rust’s lack of variadic generics, not application-varying capacity
bounds. MAX_RESOLVER_TUPLE_ARITY is structurally bounded below by
card(ResolverCategory) (8 per ADR-035’s eight resolver-bound ψ-stages,
tracking any ADR-013/TR-08 substrate amendments that revise its
cardinality). The architectural surface restores compliance with this
ADR’s commitment for all data-shape capacities; the impl-table carve-out
is explicit and bounded.
Rejected alternative 1: Foundation-global capacity constants
declared once in uor-foundation and referenced by every signature.
Rejected because this collapses the HostBounds substitution axis at
those bounds: the application cannot vary the constant, the selected
HostBounds does not control it, and applications with capacity needs
outside the constant must either accept the foundation’s choice or fork
the substrate. ADR-007’s guarantee that variation is substitutable does
not hold under this alternative.
Rejected alternative 2: A closed enum of foundation-controlled variants for bit-width selection (e.g., a discrete set of supported levels). Rejected because the enum’s variant set is foundation-fixed: applications with bit-width needs not in the enum cannot express their capacity through any substitution axis. The substitution-axis discipline names the application as the locus of variation; a closed enum places the locus at the foundation.
Rejected alternative 3: Per-application capacity bounds carried
through a fourth substitution axis, leaving HostBounds to mean only
"the present narrow set of capacities." Rejected because there is no
principled distinction between "host bounds" and "other capacity
bounds"; a fourth axis would duplicate HostBounds's role and create an
opaque allocation rule for which capacities go where. The principled
position is that HostBounds is the carrier of every capacity, and the
trait’s associated-constant surface enumerates them.
ADR-019 — Foundation is a closed signature endofunctor; Term is its initial algebra; pipeline::run is the catamorphism
Status: Accepted.
Context: ADR-013 commits Prism to closure under uor-foundation's
vocabulary: every type prism exposes derives from uor-foundation's
type-declaration vocabulary; every operation declaration composes
uor-foundation::PrimitiveOp discriminants. TC-01 commits Prism to a
zero-cost runtime: no Prism runtime layer mediates the function call
into pipeline::run. The two have been stated as separate properties.
They are not separate; they are two halves of one categorical theorem,
and stating that theorem in its native vocabulary lets the rest of the
architecture compose against it without re-deriving the result at every
reference site.
Decision: uor-foundation's vocabulary is the signature
category of Prism’s typed routes. The category’s objects are
ConstrainedTypeShape impls under the substitution-axis selections; its
morphisms are typed compositions of PrimitiveOp discriminants and
Term::Application constructions. The category supports a signature
endofunctor F whose signature is enriched: first-order algebraic
constructors (one per PrimitiveOp discriminant; one per first-order
Term variant — Literal, Application, Lift, Project), plus
binding (Variable), case analysis (Match), explicit fixed-point
(Recurse), explicit unfold (Unfold), and failure-promote (Try).
Term is F’s initial algebra in this enriched sense: any well-typed
term tree is an element of the free term language F generates from its
enriched signature, and any carrier supporting the same enriched
structure admits a unique structure-preserving map from Term.
Initiality entails that for any such carrier (any carrier with
operations matching the enriched signature), there is a unique
structure-preserving map from Term into that carrier — the
catamorphism into the carrier. pipeline::run is the catamorphism
into the runtime carrier (carrier parameterized by the substitution
axes; see Consequences); the replay surface is the dual
anamorphism the trace witnesses; the four UOR-domain sealed types
and the three Prism-mechanism sealed types are fixed points of the
typed pipeline endofunctor (distinct from F; see section 8, Fixed
Points). The categorical reading is normative: the architecture’s
behavior is determined by the structure F + initial algebra +
catamorphism, and any Prism implementation that admits a route,
sealed-type construction, or trace replay outside this structure is
non-conforming. The catamorphism’s per-variant evaluation semantics —
the fold-rules that turn Term-shaped input into carrier-shaped output by
induction on Term structure — are specified normatively in ADR-029.
ADR-019 establishes the categorical structure (initial algebra, unique
morphism into the carrier, parametricity in (H, B, A)); ADR-029
specifies the fold-rules that realize the catamorphism at the value
level. The two together fully specify pipeline::run as a real
catamorphism: ADR-019 provides the categorical commitment, ADR-029
provides the operational realization.
Consequences: The closure property (ADR-013) and the zero-cost
runtime (TC-01) are two halves of one theorem: closure is the
precondition that makes F’s signature complete; completeness lets the
catamorphism be discharged entirely at the application’s compile time
(TC-04, UORassembly), with no runtime indirection through opaque
imports; TC-01 follows. Stating the theorem in its native vocabulary
lets later commitments — PrismModel (ADR-020), the relationship
between trace and certificate, the seal regime’s coverage of fixed
points — compose against initiality, completeness, and uniqueness rather
than re-establishing them per reference. The vocabulary
uor-foundation's public surface gains is editorial: signature
endofunctor, F-algebra, initial algebra, catamorphism, anamorphism,
fixed point. None of these names a new runtime concern; each names a
structure already present in the architecture.
The carrier pipeline::run evaluates against is parameterized by the
three substitution axes (HostTypes, HostBounds, Hasher; ADR-007,
ADR-018). Initiality and uniqueness of the catamorphism hold within
each fixed choice of the three axes: for a given
(HostTypes, HostBounds, Hasher) selection, there is exactly one
F-algebra homomorphism from Term to the corresponding carrier. Across
selections, the carriers differ as an indexed family, and the
architecture commits each application’s selection at the application’s
compile time (TC-04). The categorical statement of ADR-018’s capacity
completeness is that the indexing of carriers is total over HostBounds
— every capacity-bounded width that varies along the principal data path
is part of the index.
The substrate-vs-implementor split (ADR-007’s three-position pattern)
extends naturally: uor-foundation defines the signature endofunctor
and the initial algebra; prism declares the bound (the F-algebra
contract any application’s Route MUST satisfy, and the catamorphism
that compiles it); the application author selects the F-algebra by
writing the model. The categorical reading is the deeper expression of
the same pattern that allocates HostTypes/HostBounds/Hasher across
the three crates.
Rejected alternative 1: Continue stating closure (ADR-013) and
zero-cost runtime (TC-01) as separate, independently-derived properties.
Rejected because the architecture’s higher commitments (PrismModel's
monomorphism-via-compilation in ADR-020; the trace’s role as the
anamorphism’s witness; the standard library’s status as canonical UOR
addresses in ADR-017) all rely on initiality of Term against a closed
signature. Re-deriving initiality at every reference site is editorially
costly and obscures the load-bearing structure; stating it once as
ADR-019 lets every later commitment cite it.
Rejected alternative 2: State the categorical structure but apply it only to the term language, leaving the principal data path’s stage transitions and the sealed types' construction discipline outside the categorical reading. Rejected because the stage transitions are the structure of the typed pipeline endofunctor (Datum → Triad → Derivation → FreeRank → Grounded is its forward sequence; the seven sealed types are its fixed points) — distinct from F the signature endofunctor but structurally entangled with it: F structures the term language the catamorphism consumes, and the catamorphism’s image is the pipeline endofunctor’s fixed-point sequence. The sealed types' construction discipline is exactly the categorical statement that the fixed-point inhabitants are the catamorphism’s images. A partial categorical reading would leave the strongest statements (TC-02 sealing, TC-03 single-path) unmoored from the reading that gives them their precise meaning.
Rejected alternative 3: Adopt the categorical reading but call it something other than what it is (e.g., "data flow algebra," "type pipeline structure"). Rejected because the structures are signature endofunctor + initial algebra + catamorphism + anamorphism + fixed point; renaming them would introduce a parallel vocabulary with no compensating clarity, and would prevent the wiki from connecting to the existing literature on free-monad-style program structures. The mathematical names are normative.
ADR-020 — PrismModel is the application author’s contract for declaring a route through the foundation hylomorphism
Status: Accepted.
Context: ADR-019 establishes that a Prism application’s compiled
form is the catamorphism induced by initiality of Term against
prism's declared F-algebra carrier. The structure is correct, but a
developer reading the wiki for the first time and starting to build an
application has no surface that names "the model I am declaring."
Foundation owns the categorical machinery (ADR-019); prism's job is to
surface it as the developer’s contract. Without that contract, the
structure exists but is not actionable: the developer assembles
ConstrainedTypeShape impls, picks substitution-axis selections, and
writes hand-rolled Rust to compose them, with no type system enforcing
that the composition is the unique homomorphism the architecture
demands. Real-world Prism applications observed in the field exhibit
exactly this failure mode: the operations are foundation-vocabulary; the
composition is hand-rolled outside the type system; the categorical
structure (catamorphism + anamorphism + trace as residue object) exists
in the documentation but not in the code.
Decision: prism exposes a public trait PrismModel codifying the
application author’s hylomorphism contract. The trait carries three
associated types — Input, Output, Route — and one method,
forward(input: Input) → Result<Grounded<Output>, PipelineFailure>
(signature aligned with pipeline::run's contract). Input and
Output are ConstrainedTypeShape impls declared in foundation
vocabulary. Route is a type-level witness of the value-level term tree
that maps Input to Output. The witness is emitted by a prism-side
proc-macro prism_model! (per ADR-022 D3; emitted from
uor-foundation-sdk per ADR-015’s bundling) from the application
author’s syntactic Route declaration; the macro emits both the
type-level witness (which the application’s Route associated type
aliases) and the value-level TermArena slice pipeline::run consumes.
The witness’s nodes range over the full Term enum (the twenty-one
variants in foundation::enforcement::Term: nine from ADR-022 D3 —
Literal, Variable, Application, Lift, Project, Match,
Recurse, Unfold, Try — plus AxisInvocation added in ADR-029 as
HasherProjection and generalized per ADR-030, plus ProjectField per
ADR-033, plus FirstAdmit per ADR-034, plus the nine ψ-chain variants
per ADR-035: Nerve, ChainComplex, HomologyGroups, Betti,
CochainComplex, CohomologyGroups, PostnikovTower,
HomotopyGroups, KInvariants); the value-level slice is the arena
form pipeline::run traverses. The bound that any Route MUST satisfy
is closure under foundation vocabulary, expressed at the type level
by the FoundationClosed trait prism declares. The trait carries one
method, fn arena_slice() -> &'static [Term], that returns the route’s
term-tree slice (the value-level state the macro emits alongside the
impl); pipeline::run_route reads
<M::Route as FoundationClosed>::arena_slice() to populate the
CompileUnit's root_term. The route-emitting macro emits an impl of
FoundationClosed for the witness it generates if and only if every
node in the witnessed tree is a foundation-vocabulary item; a witness
for a tree that imports a function outside foundation vocabulary
receives no impl, and the application fails to compile with an
unsatisfied bound on Route. The check is performed at the
application’s compile time by UORassembly (TC-04, ADR-006). forward is
the catamorphism into pipeline::run's runtime carrier; the application
author does not write forward's body — prism derives it from the
model’s Route declaration via initiality of Term (ADR-019). The
trait codifies a hylomorphism-with-verifiable-round-trip structure
(catamorphism from Input to
Result<Grounded<Output>, PipelineFailure>, recoverable anamorphism
through the trace to Certified<GroundingCertificate>); it does not
realize a standard categorical-optic shape, and the trait’s name derives
from the implementation crate’s name, not from the categorical Prism
optic.
Route’s level: Route is exposed as an associated type, not a
value-level constant. The associated-type form admits a trait-bound
enforcement of closure under foundation vocabulary (the marker trait the
route-emitting macro produces), which pipeline::run's contract requires
at the application’s compile time. A value-level alternative (e.g.,
const ROUTE: &'static [Term]) is feasible but would require a separate
const fn validator or build script to enforce closure, since Rust’s
const-context evaluation does not admit trait-bound checks on values.
The "type carries the proof, value carries the data" split — the
type-level witness proves closure; the value-level arena carries the
term tree — is the canonical Rust idiom for compile-time-checked
structured data and is what this trait adopts.
The framing exposed at the developer’s reading surface is Real-Time
Inference: input features come in, types route them to output labels,
the pipeline is the route’s compiled form, runtime cost is the cost of
executing the route. The framing the architecture supports underneath —
the route is an F-algebra, the compilation is the unique homomorphism
induced by initiality, the runtime form is monomorphized native code —
lives in foundation’s chapter (section 8, Foundation as a Signature
Category). The two framings are the same statement at two levels of
abstraction; PrismModel's public-API documentation states the
developer-facing one and cross-references the categorical one.
Consequences: An application author who implements PrismModel for
their application receives, by virtue of the trait’s compile-time
enforcement, the following without further action: closure of every
operation under foundation vocabulary (the Route bound checks it);
zero-cost runtime (the catamorphism is monomorphized at compile time per
TC-01 and ADR-019); seal coverage of the output (the catamorphism’s
image is Grounded<Output>, sealed via the prism seal regime per
TC-02 and ADR-011); a Trace recoverable from the
Grounded<Output> via derivation().replay() (the anamorphism’s
witness object, per ADR-019); and a Certified<GroundingCertificate>
reachable from the trace via prism-verify (the round-trip property,
per TC-05 and Scenario 2). The trait surfaces the categorical structure
as a Rust contract; the type system is what the developer writes
against, and the architectural commitments hold by the trait’s
enforcement.
The trait is parameterized by
PrismModel<H: HostTypes, B: HostBounds, A: AxisTuple + Hasher, R: ResolverTuple = NullResolverTuple>
per ADR-030 + ADR-036; the application author selects all four
parameters at the impl site, and each impl is one member of the
H-indexed family of carriers (ADR-019; ADR-022 D4). The
FoundationClosed marker uses the standard ecosystem seal idiom — a
#[doc(hidden)] pub mod __sdk_seal { pub trait Sealed {} } in
prism that the prism_model! proc-macro can name when emitting impls
(ADR-022 D1). The catamorphism’s call-site is
prism::pipeline::run_route<H, B, A, Self, R>(input, &resolvers), which
the forward body invokes after the macro emits it; the lower-level
pipeline::run API remains for callers that construct the CompileUnit
themselves (ADR-022 D5).
The Output associated type is declared through the output_shape! SDK
macro for shape-rich outputs (per ADR-027), with ConstrainedTypeInput
retained as the foundation-sanctioned identity for models that declare
no transformation. The returned Grounded<Output> carries the route’s
evaluation result as a value payload accessible via output_bytes()
(per ADR-028); the metadata fingerprint and unit_address remain as
typed-iso path attestation. The route’s evaluation is the catamorphism’s
structural fold per ADR-029, with per-variant fold-rules across
twenty-one Term variants, including the nine ψ-chain variants whose
resolver-bound fold-rules consult the ResolverTuple per ADR-036.
Together, ADR-020 + ADR-022 + ADR-027 + ADR-028 + ADR-029 + ADR-030 +
ADR-033 + ADR-034 + ADR-035 + ADR-036 + ADR-041 + ADR-042 + ADR-043 +
ADR-044 + ADR-045 + ADR-046 + ADR-047 + ADR-048 + ADR-049 + ADR-050 +
ADR-051 + ADR-052 + ADR-053 + ADR-054 + ADR-055 + ADR-056 fully specify
the typed-iso surface end-to-end: the developer declares Input, Output,
Route, and optional C: TypedCommitment per ADR-048; the macro emits
the witness, the seal, and the impls per ADR-022 + ADR-027 + ADR-044;
the closure-body grammar G1–G29 is rejected per ADR-035’s ψ-residuals
discipline at proc-macro expansion (ADR-046 records the discipline-scope
boundary); the catamorphism evaluates the route to produce the output
value (consulting the ResolverTuple for resolver-bound ψ-Term variants);
resolver impls realize the typed-carrier transform per ADR-043’s
iterative-resolution discipline (FreeRank protocol,
convergence/exhaustion termination, impossibility-witness emission); the
κ-label is consulted by C::evaluate per ADR-048 for the
typed-bandwidth admission decision before the catamorphism’s success
envelope is sealed; the canonical hash axis selection per ADR-030
qualifies against the σ-Projection Hardening Principle (U1–U6) per
ADR-047, with empirical witness through axis::cryptanalyze per
ADR-049; UOR observables consumed by SingletonCommitment<P> predicates
are foundation-declared typed surfaces per ADR-049; the Grounded carries
both the path attestation and the value (with tag::<NewTag>()
re-tagging affordance per ADR-045); typed verdict-envelope accessors per
ADR-042 expose the inhabitance certificate / impossibility certificate
surfaces.
A "compiled prism application is a monomorphism via the catamorphism
induced by initiality of Term, with the trace as residue object
enabling the recoverable backward direction" reads, under this trait,
as: forward is the unique map induced by the initial F-algebra into
the target machine-code carrier (mono in the embedding category, by the
seal-regime + content-addressing argument in section 8, Compilation as
Monomorphism); the Input → Result<Grounded<Output>, PipelineFailure>
direction is the catamorphism; the recoverable
Grounded<Output> → Trace → Certified<GroundingCertificate> direction
is the anamorphism; the trace is the residue object linking the two. The
"two typed parameters" are Input and Output; the "monomorphism" is
forward after monomorphization; the verifiable round-trip is the
PrismModel declaration as a whole. This is a hylomorphism with
verifiable round-trip, not a categorical iso (the backward direction
certifies provenance rather than inverting the forward map; section 8,
Anamorphism).
Rejected alternative 1: Document the categorical structure without
surfacing a trait. Rejected because documentation alone does not enforce
closure: a developer can read the wiki, understand the hylomorphism
framing, and still write a hand-rolled Rust composition that escapes
foundation vocabulary. The bound on Route is the load-bearing
enforcement; without it, the architecture’s commitments hold by author
discipline rather than by type-system check. ADR-006 (bilateral
compile-time UORassembly) requires that the contract be enforceable
through Rust’s type system; PrismModel's Route bound is the
type-level expression of that enforcement for the model declaration as a
whole.
Rejected alternative 2: Surface the trait under a different name
than PrismModel (e.g., Prism, Model, Inference, Route).
Rejected for Prism because prism is already the crate name —
overloading the bare name would conflate the implementation crate and
the trait. (The trait does not realize the categorical Prism optic;
the trait’s name derives from the implementation crate’s name; section
8, Anamorphism.) Rejected for Model alone because the term carries
machine-learning connotations (parameterized weights, training) that
conflict with the architecture’s compile-time-determined,
zero-cost-runtime commitments — a PrismModel has no learned
parameters; its behavior is type-determined. Rejected for Inference
because the trait names what is declared (the model) rather than
what happens to declarations (inference); inference is the runtime
behavior of a forward call. Rejected for Route because Route is
one of the trait’s associated types, not the trait itself; the trait
carries the hylomorphism, of which the route is one component.
Rejected alternative 3: Make PrismModel a type alias rather than a
trait. Rejected because a type alias cannot carry an associated-type
bound that enforces algebraic closure on Route; the closure check is
the load-bearing enforcement, and Rust’s type aliases do not support
trait-level bounds on their parameters in a way the application author’s
code is monomorphized against. The trait form admits the bound; the
alias form does not. (A type alias for the canonical instantiation
pattern — e.g., type SimpleModel<I, O, R> = … over PrismModel — may
be added as ergonomic sugar later without superseding the trait.)
Status: Accepted.
Context: ADR-019 + ADR-020 reframed Prism’s architectural
commitments in categorical vocabulary: the catamorphism pipeline::run
produces sealed Grounded<T> from foundation-vocabulary routes; the
anamorphism prism-verify::certify_from_trace produces
Certified<GroundingCertificate> by walking the trace; together they
form a hylomorphism with verifiable round-trip witnessed by the trace
(section 8, Foundation as a Signature Category; ADR-020). The
verification + validation framework Prism is conformed to needs to align
with this framing rather than treating V&V as a parallel concern.
The six-layer V&V framework Prism adopts — ASME V&V 40 (context of use, intended-use rigor budget), NASA-STD-7009A (model M&S credibility), Oberkampf-Roy (code verification), DO-330 (tool qualification), OntoClean + OOPS! (ontology QA), IEEE 1012 (V&V plan structure with integrity-level grading) — leaves four decisions open at framework selection: (1) the Context of Use (CoU); (2) the external referent for validation; (3) the V/IV&V independence model; (4) the IEEE 1012 integrity level (IL). The ADR-019/020 reframing sharpens each of the four; this ADR records the resolutions.
Decision: The four V&V decisions resolve as follows under the hylomorphism framing.
Decision 1 — Context of Use: The CoU is "UOR Framework as a production substrate for compiled prism applications, with the catamorphism + anamorphism pair providing internal round-trip verification." The published UOR Foundation mathematics is in scope as the validation referent (Decision 2), not as a separate CoU. ADR-019’s normative statement — "any Prism implementation that admits a route, sealed-type construction, or trace replay outside this structure is non-conforming" — is a CoU statement in V&V 40 vocabulary: it specifies what the framework is for (applications) and the conformance bar (the structure).
Decision 2 — External referent for validation: Validation is
stratified, not substituted. The external referent is the published UOR
Foundation mathematics (ring on Z/(2^n)Z, Witt-tower theory): it
governs spec faithfulness — whether the wiki’s src/ and the
implementation faithfully encode the mathematics, verified by
Oberkampf-Roy code-verification activities plus the Lean 4 corpus’s
zero-sorry proofs of mathematical identities. The internal referent is
the trace as anamorphism witness: it governs implementation
reproducibility — every Grounded<T> produced by the catamorphism
MUST replay through prism-verify to a
Certified<GroundingCertificate>. The trace-replay round-trip is
elevated to a first-class IEEE 1012 V&V activity, not a behavior test
fixture: the reading is normative — round-trip closure is an
architectural property the implementation MUST satisfy.
Decision 3 — Independence (V vs IV&V): Independence is structural
and built-in. The hylomorphism’s two halves divide between two
distinct agents: prism is the V agent (the catamorphism produces
Grounded from foundation-vocabulary routes; correctness measured
against term-language semantics); prism-verify is the IV&V agent (the
anamorphism produces Certified by walking the trace, without
re-evaluating the application author’s deciders or invoking any
cryptographic hasher beyond identifier matching, per TC-05). The trace
is the artifact crossing the V/IV&V boundary. This is
independence-by-construction — the verifier cannot cheat by re-running
the catamorphism, because the anamorphism’s contract is to walk the
trace structurally. ADR-016’s "prism’s pipeline is the only sanctioned
caller of the mint primitives" + ADR-019’s normative split together
establish that the catamorphism and anamorphism are distinct surfaces;
IEEE 1012’s technical-independence dimension is satisfied structurally.
External IV&V (a third-party assurance organization re-implementing
prism-verify against the trace and checking the round-trip
independently) is additional, not substitute — the architecture’s
own split establishes the property.
Decision 4 — Integrity Level: A single global IL is inappropriate; the V&V plan parameterizes deliverables by IL per consumer class. The PRISM-substrate floor is IL 3. Justification: TC-01’s compile-time-determined zero-cost-runtime commitment plus the seal-regime + content-addressing embedding property (section 8, Compilation as Monomorphism) lower the dynamic-validation burden compared to systems that reach IL 3 through dynamic monitoring. Consumer-class bands:
| Consumer class | Example | IL band |
|---|---|---|
| Entertainment / educational | Toy demonstrators | IL 1 |
| Cryptographic-search consumers | High-cardinality bounded first-admission search applications | IL 3 |
| Cryptographic-substrate | Fully-homomorphic-encryption integrations | IL 3-4 |
| Safety-of-life | Not currently in scope | IL 4 |
IL 3 deliverable set: V&V plan + concept-of-operations document (IEEE
1012 §5); requirements traceability matrix from src/ to source;
code-verification artifacts (Oberkampf-Roy + the Lean 4 corpus); the
round-trip property as a normative behavior (Decision 2); tool
qualification for the codegen pipeline (DO-330). IL 4 adds: independent
assurance review, formal arguments per GSN Community Standard v3, and
explicit hazard analysis per the consumer’s safety-of-life requirements.
Consequences: V&V activities Prism’s wiki commits to executing are
now grounded in named architectural mechanisms rather than restated as
parallel quality concerns. The wiki’s existing V&V apparatus already
realizes much of the structure: the eight wiki validators (V1–V8) are
the structural-conformance activities; the Lean 4 corpus is the
formal-spec verification; cargo test + the conformance suite are the
code-verification + behavioral-test activities; prism-verify is the
structural IV&V agent; the trace is the witness object the V/IV&V
boundary uses. ADR-021 names these as the V&V framework’s instantiation
rather than introducing new mechanisms. Future V&V plan documents
(chapter 7, technical lifecycle Verification + Validation sections;
potentially a new vv/ directory) author against ADR-021’s resolved
decisions rather than re-litigating them.
The IL parameterization means a single Prism deliverable is not "IL N" globally; consumer-class-specific assurance arguments cite the relevant IL band for their context. A cryptographic-search consumer’s V&V plan cites IL 3; an FHE consumer’s V&V plan cites IL 3-4 with the cryptographic-substrate justification; a hypothetical safety-of-life consumer would have to add explicit hazard analysis and independent assurance review per IL 4 themselves.
Rejected alternative 1: Treat the published UOR Foundation mathematics as the sole CoU, with the production-substrate framing as a downstream concern. Rejected because the architecture’s catamorphism + anamorphism + sealed types are realized in the production substrate, not in the foundational mathematics; conformance is checked at the substrate level, and that’s what the CoU statement should name. The mathematics remains the validation referent (Decision 2).
Rejected alternative 2: Single-referent validation against the published mathematics, with the trace-replay round-trip captured only as a behavior-test fixture in the conformance suite. Rejected because the round-trip is an architectural property normatively committed by ADR-019 (initiality + uniqueness) and by TC-05 (replayability without re-evaluating deciders); demoting it to a test fixture obscures that it carries the architecture’s own internal V&V mechanism, distinct from external validation against the mathematics.
Rejected alternative 3: Engage an external IV&V organization as the
sole independence mechanism, treating prism-verify's replay surface as
an internal verification convenience. Rejected because the
catamorphism + anamorphism split is the V/IV&V split structurally —
the trace is the artifact crossing the boundary, and prism-verify's
contract precludes it from re-running the catamorphism. External IV&V
remains valuable as an additional check (a third party re-implementing
prism-verify against the trace strengthens the architectural claim)
but is not the load-bearing independence mechanism.
Rejected alternative 4: Specify a single global IL for the framework. Rejected because the framework spans consumer classes from entertainment-grade demonstrators (IL 1) to safety-of-life systems (IL 4); a single IL would either over-burden low-criticality consumers with unwarranted assurance overhead or under-specify high-criticality consumers' rigor requirements. The per-consumer-class parameterization is the principled position.
Status: Accepted.
Context: ADR-020 specifies the PrismModel contract — Input,
Output, Route associated types;
forward(input) → Result<Grounded<Output>, PipelineFailure> method;
Route carries a FoundationClosed marker bound checked at the
application’s compile time; the route-emitting proc-macro
(prism_model!) generates the type-level witness and the value-level
TermArena slice. Five implementation-surface concerns the ADR-020 text
either leaves to the implementation or contradicts the foundation source
require explicit architectural resolution before the implementation can
land. Two are contradictions (the foundation source as currently written
cannot satisfy ADR-020’s commitments); three are gaps (the architectural
decision is currently delegated to the implementation by silence).
Decision: Five resolutions, each binding on the foundation/prism implementation.
D1 — FoundationClosed seal mechanism: The seal is implemented by
the standard ecosystem idiom for cross-crate-extensible-but-controlled
traits: a #[doc(hidden)] pub mod __sdk_seal { pub trait Sealed {} }
in prism, with FoundationClosed declaring Sealed as a supertrait.
The module is pub (so the proc-macro crate can name
prism::__sdk_seal::Sealed in the impls it emits) but #[doc(hidden)]
(so it does not appear in rustdoc and is not part of the
publicly-discoverable API surface). The proc-macro crate emits impl
prism::__sdk_seal::Sealed for <RouteWitness> alongside
impl prism::FoundationClosed for <RouteWitness>. External crates that
name __sdk_seal::Sealed are technically permitted by Rust’s visibility
rules but architecturally non-conforming; the doc-hidden +
naming-convention pair is the ecosystem-standard signal of "for the SDK
only." A purely pub(crate) seal would prevent the SDK proc-macro from
emitting impls (which is the contradiction this resolution closes); a
fully-public seal would lose the architectural commitment that only the
SDK macro emits the impl.
D2 — TermArena const construction: Foundation adds a const
constructor to the TermArena public API:
impl TermArena {
pub const fn from_slice(slice: &'static [Term]) -> Self { /* ... */ }
}The prism_model! macro emits a const ROUTE_TERMS_FOR_<MODEL>:
&'static [Term] = &[Term::…, …] containing the term tree, and the
route witness’s FoundationClosed::arena_slice() (D6 below) returns it.
The catamorphism (pipeline::run_route, D5 below) consumes &'static
[Term] via arena_slice(). The TermArena<CAP>::from_slice const
constructor remains available for callers that explicitly want the
TermArena form (e.g., test harnesses that need the arena’s
as_slice() accessor or its capacity tracking); the macro’s own
emission uses the bare slice to avoid threading the arena’s CAP
const-generic through the FoundationClosed trait surface. On stable
Rust without generic_const_exprs, the slice form is the architectural
equivalent of the &'static TermArena<CAP> form: both expose the term
tree as a static, fully-const value the catamorphism reads at the
application’s compile time. The existing &mut self push API on
TermArena is preserved for runtime constructions; from_slice is
purely additive.
D3 — Route declaration syntax: The prism_model! macro accepts a
closure-bodied route function inside the model’s declaration:
prism_model! {
pub struct MyModel;
impl PrismModel<MyHostTypes, MyHostBounds, MyAxisTuple> for MyModel {
type Input = MyInputShape;
type Output = MyOutputShape;
fn route(input: Self::Input) -> Self::Output {
// closure body — Rust expression syntax, parsed by the
// macro into a Term tree at expansion time.
hash(concat(input.left, input.right))
}
}
}The macro parses the route function’s body as a Rust expression tree;
every function call is resolved against the foundation-vocabulary names
the macro recognizes (the PrimitiveOp discriminants and the
Term::Application shapes). A call to a function the macro does not
recognize is a closure-violation; the macro emits a compile error
pointing at the offending call site rather than emitting an unsealed
impl. The closure body’s Rust syntax is the grammar enumerated below
(G1–G11). Each form names the accepted Rust syntax, the emitted Term
variant (or binding-table action), and any per-form restrictions. A Rust
construct outside G1–G11 is a closure violation: the macro emits a
compile error pointing at the offending span with text identifying the
rejected construct and the G1–G11 enumeration as the recognized set. The
closure body never executes as Rust at runtime; it is consumed at macro
time, mapped to the term-tree representation and the binding table, and
the macro emits the term tree (as the value the route witness’s
arena_slice() returns), the binding-table edits, and the
closure-checked FoundationClosed impl together.
Two reserved name-index sentinels appear in the grammar:
name_index = 0 is reserved for the route’s input parameter (G2);
name_index = u32::MAX is reserved for the wildcard arm in match (G6)
and for the default-propagation handler in try (G9). All other
name_index values are assigned by the macro in declaration order to
let-introduced bindings and to the closure parameters of recurse and
unfold (G7, G8, G10).
G1 — Integer literals. Rust syntax: any integer literal parseable as
u64. Emitted:
Term::Literal { value: <parsed>, level: WittLevel::W8 }. The Witt
level is fixed at W8 for the literal path; routes that require wider
literals use lift::<W{n}> (G4) to widen explicitly.
G2 — The input parameter. Rust syntax: the bare identifier input
(the route function’s sole parameter, by macro convention). Emitted:
Term::Variable { name_index: 0 }.
G3 — PrimitiveOp operator forms. Two Rust-syntactic surface forms
admit PrimitiveOp discriminants in closure bodies; both lower to
Term::Application { operator: PrimitiveOp::<…>, args: TermList { start, len } }
with args a contiguous block in the arena.
G3a — identifier-call form. A bare-identifier call to a lowercase
PrimitiveOp name. The PrimitiveOp catalog at any committed snapshot
enumerates the admissible identifiers; foundation’s canonical
PrimitiveOp enum at the snapshot is the authority. Foundation 0.3.6’s
catalog admits add, sub, mul, xor, and, or (binary
arithmetic and bitwise); neg, bnot, succ, pred (unary arithmetic
and bitwise); le, lt, ge, gt (binary byte-level comparison,
returning Literal(1) on true, Literal(0) on false); concat (binary
byte-sequence concatenation). The catalog extends through ADR-013’s
substrate-amendment-via-foundation rule (TR-08).
G3b — binary-operator form. A binary expression whose operator is
one of Rust’s recognized binary operators with a corresponding
PrimitiveOp discriminant: + (Add), - (Sub), * (Mul), ^ (Xor),
& (And), | (Or), ⇐ (Le), < (Lt), >= (Ge), > (Gt). Each
binary-operator surface form is architecturally equivalent to the
corresponding identifier-call form — both lower to identical
Term::Application emissions with identical args ordering — and the
application author selects the surface form that reads most naturally
for the operation. Unary PrimitiveOp discriminants (Neg, Bnot, Succ,
Pred) and byte-packing (Concat) admit only the identifier-call form per
G3a.
Arity mismatches in G3a (wrong number of arguments to the identifier-call) and operator-mismatches in G3b (binary operator without corresponding PrimitiveOp) are closure violations surfaced at proc-macro expansion time pointing at the offending span.
G4 — Lift (canonical injection). Rust syntax:
lift::<W{n}>(operand_expr) where n ∈ {16, 24, 32} names the target
Witt level. Emitted:
Term::Lift { operand_index: <operand_term_idx>, target: WittLevel::W{n} }.
The target level MUST be strictly greater than the operand’s level
(lossless injection); a downward lift is a closure violation. lift
is a reserved macro-vocabulary identifier — foundation does not export a
Rust function lift, and the macro consumes the form.
G5 — Project (canonical surjection). Rust syntax:
project::<W{n}>(operand_expr) where n ∈ {8, 16, 24} names the target
Witt level. Emitted:
Term::Project { operand_index: <operand_term_idx>, target: WittLevel::W{n} }.
The target level MUST be strictly less than the operand’s level (lossy
surjection); an upward project is a closure violation. project is a
reserved macro-vocabulary identifier (parallel to lift).
G6 — match. Rust syntax: match <scrutinee_expr> { <pat1> =>
<arm_expr1>, <pat2> => <arm_expr2>, …, _ => <default_expr> }.
Emitted: Term::Match { scrutinee_index: <scrutinee_term_idx>, arms:
TermList { start, len } } where arms references a contiguous block of
2 * num_arms terms in the arena, alternating pattern terms and
arm-body terms. Accepted patterns: integer literal patterns (mapped to
Term::Literal { value, level: WittLevel::W8 }) and the wildcard _
(mapped to Term::Variable { name_index: u32::MAX } as the wildcard
sentinel). Identifier patterns, tuple patterns, struct patterns, enum
patterns, reference patterns, and range patterns are closure violations.
The match MUST end with a wildcard arm (_ => <default_expr>);
non-exhaustive matches are closure violations. The pattern-arm
alternation in the arms slice is the convention foundation’s
catamorphism reads to dispatch.
G7 — Recurse (well-founded recursion). Rust syntax: the
macro-recognized form
recurse(<measure_expr>, <base_expr>, |<self_ident>[, <idx_ident>]| <step_expr>)
where <measure_expr> is the descent measure (a term evaluating to a
non-negative integer that decreases each step), <base_expr> is the
base case (taken when the measure reaches zero), and <step_expr> is
the recursive case with <self_ident> bound to the recursive-call
placeholder and (optionally) <idx_ident> bound to the current
iteration counter (the descending measure value at this step) per
ADR-034. Emitted:
Term::Recurse { measure_index: <measure_term_idx>, base_index: <base_term_idx>, step_index: <step_term_idx> }.
The SDK proc-macro lowers <self_ident> references inside the step body
directly to
Term::Variable { name_index: RECURSE_PLACEHOLDER_NAME_INDEX } and
(when present) lowers <idx_ident> references directly to
Term::Variable { name_index: RECURSE_IDX_NAME_INDEX } per ADR-034 —
both foundation-fixed name indices are the SDK’s canonical lowering
targets for these bindings, not fresh per-invocation indices.
Foundation’s catamorphism resolves these Variable references within the
enclosing Term::Recurse's step subtree to the recursive call (binding
RECURSE_PLACEHOLDER_NAME_INDEX per ADR-029) and the current iteration
counter (binding RECURSE_IDX_NAME_INDEX per ADR-034) respectively.
recurse is a reserved macro-vocabulary identifier.
G8 — Unfold (anamorphism). Rust syntax:
unfold(<seed_expr>, |<state_ident>| <step_expr>) where <seed_expr>
produces the initial state and <step_expr> is the per-step
transformation with <state_ident> bound to the current state. Emitted:
Term::Unfold { seed_index: <seed_term_idx>, step_index: <step_term_idx> }.
The <state_ident> parameter is assigned a fresh name_index (parallel
to G7’s <self_ident> mechanism). unfold is a reserved
macro-vocabulary identifier.
G9 — Try (failure-promote). Rust syntax: the postfix ? operator
on a sub-expression, <expr>?. Emitted:
Term::Try { body_index: <expr_term_idx>, handler_index: u32::MAX }
where u32::MAX is the default-propagation sentinel: foundation’s
catamorphism interprets handler_index = u32::MAX as "propagate the
failure unchanged through PipelineFailure." The try { … } block
syntax (unstable Rust) is not in scope; only the ? postfix form. The
sentinel-based handler representation leaves the alternative encoding (a
real arena index in handler_index) syntactically reachable for
foundation’s carrier to interpret, so the encoding does not foreclose
richer handling architectures.
G10 — let bindings. Rust syntax:
let <ident> = <value_expr>; <body_expr> inside the closure body. The
macro assigns <ident> a fresh name_index (the next available;
indices 1, 2, … in declaration order, with index 0 reserved for input
per G2 and u32::MAX reserved per G6 / G9). Emitted: the
<value_expr>'s term tree is appended to the arena; a binding-table
entry is registered associating the new name_index with the value’s
term-tree root index; references to <ident> inside <body_expr> emit
Term::Variable { name_index: <assigned> }. The let itself does not
emit a Term variant; it modifies the binding-table mapping the macro
assembles. Shadowing (declaring two lets with the same identifier in
the same scope) is a closure violation. Sequential lets in a block are
accepted; the bindings stack with each let's <ident> in scope
through the remainder of the block.
G11 — Block expressions and parentheses (transparent grouping). Rust
syntax: { <stmts>; <tail_expr> } and (<expr>). The macro descends
into them without emitting a Term variant. Block expressions MUST end
with an expression statement (no trailing ;); a trailing-; block is
a closure violation ("expected an expression, got a statement-terminated
block"). Parens are pure grouping with no semantic content.
Any Rust construct not enumerated in G1–G11 — including but not limited
to: closures, if/else, loop/while/for, return, references
and dereferences, method calls, field access, struct literals, array
literals, tuple literals, type ascription, casts, range expressions,
unsafe blocks, and any function call to an identifier not enumerated in
G3, G4, G5, G7, or G8 — is a closure violation. The error message text
identifies the rejected construct and the G1–G11 enumeration as the
recognized set.
The closure-body syntax was chosen over the alternatives — explicit
Term::Application { … } literal arena (verbose, alien to Rust
developers), builder-pattern (route().then(…).then(…), ergonomic but
obscures the term-tree structure), and a custom DSL (cognitively
expensive, requires its own grammar) — because it is the maximally
Rust-native form: developers who can write Rust expressions can declare
routes; closure-violations are caught at compile time pointing at the
offending span; the macro’s input grammar is documented as the G1–G11
subset of Rust expression syntax above. Five reserved macro-vocabulary
identifiers (lift, project, recurse, unfold, plus the
route-function-name route itself) are the only departures from the
"any Rust function" pattern: foundation does not export Rust functions
with these names, and the macro consumes them as syntactic forms.
D4 — Substitution-axis selection at the model declaration: The
PrismModel trait is parameterized by the three substitution axes plus
the ResolverTuple substrate parameter per ADR-036, not by adding
associated types. The A position carries the canonical-hash-axis bound
(A: AxisTuple + Hasher) so axis methods like
<A as Hasher>::initial() are reachable type-associatedly; R defaults
to NullResolverTuple so models that emit no resolver-bound ψ-Term
variants per ADR-035 can omit the parameter at the impl site:
pub trait PrismModel<H: HostTypes, B: HostBounds, A: AxisTuple + Hasher, R: ResolverTuple = NullResolverTuple>
where Self: __sdk_seal::Sealed {
type Input: ConstrainedTypeShape + IntoBindingValue;
type Output: ConstrainedTypeShape + GroundedShape + IntoBindingValue;
type Route: FoundationClosed;
fn forward(input: Self::Input) -> Result<Grounded<Self::Output>, PipelineFailure>;
}// `ConstrainedTypeShape` (declared elsewhere) carries `CYCLE_SIZE: u64`
// per ADR-032, used by the SDK proc-macro for `first_admit`'s domain
// cardinality emission per ADR-026 G16. Foundation defines fixed name
// indices `RECURSE_PLACEHOLDER_NAME_INDEX`, `RECURSE_IDX_NAME_INDEX`
// (per ADR-034), `UNFOLD_PLACEHOLDER_NAME_INDEX`, and
// `FIRST_ADMIT_IDX_NAME_INDEX` (per ADR-034) for binding the iteration
// and recursion placeholders the catamorphism's per-variant fold-rules
// resolve at evaluation time. The PrismModel trait has four substrate
// parameters per ADR-030 + ADR-036:
// - `H: HostTypes` (host-platform witness type per ADR-022 D5),
// - `B: HostBounds` (host-platform capacity bounds per ADR-022 D5),
// - `A: AxisTuple + Hasher` (substitution-axis tuple with the
// canonical hash axis bound per ADR-030),
// - `R: ResolverTuple` (resolver tuple per ADR-036; defaults to
// `NullResolverTuple` so models that emit no resolver-bound
// ψ-Term variants per ADR-035 can omit the parameter).
// The catamorphism's evaluation environment threads `R` as a value
// reference and `A`/`H`/`B` as type parameters; ψ-Term variants per
// ADR-035 consult `R` at evaluation time for per-value content
// provision, and the canonical hash axis is invoked through
// `<A as Hasher>::initial()` per ADR-022 D5.The model author selects the axes and the resolver tuple at the impl
site:
impl PrismModel<DefaultHostTypes, MyHostBounds, (MyHashAxisImpl,), MyApplicationResolvers<MyHashAxisImpl>> for MyModel { … }
— the third position is now an AxisTuple per ADR-030 (with single-axis
selections written as a 1-tuple, e.g., a single HashAxis impl from
prism-crypto for content-addressing routes; multi-axis tuples for
cross-domain models), and the fourth position is a ResolverTuple per
ADR-036 (declared via the resolver! SDK macro and carrying per-value
content for resolver-bound ψ-Term variants per ADR-035). The trait
itself stays at three associated types (Input, Output, Route),
preserving ADR-020’s contract surface. The parameter-as-trait-position
form expresses the H-indexed family (ADR-019, Consequences)
directly: each impl block names the family member. An application that
uses two distinct axis selections (or two distinct resolver selections)
has two impl PrismModel<…> for MyModel blocks (one per selection);
each is a distinct member of the indexed family and produces its own
monomorphized forward.
The axis-as-trait-parameter form was chosen over the alternatives: adding three more associated types (would inflate the trait’s surface to six associated types, harder to teach, conflates "what the model is" with "where it runs"); macro parameters (would push axis selection out of the type system into the macro grammar, breaking the type-system-as-enforcement story); default-only convention (would prevent applications from selecting non-default axes, contradicting ADR-007’s substitution discipline).
D5 — Catamorphism call-site: Foundation exposes a higher-level entry
point that takes the route directly and constructs the CompileUnit
internally:
pub fn run_route<H, B, A, M, R>(
input: M::Input,
resolvers: &R,
) -> Result<Grounded<M::Output>, PipelineFailure>
where
H: HostTypes,
B: HostBounds,
A: AxisTuple + Hasher,
M: PrismModel<H, B, A, R>,
R: ResolverTuple
+ HasNerveResolver<A>
+ HasChainComplexResolver<A>
+ HasHomologyGroupResolver<A>
+ HasCochainComplexResolver<A>
+ HasCohomologyGroupResolver<A>
+ HasPostnikovResolver<A>
+ HasHomotopyGroupResolver<A>
+ HasKInvariantResolver<A>,
<M as PrismModel<H, B, A, R>>::Route: AsRef<&'static TermArena>,The prism_model!-emitted forward body calls
prism::pipeline::run_route::<H, B, A, Self, R>(input, &resolvers) per
ADR-036. run_route constructs the Validated<CompileUnit, FinalPhase>
from the model’s Route (whose &'static [Term] arena slice is read via
<M::Route as FoundationClosed>::arena_slice(), per D6) plus the input
value (serialized to a transient BindingEntry via the
IntoBindingValue trait, per ADR-023), threads the resolvers value
reference through the catamorphism’s evaluation environment, and invokes
pipeline::run against it. The signature takes no axes value
parameter — axis methods are type-associated and invoked through
<A as Hasher>::initial() per D4’s A: AxisTuple + Hasher bound; only
the resolver tuple flows as a value reference. The lower-level
pipeline::run<T, P, H>(unit: Validated<CompileUnit, P>) API remains
for callers that want to construct the CompileUnit themselves (e.g.,
test harnesses, conformance suites, alternative SDK surfaces); the
higher-level run_route is what PrismModel::forward calls and what
the wiki commits to as the canonical model-execution surface.
The higher-level entry point was chosen over inline CompileUnit
construction in the macro (would require the macro to know foundation’s
CompileUnit internals, coupling the SDK macro to the substrate’s
private structure) and over exposing only pipeline::run (would force
every model author to construct CompileUnit themselves, surfacing a
stage-transition implementation detail at the application layer). The
higher-level surface keeps the architectural layer correct: the
substrate exposes run_route; the SDK’s macro emits forward body that
calls run_route; the application author writes model.forward(input).
D6 — FoundationClosed trait surface: The trait’s full surface is:
pub trait FoundationClosed: __sdk_seal::Sealed {
fn arena_slice() -> &'static [Term];
}arena_slice() returns the route witness’s term-tree slice — the
value-level term arena the prism_model! macro emits alongside the
impl. pipeline::run_route reads it via
<M::Route as FoundationClosed>::arena_slice() to populate the
CompileUnit's root_term (D5). The foundation-sanctioned identity
route (ConstrainedTypeInput) implements the method returning &[] —
the empty term tree, no transformation. The route-emitting macro emits
an impl returning the parsed closure body’s term tree as a const
static slice (D3).
The method-on-trait form was chosen over alternatives: an associated
constant (const ARENA: &'static [Term]) would carry the same
information but const-trait-items have surface-area issues with Rust’s
const-evaluation ordering; a separate trait (RouteTerms carrying the
method, with FoundationClosed as a pure marker) would split the
closure-witness role across two traits without enabling any additional
checks; an associated type with a fixed-capacity TermArena would
require trait-level const generics (rejected per D2). The single trait
with one method is the surface that makes
run_route::<…, M>(input, &axes, &resolvers) resolve at the
application’s compile time without further infrastructure.
Consequences: Together the six resolutions specify enough of the
implementation surface that the foundation + prism + prism_model!
proc-macro can be built without further architectural decision. The
trait’s contract (ADR-020) plus the parameter parameterization (D4) plus
the call-site (D5) plus the syntax (D3) plus the seal (D1) plus the
const-construction primitive (D2) plus the FoundationClosed surface
(D6) collectively determine: what the trait surface is, how the author
declares a model, how the macro generates code, what the macro’s emitted
impls look like, what the catamorphism’s entry point is, how the closure
check is enforced at compile time, and how the catamorphism reads the
route’s term tree at runtime.
The [H: HostTypes, B: HostBounds, A: AxisTuple, R: ResolverTuple]
parameterization on the trait (per ADR-030’s generalization of ADR-007’s
third position plus ADR-036’s fourth model-declaration parameter) makes
the H-indexed family (ADR-019) a literal feature of the type signature:
every impl PrismModel<…> for … is one member of the family, and
applications can declare multiple impls for distinct selections. The
macro’s closure-bodied route function body is processed at expansion
time and the body never runs as Rust at runtime; the term tree the macro
emits is what pipeline::run_route evaluates via the catamorphism.
Foundation’s TermArena::from_slice const constructor enables the macro
to emit a fully-const route declaration, which is what ADR-020’s
"monomorphization is complete" commitment requires.
The __sdk_seal::Sealed doc-hidden public module is the
ecosystem-standard form for the closure check: external crates can
technically write impl Sealed for … but doing so is a non-conforming
act flagged by the documentation and the naming convention. The
architecture commits the prism_model! proc-macro as the only
sanctioned emitter of these impls, in the same spirit as ADR-016’s
commitment that prism's pipeline is the only sanctioned caller of the
mint primitives.
Rejected alternative (D1): Use pub(crate) Sealed in
prism::pipeline. Rejected — the prism_model! proc-macro lives
outside prism's pipeline module (typically in a sibling proc-macro
crate prism-macros or a prism::macros module published as a separate
compilation unit) and so cannot name a pub(crate) supertrait. The
doc-hidden public module preserves the architectural commitment without
violating Rust’s visibility rules.
Rejected alternative (D3): Accept Term::Application { … }
literal-arena syntax. Rejected — verbose to write, alien to Rust
developers, and the closure-bodied form is what the architecture wants
developers to read as "this is just a function." Hundreds of nested
Term::Application constructors per model would replicate the failure
mode the closure-bodied form is meant to avoid: the architecture’s
intent gets lost behind hand-rolled term-tree literals that no one
reads.
Rejected alternative (D4): Seven associated types on PrismModel
(Input, Output, Route plus HostTypes, HostBounds, AxisTuple,
ResolverTuple). Rejected — conflates two distinct concerns: what the
model declares (Input, Output, Route) vs what the family member is
parameterized by (H, B, A, R). The trait’s surface should name only the
former; the latter is a per-impl-block selection that lives in the
impl’s type parameters.
Rejected alternative (D5): Inline CompileUnit construction in the
macro. Rejected — couples the macro to foundation’s CompileUnit
internals, breaking the substrate-vs-SDK boundary. Foundation’s
pipeline::run_route higher-level entry point keeps the macro’s emitted
code at the architectural layer the wiki commits to.
Rejected alternative (D2): Have FoundationClosed expose the term
tree as &'static TermArena<CAP> (associated constant or method) rather
than as &'static [Term]. Rejected because Rust’s trait-level const
generics on the form needed to make CAP a per-impl quantity require
generic_const_exprs (unstable); fixing CAP at the trait level would
force every route in a workspace to share a capacity ceiling. The slice
form admits per-route term-count variation without trait-level const
generics and exposes the static, fully-const term tree the
catamorphism consumes. The slice form is the canonical surface; the
TermArena::from_slice constructor remains available for callers that
explicitly want the arena form (test harnesses needing the arena’s
as_slice() accessor or capacity tracking).
Status: Accepted.
Context: ADR-022 D5 specifies that
pipeline::run_route<H, B, A, M>(input: M::Input) constructs the
Validated<CompileUnit, FinalPhase> "from the model’s Route … plus
the input." The Route part is realized by reading
<M::Route as FoundationClosed>::arena_slice() (D5 + D6). The input
part is unspecified: an M::Input value of arbitrary
ConstrainedTypeShape cannot flow into the CompileUnit binding table
(foundation::enforcement::BindingsTable) without a serialization
mechanism, because the BindingEntry::bytes field has type &'static
[u8] — content-addressed static bytes — and an M::Input value supplied
at runtime is not static. The Term::Variable { name_index: 0 }
references the macro emits for the route’s input parameter therefore
have no runtime resolution mechanism. ADR-022 was silent on this; the
absence is an architectural gap that blocks correct catamorphism
execution for any non-empty Input.
Decision: Foundation declares a trait, IntoBindingValue, that any
ConstrainedTypeShape used as a PrismModel::Input MUST implement. The
trait surface is:
pub trait IntoBindingValue: ConstrainedTypeShape {
/// Serialize this input value into the binding-table form.
/// `out` is a fixed-capacity buffer the call-site provides;
/// the implementation writes the canonical content-addressable
/// byte sequence and returns the written length.
fn into_binding_bytes(&self, out: &mut [u8]) -> Result<usize, ShapeViolation>;
/// Maximum byte length any value of this shape can produce.
/// Used by `pipeline::run_route` to size the on-stack buffer
/// and reject inputs that would overflow.
const MAX_BYTES: usize;
}pipeline::run_route calls
input.into_binding_bytes(&mut buf[..max_bytes]) with a stack buffer of
size <B as HostBounds>::ROUTE_INPUT_BUFFER_BYTES (migrated to
HostBounds per ADR-037; was foundation-fixed
pipeline::ROUTE_INPUT_BUFFER_BYTES), where
max_bytes = <M::Input as IntoBindingValue>::MAX_BYTES. Inputs
declaring a MAX_BYTES exceeding
<B as HostBounds>::ROUTE_INPUT_BUFFER_BYTES are rejected at runtime
with a PipelineFailure::ShapeViolation carrying the IRI
https://uor.foundation/pipeline/RouteInputBufferShape/maxBytes. The
serialized bytes are hashed through the selected Hasher (initial
state, fold_bytes over the written prefix, finalize) to produce a
ContentAddress; the first 8 bytes of the digest are interpreted
big-endian as a u64 content fingerprint. The result populates a
transient
Binding { name_index: 0, type_index: 0, value_index: 0, surface: <M::Input as ConstrainedTypeShape>::IRI, content_address }
passed into CompileUnitBuilder::bindings(&[transient_input]) before
validate(). The transient binding lives in the CompileUnit's
bindings slice alongside any static bindings the route declares.
The foundation-fixed ceiling is the stable-Rust 1.83 equivalent of
nightly’s per-impl-sized form. On stable Rust, sizing the buffer as
[u8; <M::Input as IntoBindingValue>::MAX_BYTES] requires
generic_const_exprs (unstable); the foundation-fixed ceiling exposes
the same architectural surface (a static, const-known buffer-size
invariant the catamorphism depends on) without the unstable feature. The
architectural commitment is to the foundation-fixed ceiling form; the
specific numeric value is a foundation parameter, not architecture, and
raising the ceiling for applications with larger inputs is a
foundation-parameter change rather than an application-side override.
The foundation-sanctioned identity route (ConstrainedTypeInput)
implements IntoBindingValue returning zero bytes (MAX_BYTES = 0);
into_binding_bytes writes nothing and returns Ok(0). The macro adds
the trait bound to PrismModel's Input associated type when emitting
impls (so author-declared inputs carry the bound).
Consequences: Routes that reference the input parameter resolve
the Term::Variable { name_index: 0 } reference at runtime to the input
value’s content-addressable byte sequence, which the catamorphism then
reads through the standard binding-table lookup path
(Grounded::get_binding and friends). The author writes
into_binding_bytes once per ConstrainedTypeShape they use as an
Input; for shape-derived inputs (those produced by product_shape!,
coproduct_shape!, cartesian_product_shape!) the SDK macros emit the
IntoBindingValue impl alongside the ConstrainedTypeShape impl, so
the author writes nothing.
The trait is sealed via the same __sdk_seal::Sealed supertrait as
FoundationClosed and PrismModel: only foundation and the SDK macros
emit impls, preserving the architectural commitment that closure-bound
values flow through sanctioned constructors only.
Rejected alternative 1: Serialize the input via a generic
serde::Serialize impl. Rejected — serde is a heavyweight dependency
for foundation; the canonical-byte-sequence requirement
(content-addressing demands a single canonical serialization) is
stricter than serde's "any serializable form" contract; a
serde-driven path would invite the bincode/postcard/json-style
debate that foundation’s compile-time-zero-cost discipline rules out.
The dedicated trait surface is foundation-internal and has one canonical
implementation per shape.
Rejected alternative 2: Make pipeline::run_route accept binding
bytes directly (run_route<…, M>(input_bytes: &[u8])) rather than a
typed M::Input. Rejected — pushes the serialization burden onto every
caller, breaks the "developer writes model.forward(input)" surface
ADR-020 commits to, and makes type-system enforcement of input-shape
conformance impossible (the bytes are opaque to the type system).
Rejected alternative 3: Defer input-binding until a future ADR.
Rejected — the gap blocks correct catamorphism execution for non-empty
inputs; the architecture must specify the mechanism for the trait
surface to be complete. Currently only ConstrainedTypeInput (empty
shape) works, which is insufficient for any real application.
Rejected alternative 4: Have pipeline::run_route allocate the
buffer per-impl-sized via [u8; <M::Input as
IntoBindingValue>::MAX_BYTES], so each route’s buffer is exactly the
size its input declares. Rejected because Rust’s trait-level const
generics on the form needed to size a buffer with an associated constant
from a generic trait require generic_const_exprs (unstable); the
HostBounds-parametric ceiling (per ADR-037:
<B as HostBounds>::ROUTE_INPUT_BUFFER_BYTES) exposes the same
architectural surface (a static, const-known buffer-size invariant the
catamorphism depends on) on stable Rust. The runtime-rejection behavior
for inputs declaring
MAX_BYTES > <B as HostBounds>::ROUTE_INPUT_BUFFER_BYTES keeps the
type-system enforcement of input-shape conformance intact: an input
whose static MAX_BYTES exceeds the application-selected ceiling fails
at the same place a generic_const_exprs-form would fail at compile
time, just relocated to runtime under the stable-Rust form. The
HostBounds-parametric form is the canonical architectural commitment;
the per-impl-sized form is not a future migration target but the
rejected stable-Rust alternative.
Status: Accepted.
Context: ADR-013 commits prism to closure under uor-foundation's
vocabulary — every type prism exposes derives from foundation’s
type-declaration vocabulary, every operation composes PrimitiveOp
discriminants. The closure is one-dimensional in ADR-013’s text:
substrate vocabulary in, no extension. As the framework matures and
applications declare structured routes (ADR-020), a second closure
surface appears at the prism layer — the operator set application
authors compose to express routes — and a third at each implementation,
where domain-specific verbs (named compositions of prism operators
applied to substrate primitives, declared by a Layer-3 implementation
crate) compose prism operators into named, reusable units. The
architecture has three closures, not one; ADR-013’s text addresses only
the first. Without an explicit framing of the three-layer structure, the
relationship between operator-set commitments (ADR-025, ADR-026) and the
existing closure commitment (ADR-013) is unstated, and the
implementation layer’s closure pattern is not architecturally named.
Decision: The architecture commits to three layers of algebraic closure, each with its own carrier, its own operator set, and its own closure check. The three layers compose: each layer’s operators take operands from the layer below.
Layer 1 — Substrate closure. Carrier: uor-foundation's primitive
vocabulary (the Term enum’s variants, the PrimitiveOp discriminants,
the ConstraintRef variants, the WittLevel ceiling). Operators: the
algebra-level composers and endomorphisms that act on closures over the
constraint vocabulary (specified in ADR-025). Closure check: every
algebra reachable at substrate level decomposes under the substrate
operator set into irreducibles drawn from foundation’s primitive
vocabulary. ADR-013’s commitment is the type-and-operation half of
substrate closure; ADR-025 adds the operator-set half.
Layer 2 — Prism closure. Carrier: routes over substrate-closed
shapes — ConstrainedTypeShape impls bounded by prism's declared
bounds, composed into forward bodies via the operator set. Operators:
the prism operator set (specified in ADR-026). Closure check: every
route reachable at prism level decomposes under the prism operator set
into substrate-closed primitives. The macro’s FoundationClosed impl
emission (ADR-020, ADR-022 D1) is the type-level expression of prism
closure for whole-route declarations.
Layer 3 — Implementation closure. Carrier: each implementation’s
verb set — named, reusable compositions of prism operators applied to
substrate primitives, declared by the implementation for use within its
own routes (each Layer-3 crate declares verbs whose names and semantics
are domain-specific to that crate’s substrate; the architecture commits
to the closure pattern, not to specific verb identifiers). Operators:
composition under prism operators only — the implementation introduces
no new operators, only new named compositions. Closure check: every verb
is a composition of prism operators applied to substrate primitives ∪
other verbs of the same implementation ∪ verbs of explicitly imported
implementations; the verb-reference graph through non-recurse
operators is acyclic.
Verb declaration mechanism: An implementation declares a verb via a
verb! SDK macro (parallel to prism_model!, output_shape!, etc.).
The macro takes a closure-bodied form analogous to prism_model!'s
route declaration:
verb! {
pub fn my_named_verb(input: ...) -> ... {
// closure body composed of prism operators (G12–G19)
// applied to substrate primitives (G1–G11) and other
// verbs declared in this implementation
}
}The macro emits the verb’s term-tree fragment as a &'static [Term]
slice and a pub fn whose body the prism_model! macro can reference
by name during route-closure expansion. The verb-closure check
(acyclicity through non-recurse operators; closure under foundation
primitives ∪ own-implementation verbs ∪ imported verbs) is performed at
the application’s compile time by the verb! macro on each verb, plus a
final whole-implementation cycle check the prism_model! macro performs
over the verb-reference graph reachable from the model’s route. A cycle
in the verb-reference graph through non-recurse operators is a closure
violation, surfaced as a Rust compile error at the offending verb’s
verb! invocation site.
Axis declaration mechanism: An implementation declares a
substrate-extension axis via the axis! SDK macro per ADR-030,
paralleling verb!. The macro emits the axis trait declaration, the
sealed-trait marker, the kernel-identifier consts, and the dispatch glue
the catamorphism uses. The closure check at the axis! invocation
verifies the trait’s bounds satisfy AxisExtension's contract (sealed,
deterministic, #![no_std]-clean, output-bounded). Layer-3
implementations contribute both verbs (named compositions of operators)
and axes (substrate-extension vocabularies); both go through SDK macros,
both are sealed via __sdk_seal::Sealed, both participate in the
closure check at the prism_model! invocation site.
Cross-implementation verb imports: An implementation that wants to
use verbs from another implementation declares them through a
use_verbs! macro at the importing crate’s root (parallel to Rust’s
use statement but specific to verb identifiers):
use_verbs! {
from other_implementation_crate {
verb_name_a,
verb_name_b,
};
}The macro emits trait-method-style re-exports for the named verbs, gated
on the imported crate’s seal regime (the imported crate’s verb! impls
are themselves sealed via the standard __sdk_seal::Sealed pattern).
The importing implementation’s verb-closure check treats imported verbs
as opaque atoms satisfying the closure invariant; the imported
implementation’s own verb! macro performs that implementation’s
closure check. Imported verbs participate in the importing
implementation’s acyclicity check (the verb-reference graph including
imports must be acyclic outside recurse).
The three-layer structure is parametric in the substitution axes
(ADR-007). Substrate closure varies by (HostTypes, HostBounds, Hasher)
selection (which determines the primitive vocabulary’s instantiation at
the application’s compile time); prism closure varies in the same way
(the operator set’s lowering rules are parametric in the axes);
implementation closure varies as well (each implementation’s verbs
target a specific axis selection or range). No layer’s closure is fixed
at any specific axis selection; the closure procedures are theorems, the
snapshots at any selection are derivable.
Consequences: ADR-013’s substrate closure becomes one of three closures, with ADR-024 as the spine. ADR-025 and ADR-026 specify the substrate and prism operator sets respectively; together with ADR-013 they fully specify Layers 1 and 2. Layer 3 is implementation-defined per the pattern above; each implementation’s wiki (or equivalent) records its verb set. The three closures are independent (an implementation can extend its verb set without touching prism; prism can extend its operator set without touching substrate, subject to ADR-013’s substrate-amendment requirement) and compatible (operators at one layer compose objects from the layer below).
The architectural property the three-layer closure is load-bearing for:
parametric scaling. Nothing about the architecture is hardcoded at a
specific catalog enumeration, a specific Witt-level ceiling, a specific
verb count, or a specific n — every layer’s closure is enumerable at
any committed substitution-axis selection, and the relationships between
layers are theorems whose conformance is checked at each
implementation’s compile time.
Rejected alternative 1: Treat all three closures as a single flat
commitment under ADR-013. Rejected because ADR-013 is specifically about
substrate’s relationship to uor-foundation's type-and-operation
vocabulary; extending it to cover the operator-set surface and the
implementation verb-pattern conflates three concerns with distinct
change cadences (substrate vocabulary changes through foundation
amendment per TR-08; prism operator set changes through prism release;
verb sets change with each implementation) and three distinct
conformance checks.
Rejected alternative 2: Merge the prism and implementation layers — treat verbs as just another kind of prism operator. Rejected because verbs are domain-specific (the verb set of one Layer-3 implementation is not appropriate for an unrelated Layer-3 implementation — a tensor-compute crate’s verbs do not transfer to an FHE crate, etc.) while prism operators are domain-agnostic; conflating them would require prism’s release to enumerate every domain’s verbs, defeating the substrate-stability property and contradicting ADR-014’s "operation declaration vs operation shipment" separation.
Rejected alternative 3: Push verb-set declaration entirely outside the architecture, treating verbs as application-private compositions with no architectural status. Rejected because the verb-closure pattern (acyclicity through non-recurse operators; cross-implementation imports through explicit declaration) is itself an architectural commitment — it determines whether a verb-using implementation conforms to the architecture’s parametricity guarantees. Implementations that introduce new primitive operations under the guise of verbs (rather than compositions of prism operators) violate ADR-013’s substrate-closure commitment; the architecture must explicitly carry the verb-pattern definition to make this check well-formed.
ADR-025 — Substrate operator set: composers, endomorphisms, and the catalog as conformance test data
Status: Accepted.
Context: ADR-024 commits to substrate closure as one of three
layers. ADR-013 specifies substrate closure at the type-and-operation
level; what’s not specified is the operator set under which
substrate-level algebras compose. The catalog of algebras
(catalog_extended_v2.json and successors) and the transition tables
(transition_table_product, transition_table_coproduct,
transition_table_unary_add, etc.) at any committed snapshot enumerate
a finite closure of algebras under specific operators with specific
composition rules. The architecture currently treats the catalog and
transition tables as discovery artifacts; without an ADR commitment to
which operators are normative, conformant implementations could disagree
about whether a given algebra is reachable, what its decomposition kind
is, or what its composition with another algebra produces.
Decision: The substrate operator set has two components, applied to
closures over the constraint vocabulary (Site, Carry, Affine1,
AffineK and their successors at any HostBounds selection):
Composer operators: binary algebra-level operations that compose two operand algebras into a composite algebra.
-
×(partition_product). Composition rule PT_3: Betti numbers add at the nerve level (Künneth applies for the snapshot’s ConstraintRef alphabet; the rule extends with the alphabet); site counts add per ProductLayoutWidth (composite SC = SC(A) + SC(B)); CONSTRAINTS combine canonically per the constraint-pair canonicalization rule. -
+(partition_coproduct). Composition rule ST_10: Betti numbers add per the ST_10 corollary; site count ismax(SC(A), SC(B)) + 1per CoproductLayoutWidth; CONSTRAINTS combine via variant ordering by content fingerprint.
Endomorphism operators: unary algebra-level operations parametric in
a width parameter (typically the Witt-level n_bits), forming an
arithmetic-tower endomorphism family indexed by op ∈ Γ, where
Γ = {Add, Sub, Mul, Div, Mod, Pow} is the ring-axis arithmetic
operator set on Z/(2^n)Z (per ADR-053’s substrate-catalog extension),
separate from the hypercube-axis operator set {Xor, And, Or, Bnot};
the catalog distinction reflects the two metric axes per the
MetricAxis enum. Per ADR-050, every ring-axis and hypercube-axis
primitive evaluates at the full Witt tower (W8 through
TERM_VALUE_MAX_BYTES-bounded widths) with width =
max(operand widths) for binary ops.
-
after_op(src, n_bits)for eachop ∈ Γ: appends tosrc's witness set the constraints emitted by one application ofopwith a fresh LWE operand at widthn_bits. The emission rule has a regime split: a pre-triality rule applies forn_bits < 4(where the address space cannot host the full T=3 cycle); a post-triality rule applies forn_bits ≥ 4(where bits {0,1,2} close the triality cycle and the bit-1 anchor establishes). The regime-split structure, the constants T=3 (triality dimension) and O=8 (Hurwitz bound), and the derived constantpent = O − T = 5are theorem-grounded — they belong to the gauge-tower’s algebraic structure as normed-division-algebra extensions, not to a chosen encoding.
The disambiguator between × and structural coincidence is PT_1: an
algebra whose witness is structurally site-disjoint with no tag-pinner
and whose sum-of-component-sizes equals its observed site count is
partition_product-decomposable. An algebra that is Betti-additive
without satisfying PT_1’s site-disjointness —
irreducible_kunneth_coincidence in the catalog — is irreducible. PT_1
is the conformance test for × classification; without a normative
commitment to PT_1, two implementations could classify the same algebra
differently.
The catalog and transition tables at any committed snapshot enumerate
the closure of substrate-admissible irreducibles under the composer
operators (×, +) plus the application of endomorphism operators
(after_op for op ∈ Γ) at the snapshot’s parameter ranges. Any
committed snapshot (defined by the snapshot’s ConstraintRef alphabet
version, scope n ∈ {n_min..n_max}, and any other snapshot-level
parameters) is one row of an H-indexed family. Algebra IDs are 16-hex
content fingerprints; future snapshots at extended n or alphabets do
not invalidate older IDs because the IDs derive from algebra structure,
not from list position.
The catalog’s decomposition_kind enumeration follows the
operator-to-kind mapping:
-
×generatespartition_product(catalog kind populated at any snapshot at which composite algebras have been enumerated under the operator; the count is snapshot-specific). -
+generatespartition_coproduct(catalog kind populated to whatever count of genuine coproducts the snapshot’s enumeration scope contains; under PT_1 disambiguation, entries that are Betti-additive without satisfying the site-disjointness criterion reclassify toirreducible_kunneth_coincidenceand do not appear as coproducts). -
Each
after_opforop ∈ Γgenerates an arithmetic-tower endomorphism kind; the snapshot’s transition tables enumerate the resolutions perop, with the regime split (pre- and post-triality emission rules) verified at the snapshot’s enumeration scope. The architectural commitment is to the operator family{after_op : op ∈ Γ}and the regime split; specific snapshot enumeration coverage (whichopvalues, whichn_bitsranges) is snapshot-specific. -
Algebras that are not generated by any operator at the current snapshot are
irreducible; algebras that are Betti-additive without satisfying PT_1 areirreducible_kunneth_coincidence.
The catalog’s decomposition_kind enumeration at any snapshot is a
subset of the operator-to-kind mapping populated by enumeration; the
architecture commits to the mapping, not to specific snapshot
enumerations. Future snapshots at extended n may populate additional
kinds.
Composer operators vs endomorphism operators in catalog terms:
Composer operators (×, +) generate decomposition kinds for the
catalog directly; the catalog records each composite’s
decomposition_factors field naming the operands. Endomorphism
operators (after_op) predict catalog membership rather than generating
new decomposition kinds: the result of after_add(src, n_bits) is
either a pre-existing catalog entry (the operator collapses to an
already-catalogued algebra, possibly itself for fixed points) or
absent_structurally_distinct (a novel algebra not in the current
snapshot — a candidate for future snapshot inclusion). The transition
table for an endomorphism records the prediction; the catalog records
the resulting algebras when they’re present. Both patterns are
conformance-checkable: composer-generated algebras'
decomposition_factors match the operator’s operands;
endomorphism-predicted algebras' resolution status agrees across
implementations at the snapshot’s enumeration scope.
Consequences: ADR-025 commits the architecture to a substrate-level
operator set {×, +, after_op for op ∈ Γ} plus the PT_1 disambiguator.
The catalog and transition tables at any committed snapshot are
conformance test vectors for the operator set’s predictions: a
conformant Layer-1 implementation reproduces every catalog entry’s
algebra_id, betti, witness, decomposition_kind, and
decomposition_factors; reproduces every transition-table row’s
composite_* fields and resolution_status; reproduces the PT_1
classifications for every irreducible_kunneth_coincidence vs
partition_product distinction. Conformance is layer-1-local: it
concerns substrate behavior at the snapshot, independent of prism’s
operator set or any implementation’s verb set.
The arithmetic-tower endomorphism family’s regime split makes the
Categorical X regime split (per the ADR-025 glossary entry)
architecturally normative at the substrate layer: T=3 and O=8 govern the
n_bits=4 transition and the n_bits=8 Hurwitz boundary respectively,
and any implementation’s after_op runtime MUST exhibit these
transitions. The constants are theorem-grounded; the architecture
inherits them from the algebraic structure of normed division algebras
and commits to them as substrate-level invariants.
Bitwise operations (Xor, And, Or, Bnot) are PrimitiveOps but are
not in Γ; consequently they do not generate substrate-level
endomorphism kinds under the arithmetic-tower theorem framework. They
are reachable as Term::Application operators at the term-language
level (and through G3 in the closure-body grammar) but do not contribute
to the catalog’s algebraic structure. If a future theorem covers bitwise
operations in an analogous endomorphism framework, ADR-025 amends to
extend Γ.
Rejected alternative 1: Treat the catalog and transition tables as
normative reference data with a fixed enumeration scope. Rejected — any
specific snapshot’s n range and ConstraintRef alphabet are points in
an H-indexed family, not architectural ceilings; baking them into the
architecture would make the framework non-parametric in the substitution
axes and require an ADR amendment for every snapshot extension.
Rejected alternative 2: Commit to × and + only, leaving
after_op outside the substrate operator set. Rejected — the
arithmetic-tower endomorphisms are first-class catalog operators in the
transition tables (transition_table_unary_add is normative test data);
without an ADR commitment, the regime-split structure (T=3 triality
threshold, O=8 Hurwitz bound) is implicit and conformance is undefined
for the endomorphism predictions.
Rejected alternative 3: Treat all 10 PrimitiveOps as inducing
substrate-level endomorphism operators in the same framework. Rejected —
the Categorical X regime split is grounded in the gauge tower’s
normed-division-algebra structure, which holds for Γ = {+, −, ×, ÷, ^}
but not for the bitwise operations. Forcing the framework onto bitwise
ops would either require a different theorem (which the architecture
doesn’t currently have) or introduce a fictional regime split absent
from the algebra. Restricting the family to Γ keeps the commitment
theorem-grounded.
Status: Accepted.
Context: ADR-024 commits to prism closure as the second of three
layers. ADR-026 specifies the operator set under which routes —
forward bodies in PrismModel impls — are composed at prism level.
The closure-body grammar (ADR-022 D3, G1–G11) specifies the
substrate-level forms an application author writes in a route’s closure
body. The route-level composers — operators that compose multiple
substrate forms into structured routes — are not specified by G1–G11
alone; without a prism-level operator set, application authors writing
structured computations (iteration over rounds, tree-shaped reductions,
search over fibers, parallel pairings of independent routes) either
hand-roll the structure outside the type system (verbs declared in
prose, computation hand-rolled in sibling Rust modules, Term tree
degenerate to a placeholder literal — the architecturally non-conformant
pattern) or stretch G1–G11’s primitive forms to express patterns the
grammar wasn’t designed for.
Decision: The prism operator set has seven operators. Each
operator is parametric in the substitution axes (H, B, A), lowers
deterministically to a substrate-level term tree per a stated rule, and
exposes a Rust-syntactic form recognized by the prism_model! macro
through the closure-body grammar extension G12–G19 (specified in this
ADR’s Consequences). The seven operators are joined by an eighth
syntactic form, G19, which is not a prism operator but the
macro-recognized surface for the substitution-axis-realized verb form
(Term::AxisInvocation, per ADR-029, generalized per ADR-030). The
seven operators:
-
compose(f, g)— sequential function composition. Operands: two routesf: A → B,g: B → C. Result: routeA → Cwhose term tree isg's tree withf's tree substituted atg's input variable position. The macro lowers via sub-tree substitution at expansion time. -
parallel_compose(f, g)— parallel composition at the morphism level. Operands: two routesf: A → C,g: B → D. Result: routeA × B → C × Dwhose term tree is the partition-product off's andg's trees, with input components routed independently to each operand. Distinct frompartition_productbelow:partition_productoperates on shapes (type constructor);parallel_composeoperates on routes (morphism constructor). Both are needed because a closed operator set is closed under both directions of structural composition. -
fold_n(n, init, |state, idx| step)— bounded linear iteration. Operands: a compile-time-known iteration countn(a const literal, a substitution-axis-derived associated constant fromH,B, orA, or a route-parameter), an initial stateinit, and a step closure bindingstate(the current accumulator) andidx(the iteration index, ranging0..n). Result: route frominit's type to the step’s accumulator type afterniterations. The macro lowers to either an unrolledTerm::Applicationchain (whennis a const literal at or below<B as HostBounds>::FOLD_UNROLL_THRESHOLDper ADR-037, withidxsubstituted as aTerm::Literalat expansion time per unroll position) orTerm::Recurse { measure_index, base_index, step_index }(whennexceeds the threshold or is parametric, withstateresolved viaRECURSE_PLACEHOLDER_NAME_INDEXandidxresolved viaRECURSE_IDX_NAME_INDEXper ADR-034’s iteration-counter binding extension to ADR-029’sTerm::Recursefold-rule). -
tree_fold(reducer, leaves)— pairwise tree reduction. Operands: a binary reducer routereducer: A × A → Aand a list of leaves with finite, compile-time-known cardinality bounded by HostBounds. Result: route from the leaves' partition-product shape to the reducer’s output type, via successive halving levels. The macro lowers tofold_nover levels, depthceil(log2(leaves.len())), with each level applying the reducer pairwise to adjacent operands. -
first_admit(domain, predicate)— first-admission search over a parametric finite ring. Operands: a domain (a HostBounds-derivable finite ring — typically aWittLevel-indexed ringW{n}or a partition-product / partition-coproduct of such rings) and a predicate route over the domain. Result: a route from the domain’s identity to a coproduct-shaped value distinguishing "first admitting index found" (in canonical successor order over the ring) from "exhausted without admission" per ADR-034’s result-value convention. The macro lowersfirst_admittoTerm::FirstAdmit { domain_size_index, predicate_index }per ADR-034 (the twelfth Term variant; the lowering target shifted from aTerm::Recurse-based structural declaration in ADR-026’s original commitment to a dedicated variant with structural short-circuit on first admission). Foundation’s catamorphism evaluatesTerm::FirstAdmitper ADR-029’s per-variant fold-rule (iterateidxascending from 0 to<domain>::CYCLE_SIZEper ADR-032 sequentially with structural short-circuit on first admission, emitting a coproduct-shaped TermValue); the implementation-runtime override per the three-way responsibility split below remains available for strategy (sequential vs parallel coset traversal, cancellation policy, cost-budget enforcement) but is no longer load-bearing for structural correctness. -
partition_product(A, B)— Cartesian shape composition at the type level. Operands: twoConstrainedTypeShapeimplsAandB. Result: aConstrainedTypeShapeimpl whoseSITE_COUNT = A::SITE_COUNT + B::SITE_COUNT, whoseCONSTRAINTSare the canonically-ordered concatenation ofA::CONSTRAINTSandB::CONSTRAINTS, and whose IRI is content-deterministic per ADR-017. Same operator as ADR-025’s substrate-level×at the catalog-algebra level, observed at the type level. The macro emits the resultingConstrainedTypeShapeimpl when the operator appears at the type level (intype Inputortype Outputpositions). -
partition_coproduct(A, B)— alternation shape composition at the type level. Operands: twoConstrainedTypeShapeimplsAandB. Result: aConstrainedTypeShapeimpl whoseSITE_COUNT = max(A::SITE_COUNT, B::SITE_COUNT) + 1, whoseCONSTRAINTScombine via variant ordering by content fingerprint per ST_10, and whose IRI is content-deterministic per ADR-017. Same operator as ADR-025’s substrate-level+at the catalog-algebra level, observed at the type level.
Each operator is parametric in (H, B, A): no const literals are
architecturally privileged, no caps are hardcoded, no specific WittLevel
is required. The same operator-set ADR holds for an FHE-substrate
consumer (different B, different ring-level operations) as for a
cryptographic-search consumer (e.g., a W32-domain consumer with a
content-addressing axis selection) as for a tensor-compute consumer
(different B, tensor-axis selections) — the operator definitions don’t
change, only the substitution-axis selections do. The operator set’s
closure is the architectural commitment: any route reachable through
these seven operators applied to substrate-closed primitives is
prism-closed; any route requiring an operator outside the seven requires
an ADR amendment to extend the set.
first_admit’s three-way runtime responsibility: The
structural-inference operator first_admit requires evaluation of the
predicate at candidate values across the domain. Per ADR-034, structural
correctness is a foundation-level commitment (the catamorphism evaluates
Term::FirstAdmit end-to-end with sequential ascending iteration and
short-circuit on first admission); the implementation-runtime override
remains available for strategy selection. The three-way split:
-
Substrate owns the structural primitives the declaration composes from:
Term::FirstAdmitper ADR-034 (the dedicated variant);Term::ApplicationoverPrimitiveOpdiscriminants for the predicate body’s primitive operations;ConstraintRefvariants for the halt-predicate constraints; theWittLevelceiling parameter for the domain’s cardinality;<Domain>::CYCLE_SIZEper ADR-032 for proc-macro-time cardinality introspection. Foundation’s catamorphism evaluatesTerm::FirstAdmitper ADR-029’s per-variant fold-rule, so structural correctness (sequential ascending iteration with short-circuit on first admission, coproduct-shaped result) is a foundation-level commitment. -
Prism owns the operator
first_admitas a typed declaration form (ADR-026 G16): it commits to "search a finite parametric domain in canonical successor order under the predicate, terminate on first admission, fail on exhaustion." The macro’s lowering emitsTerm::FirstAdmitper ADR-034; foundation evaluates the variant. -
Implementation owns the runtime strategy that evaluates the declaration: sequential (the foundation-default), parallel coset traversal, cancellation hooks on first admission, cost-budget enforcement. The implementation MAY override foundation’s default sequential evaluation for performance reasons (parallel traversal across coset partitions, GPU-accelerated batch evaluation, etc.); the override produces the same first-admitting index as foundation’s reference evaluation would (the architecture’s structural-determinism commitment), differing only in wall-clock and resource profile.
Foundation provides pipeline::run's catamorphism as the default
sequential evaluator for Term::FirstAdmit (per ADR-029’s fold-rule).
Implementations that override for parallelism or specialized hardware do
so by intercepting the variant’s evaluation at the catamorphism’s entry;
the architectural commitment is that the structural-determinism property
holds across overrides — same (domain, predicate) pair → same
first-admitting index regardless of strategy.
The same three-way split applies to fold_n and tree_fold. For
fold_n, foundation’s catamorphism evaluates Term::Recurse (with
iteration-counter binding per ADR-034) end-to-end; the
implementation-runtime override is for strategy (e.g., loop unrolling
beyond the macro’s static threshold, vectorized state updates), not
load-bearing for structural correctness. For tree_fold, the macro
lowers to a fold_n decomposition (G15), inheriting Term::Recurse's
evaluation semantics.
Consequences: The prism operator set commits the architecture to seven operators. ADR-022 D3’s closure-body grammar (G1–G11) covers the substrate-level forms; ADR-026 extends it with G12–G19 covering the seven prism operators plus the substitution-axis-realized verb form as additional Rust-syntactic forms. The G12–G19 forms are an additive extension to the grammar — application authors writing closure bodies use either substrate-level forms (G1–G11), prism-level forms (G12–G18), the substitution-axis form (G19), or mixtures, and the macro’s recursive descent recognizes all.
The G12–G19 grammar (specified at ADR-022 D3’s grammar table after G11):
-
G12 —
compose. Recognized as nested function-call expressions:f(g(input))lowers tocompose(f, g)applied toinput. The macro recognizes nesting depth bounded only by HostBounds. (No new identifier reserved; nesting is the canonical Rust syntax for compose.) Disambiguation from G3: G3a recognizes the lowercasePrimitiveOpidentifiers from foundation’s canonicalPrimitiveOpenum at any committed snapshot (post-ADR-053:add,sub,mul,div,mod,pow,xor,and,or,neg,bnot,succ,pred,le,lt,ge,gt,concat— 18 variants); G12 recognizes any other identifier as a verb call (resolved against the implementation’s declared verb set per ADR-024’sverb!macro). The macro’s identifier-resolution order is: (1) reserved macro-vocabulary identifiers — G13–G19’sparallel,fold_n,tree_fold,first_admit,partition_product,partition_coproduct,hash, plus the named grammar forms whose identifiers are reserved per ADR-022 D3 (recursefor G7,unfoldfor G8,liftfor G4,projectfor G5), plus the ψ-chain Term grammar forms per ADR-035 (nervefor G21,chain_complexfor G22,homology_groupsfor G23,bettifor G24,cochain_complexfor G25,cohomology_groupsfor G26,postnikov_towerfor G27,homotopy_groupsfor G28,k_invariantsfor G29); (2)PrimitiveOpidentifiers per G3a (from the canonical catalog at the snapshot); (3) axis-trait method identifiers from the model’s declared AxisTuple per ADR-030 (resolved against the trait methods declared by each axis in the tuple, with(axis_index, kernel_id)determined by tuple position andKERNEL_<NAME>const respectively); (4) verbs from the declaring implementation’sverb!-emitted set; (5) verbs imported viause_verbs!(per ADR-024). An identifier matching none of these is a closure violation. Binary-operator forms per G3b are recognized at expression syntax level before identifier resolution and don’t participate in the resolution order. -
G13 —
parallel_compose. Recognized through the macro-vocabulary identifierparallel:parallel(f, g)produces the parallel-composed route. The macro emits the partition-product term-tree form.parallelis a reserved macro-vocabulary identifier (foundation does not export a Rust functionparallel). -
G14 —
fold_n. Recognized as a macro-vocabulary call:fold_n(<count_expr>, <init_expr>, |state, idx| <step_body>)where<count_expr>is a compile-time-known quantity (const literal, type-parameter constant, or substitution-axis-derived constant). The macro emits the unrolled chain orTerm::Recurseper the lowering rule; the chosen form is determined by<B as HostBounds>::FOLD_UNROLL_THRESHOLDper ADR-037 — counts at or below the threshold unroll, counts above useTerm::Recurse.fold_nis a reserved macro-vocabulary identifier. -
G15 —
tree_fold. Recognized astree_fold(<reducer_expr>, <leaves_expr>)where<leaves_expr>is a finite-cardinality static array, a partition-product shape, or a HostBounds-bounded expression of compile-time-known length (e.g., a[T; N]array, apartition_product!-emitted operand list, or a substitution-axis-derived const-length sequence). The macro emits the level-by-levelfold_ndecomposition.tree_foldis a reserved macro-vocabulary identifier. -
G16 —
first_admit. Recognized asfirst_admit(<domain_type>, |<idx_ident>| <predicate_body>)where<domain_type>is a HostBounds-derivable finite ring expressed at the type level.first_admitis a reserved macro-vocabulary identifier. The macro lowersfirst_admittoTerm::FirstAdmit { domain_size_index, predicate_index }per ADR-034.domain_size_indexreferences aTerm::Literalcarrying the domain’s cardinality (the ring’s cycle size) per ADR-032’s <DomainTy as ConstrainedTypeShape>::CYCLE_SIZE introspection, at the smallestWittLevelthat fits the cardinality per the wiki’s existing G1 commitment to literals parseable asu64.predicate_indexreferences the predicate body’s Term arena root; the SDK proc-macro lowers<idx_ident>references inside the predicate body directly toTerm::Variable { name_index: FIRST_ADMIT_IDX_NAME_INDEX }per ADR-034 — the foundation-fixed name index is the canonical lowering target. Foundation’s catamorphism evaluatesTerm::FirstAdmitper its fold-rule (iterateidxascending from 0 to<domain>::CYCLE_SIZEsequentially with structural short-circuit on first admission, emitting a coproduct-shaped TermValue per ADR-034’s result-value convention — the discriminator byte distinguishes "found" from "not-found" without conflating with any in-rangeidxvalue); the implementation-runtime override per the three-way responsibility split remains available for strategy (sequential vs parallel coset traversal, cancellation policy, cost-budget enforcement) but is no longer load-bearing for structural correctness. -
G17 —
partition_product(type-level). Recognized intype Inputandtype Outputpositions (and recursively in their operands) aspartition_product!(<A>, <B>, …)— variadic for ergonomic chaining of more than two operands. The macro emits the resultingConstrainedTypeShapeimpl.partition_productis a reserved macro-vocabulary identifier. Distinction fromcartesian_product_shape!: the existingcartesian_product_shape!macro emits a Cartesian-pairConstrainedTypeShapewhoseSITE_COUNT = A::SITE_COUNT + B::SITE_COUNTand whoseCONSTRAINTSareA's andB's independently (aLeft × Rightassociated-type-pair structure for compositional pairing);partition_product!(G17) emits the same site count but withCONSTRAINTScombined per PT_3’s canonicalization rule (the algebraic-product structure ADR-025 commits to). The two macros target different compositional patterns:cartesian_product_shape!for type-level pair declarations where the components are observed independently;partition_product!for the catalog-algebra-conformant product where the composite’s CONSTRAINTS are the canonical join of the operands'. -
G18 —
partition_coproduct(type-level). Recognized aspartition_coproduct!(<A>, <B>, …), parallel to G17. The macro emits the resultingConstrainedTypeShapeimpl withSITE_COUNT = max(operands' SC) + 1.partition_coproductis a reserved macro-vocabulary identifier. -
G19 —
Term::AxisInvocation(substitution-axis-realized verb form, generalized per ADR-030). Recognized as axis-trait method call expressions where the called identifier resolves to a method on one of the model’s declared axis traits per ADR-030’s identifier-resolution order. The macro emitsTerm::AxisInvocation { axis_index, kernel_id, inputs: TermList }withaxis_indexresolved from the position in the model’s AxisTuple andkernel_idresolved from the called method’s KERNEL_<NAME> const. The catamorphism evaluates it by dispatching throughA::dispatch(axis_index, kernel_id, &evaluated_inputs)per ADR-030 and ADR-029’s per-variant fold-rule.ψ-residuals discipline restriction per ADR-035 + ADR-056:
Term::AxisInvocationis a ψ-residual — admission expressed as an axis-method dispatch on byte values rather than a structural ψ-chain witness. The ψ-residuals discipline forbids direct syntactic emission ofTerm::AxisInvocationfrom the route body’s syntactic surface (theprism_model!-declaredrouteclosure body) per ADR-056; the canonical hash axis is consumed at the route surface by resolvers (the ResolverTuple per ADR-036), not by direct route-body composition. The reservedhashidentifier remains in the macro’s identifier-resolution order (the surface form is admitted at proc-macro parse time per the resolution-order specification), but any direct emission ofTerm::AxisInvocationfrom the route body fails at proc-macro expansion with a ψ-residuals-discipline closure-violation error citing the route’s name.Term::AxisInvocationremains in the substrate’sTermenum and is admissible in all three non-route-body verb categories per ADR-056: compound verb bodies declared viaverb!per ADR-024 (their internal Term arenas fold-fuse into the route’s evaluation per ADR-054), axis impl bodies per ADR-055’s universal substrate-Term verb body discipline, and resolver bodies per ADR-046 (resolver impls use axis dispatch internally as part of theirresolvesemantics). Conformance-corpus generators and foundation-internal trace replay may also exercise the variant directly. Application authors whose route logic naturally needshash(input)express the equivalent through (a) a resolver-boundTerm::Nerve(or other resolver-bound ψ-Term) whose resolver impl internally invokes the canonical hash axis, or (b) a compound verb declared viaverb!per ADR-024 whose internal body useshash(…)directly — fold-fusion per ADR-054 inlines the verb body into the route’s evaluation. Models whose route bodies emit no axis-trait method call directly do not produce a top-levelTerm::AxisInvocationand route only through thePrimitiveOp-based fold-rules and the ψ-Term fold-rules at the route surface.
The seven operators are the closure of the prism operator set. Operators
not in the seven are out of prism’s closure; reaching them requires
either composing them from the seven (in which case they’re verbs at the
implementation layer per ADR-024) or amending ADR-026 to extend the set.
Specific candidates explicitly outside the seven and the reasoning for
each: iterate_until (runtime-bounded iteration with termination
predicate; derivable from first_admit with a state accumulator
threaded through compose, lowering through Term::FirstAdmit per
ADR-034 with the predicate body composing the termination condition over
the iteration-counter binding FIRST_ADMIT_IDX_NAME_INDEX);
partial_evaluate (β-reduction; derivable from compose with a
constant-route operand); restrict (filter the domain; derivable from
compose with a guarded-identity operand); lift_to and project_to
(Witt-level transitions; covered at the closure-body grammar level by G4
and G5 — they don’t introduce structural forms beyond a single Term
variant). Adding any of these to the prism operator set requires an ADR
amendment with the closure justification.
Rejected alternative 1: Six operators only — parallel_compose
derivable from partition_product plus compose and projection
morphisms. Rejected — projection morphisms are not currently in the
substrate primitive set, and the universal property of products requires
either explicit projections or a primitive parallel_compose. The
seven-operator set is the smaller architectural commitment under stable
Rust.
Rejected alternative 2: Lift Witt-level transitions (lift_to,
project_to) into the prism operator set. Rejected — these are 1-to-1
with Term::Lift and Term::Project and live at the closure-body
grammar level (G4, G5). Promoting them to operators would duplicate the
level boundary without adding expressivity; the grammar’s level
recognizes them at the syntactic surface, the substrate’s Term enum
recognizes them at the type level, and no prism-layer structural form is
built from them that isn’t already a single Term variant.
Rejected alternative 3: Make first_admit a substrate-layer
operator (i.e., have foundation own the operator surface itself, not
just structural primitives). Rejected — first_admit's closure-body
surface form (first_admit(<domain>, |<idx>| <predicate>)) is a
prism-level operator declaration that composes substrate primitives (the
predicate body’s Term forms, the domain’s <Domain>::CYCLE_SIZE per
ADR-032) under the operator’s typed-iso contract. Promoting the operator
to substrate would conflate the prism layer’s role (operator declaration
on substrate-closed shapes) with the substrate’s role (primitive type +
operation vocabulary). The three-way responsibility split keeps the
operator prism-level (G16) and the structural correctness
foundation-level (Term::FirstAdmit per ADR-034 + the variant’s
fold-rule per ADR-029); the implementation-runtime override per the
split’s third position is for strategy (sequential, parallel,
GPU-accelerated, etc.), not for structural correctness — ADR-034
reframed the runtime-strategy question so foundation’s catamorphism
provides a default sequential evaluator while implementations may
override for performance.
Status: Accepted.
Context: ADR-020 commits
PrismModel::forward(input) → Result<Grounded<Output>, PipelineFailure>
as the application author’s typed-iso surface; ADR-022 D4 specifies the
trait body with type Output: ConstrainedTypeShape + GroundedShape. The
current foundation source seals GroundedShape to
ConstrainedTypeInput only — every model’s Output is the empty identity
shape. The typed-iso commitment is therefore vacuous at the Output side:
applications declare forward(features) → labels, but no labels can
flow through the typed-iso surface; the labels live outside the
foundation-sealed Grounded. The architecturally non-conformant pattern
this produces in implementations: Output = ConstrainedTypeInput, the
route is the identity term, and the actual output bytes flow on a
side-channel structure outside the Grounded — a mining application’s
mined-hash bytes carried on a separate MiningOutcome::digest field, an
FHE application’s ciphertext carried on a parallel return value, etc.
Without a sanctioned mechanism for declaring shape-rich Outputs, no
PrismModel’s typed-iso surface is observable end-to-end.
Decision: Foundation generalizes GroundedShape so any
ConstrainedTypeShape impl declared through a sanctioned construction
path qualifies as an Output. The sanctioned path is the output_shape!
SDK macro, parallel to product_shape! / coproduct_shape! /
cartesian_product_shape!. The macro emits, for an application-declared
output shape:
output_shape! {
pub struct OutputHash;
impl ConstrainedTypeShape for OutputHash {
const IRI: &'static str = "https://prism.btc/shape/OutputHash";
const SITE_COUNT: usize = 32;
const CONSTRAINTS: &'static [ConstraintRef] = &[];
}
}Macro expansion:
-
pub struct OutputHash;— the application-named output shape struct (zero-sized type-level marker) -
impl ConstrainedTypeShape for OutputHashwith the application’s declaredIRI,SITE_COUNT, andCONSTRAINTS -
impl __sdk_seal::Sealed for OutputHash— the same sealed-trait pattern from ADR-022 D1 -
impl GroundedShape for OutputHash— the carrier-side commitment that this shape can appear asTinGrounded<T>, gated onSealed -
impl IntoBindingValue for OutputHashwithMAX_BYTESequal to the canonical byte-sequence length the catamorphism’s evaluation produces for this shape (per ADR-029) — for a shape declared at byte-level granularity this equalsSITE_COUNT; for shapes at higher Witt levels the macro derives the byte length fromSITE_COUNT × <H as HostTypes>::W{level}_BYTESfor the level the shape’s CONSTRAINTS commit to. TheIntoBindingValueimpl supports the compositional reading where the Output of one model is the Input of a downstream model (per ADR-022 D4’s bound).
The foundation-sanctioned identity output ConstrainedTypeInput retains
its existing direct impl (no macro emission); it remains the default for
models that declare no transformation. Application authors declaring
custom Output shapes invoke output_shape! and obtain the impls; the
resulting shape is GroundedShape-conformant by virtue of the macro’s
vetted emission, not by virtue of an open seal.
Consequences: The typed-iso surface becomes meaningful at the Output
side. PrismModel declarations carry both Input feature shapes and Output
label shapes at the type level. An application declares its custom
Output shape (e.g., a 32-byte OutputHash for a hashing application, a
ClassificationLabel for an inference application, a numeric
OutputResidue for an arithmetic-tower application) through
output_shape! and uses Output = <ShapeName> in the model
declaration. The Grounded is parameterized over the actual shape the
model produces; downstream consumers (verifiers, applications iterating
over forward() calls) read the Output bytes through the value-payload
mechanism (per ADR-028).
Models that declare Output = ConstrainedTypeInput (the identity
output) continue to work without change: the foundation-sanctioned
identity impl is preserved, and the typed-iso surface remains valid for
transformation-free declarations (e.g., a model that attests "this Input
was admitted under these substitution axes" without producing additional
output bytes). The output_shape! mechanism is additive; existing impls
require no migration.
The seal’s discipline is preserved: external crates that name
__sdk_seal::Sealed directly are flagged as architecturally
non-conforming, just as for FoundationClosed, PrismModel, and
IntoBindingValue. Custom Output shapes flow through the SDK-macro
lane, which is foundation-vetted; the seal is generalized (the path
widens to any sanctioned-construction shape), not lifted (external
direct impls remain blocked).
Rejected alternative 1: Keep GroundedShape sealed to
ConstrainedTypeInput. Rejected — makes the framework’s typed-iso
surface degenerate; the catamorphism’s purpose (yielding outputs from
inputs) is unobservable through the typed-iso surface; applications that
need to carry labels resort to side channels (a separate output-bytes
field outside the Grounded) that escape the foundation-sealed primary
surface.
Rejected alternative 2: Lift the seal entirely; allow any
application crate to impl GroundedShape directly. Rejected — breaks
the closure-bound discipline ADR-013 commits to. External direct impls
could expose shapes whose CONSTRAINTS reference unimplementable
invariants, whose SITE_COUNT exceeds carrier-side bounds, or whose
construction skips the canonical-IRI requirement of ADR-017.
Rejected alternative 3: Add a per-Output-kind trait family (e.g.,
HashOutput, NumericOutput, ByteOutput). Rejected — generates an
open-ended trait family per Output category; the unified output_shape!
macro covers all shapes through a single mechanism. The
ConstrainedTypeShape trait already carries the structural commitments
(IRI, SITE_COUNT, CONSTRAINTS) all output kinds share; per-kind traits
add no expressivity.
Rejected alternative 4: Push Output-shape declaration to a
per-application escape hatch outside the SDK-macro mechanism. Rejected —
duplicates the SDK-macro pattern that already exists for Input shapes
(product_shape!, coproduct_shape!, cartesian_product_shape!); a
parallel mechanism for Outputs is the architecturally consistent choice
and reuses the macro infrastructure.
Status: Accepted. Amended by ADR-060. The output-value payload’s
carrier changes from a fixed-capacity on-stack slot bounded by
ROUTE_OUTPUT_BUFFER_BYTES to a source-polymorphic TermValue
(Inline for outputs within the derived inline width, Borrowed into
an upstream byte source, or Stream for unbounded outputs).
ROUTE_OUTPUT_BUFFER_BYTES is removed; there is no fixed output buffer
and no application-declared output byte-width ceiling. The architectural
commitment that Grounded<T> carries the output value (not just
metadata) is unchanged; only the carrier representation changes. Read
this ADR’s ROUTE_OUTPUT_BUFFER_BYTES / fixed-stack-slot content as
superseded by ADR-060’s carrier surface.
Context: ADR-020’s typed-iso surface returns Grounded<Output> from
forward(input). ADR-019 names the catamorphism’s codomain as the
runtime carrier — Result<Grounded<T>, PipelineFailure> parameterized
over the application’s Output shape. The structural reading of "carrier"
is that the Grounded carries the catamorphism’s evaluation result:
input bytes flow in, the route’s structural fold produces output bytes,
the Grounded wraps the bytes for downstream consumers. Foundation
0.3.2’s Grounded<T> is structurally not a value carrier: its
fields hold the typed-iso path attestation (CompileUnit metadata
fingerprint, unit_address, triad, witt_level_bits, Tag phantom) but no
slot for the T-shaped bytes the route’s evaluation would produce. The
phantom-typed T parameter is unobservable at the value level — two
distinct inputs produce Groundeds with bit-identical fingerprints
because the fingerprint is over metadata, not over the output the route
would compute. The typed-iso surface is therefore vacuous at the value
side: forward(features) returns a witness of path, not labels.
Decision: Foundation extends Grounded<T> to carry an output-value
payload alongside the metadata fingerprint. The structural commitment:
-
Grounded<T, Tag>carries an output-bytes slot of fixed capacity bounded by<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES(migrated toHostBoundsper ADR-037; parallel in form to<B as HostBounds>::ROUTE_INPUT_BUFFER_BYTES). The slot’s actual length per Grounded is the route’s evaluation output length, bounded above by the Output shape’s<T as IntoBindingValue>::MAX_BYTES, itself bounded above by<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES -
Public accessor:
pub fn output_bytes(&self) → &[u8]returns the payload slice with length equal to the route’s evaluation output length -
Models declaring an Output shape whose
MAX_BYTESexceeds<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTESare rejected at validation time with aPipelineFailure::ShapeViolationcarrying the IRIhttps://uor.foundation/pipeline/RouteOutputBufferShape/maxBytes(parallel to the input-side rejection from ADR-023) -
The metadata
content_fingerprintandunit_addressremain as typed-iso path attestation; the value payload is additional, not a replacement -
The Output shape’s per-shape semantics (e.g., bytes interpreted as a 32-byte digest, a u128 numeric value, an ASCII string) are determined by the shape’s
IRIand the application’s deserialization on the receiving side; foundation carries the bytes, the application interprets them
The value payload is what pipeline::run populates as the
catamorphism’s evaluation result (per ADR-029). Foundation’s
pipeline::run_route (and its lower-level pipeline::run) evaluates
the Term tree with the input bindings, accumulates the output bytes into
a stack buffer of capacity
<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES per ADR-037, and
constructs the Grounded with the bytes copied into the payload slot. The
metadata fingerprint is computed alongside (over CompileUnit metadata,
unchanged from current behavior) and serves as the path-attestation
witness.
Consequences: forward(input) returns a Grounded that carries both
the foundation-sealed typed-iso path attestation AND the output value.
Applications access the output via grounded.output_bytes(); the path
attestation remains accessible via grounded.content_fingerprint() and
grounded.unit_address() for verification and addressing. A model whose
Output shape is OutputHash (32 bytes) returns
Grounded<OutputHash, Tag> whose output_bytes() is the actual 32-byte
hash — computed by the catamorphism’s evaluation per ADR-029. The
path-attestation property — that two distinct inputs produce Groundeds
with bit-identical fingerprints because fingerprints are over
CompileUnit metadata — remains true and is the foundation-sealed
path-attestation guarantee. Output bytes will differ across distinct
inputs because they ARE the route’s evaluation result; the
path-attestation and the value are bound together in one
foundation-sealed structure.
The value payload’s fixed-capacity-on-stack representation is required
by foundation’s #![no_std] posture (Section 8, no-std Posture
concept): no heap allocation in the carrier path. Applications whose
Output shapes exceed <B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES are
rejected at validation time, just as oversized inputs are per ADR-023;
per ADR-037, the ceiling is HostBounds-parametric — applications
declare their own HostBounds impl to raise the ceiling, or select
DefaultHostBounds which carries foundation’s prior fixed value as
default. <B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES is the
architectural commitment; both input and output buffer ceilings live on
HostBounds (per ADR-037 clause (1)) as stable-Rust associated
constants whose specific numeric values are application-selected.
Rejected alternative 1: Return a tuple (Grounded<T>, OutputValue)
from forward(). Rejected — splits the seal: the output value should be
inside the foundation-sealed Grounded so the path-attestation and the
value are bound together as one mint. A tuple makes the value separable
from the attestation, which breaks the architectural commitment that
"sealed values arise only along the principal data path" (Section 8,
Sealing Discipline).
Rejected alternative 2: Keep Grounded as metadata-only; flow output
values through a separate side channel (a parallel OutputValue type,
an out-parameter, a thread-local). Rejected — the typed-iso surface
ADR-020 specifies has forward() yielding Grounded<Output>; making
Grounded a metadata-only structure makes the typed parameter Output
vacuous (a phantom marker, not a value carrier). The architecturally
non-conformant pattern (a side-channel field outside the
foundation-sealed Grounded carrying the application’s actual output
bytes) is exactly what ADR-028 brings into the foundation-sealed primary
surface.
Rejected alternative 3: Make Grounded generic in a value-carrier
type (Grounded<T, Value, Tag>). Rejected — the bytes form is
universal: every ConstrainedTypeShape's value can be expressed as a
fixed-capacity byte buffer. Generic value-carrier types proliferate
without expressive gain; the Output shape’s IRI already names the
shape’s semantic interpretation.
Rejected alternative 4: Use a heap-allocated payload (Vec<u8>,
Box<[u8]>, Cow<[u8]>). Rejected — foundation’s #![no_std] posture
(Section 8) forbids heap allocation in the carrier path; fixed-capacity
stack buffers bounded by the HostBounds-parametric
<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES ceiling (per ADR-037) are
the architecturally consistent choice. The same constraint that drove
ROUTE_INPUT_BUFFER_BYTES (per ADR-023’s reconciliation) drives
ROUTE_OUTPUT_BUFFER_BYTES; both live as HostBounds associated
constants per ADR-037.
Status: Accepted.
Context: ADR-019 names pipeline::run as the catamorphism induced
by Term's initial-algebra structure: the unique morphism from Term
to the host carrier Result<Grounded<T>, PipelineFailure>. The
catamorphism’s defining property — turning Term-shaped input into
carrier-shaped output by induction on Term structure — requires
per-variant fold-rules that produce carrier values from variant
components and recursive results. Foundation 0.3.2’s pipeline::run
validates the CompileUnit and emits a Grounded with CompileUnit-metadata
fingerprints, but performs no Term-tree evaluation: the Term arena’s
contents do not influence the output’s value-level result, only its
path-attestation fingerprint. The catamorphism is named in ADR-019 but
not realized in the implementation; the architectural claim
"pipeline::run is the catamorphism" holds only at the
metadata-attestation level. For the input-to-output routing to be
observable end-to-end — for forward(features) to actually yield labels
per ADR-020 + ADR-027 + ADR-028 — foundation must implement the
catamorphism’s per-variant evaluation semantics.
Decision: pipeline::run evaluates the route’s Term tree as a
structural fold, with per-variant fold-rules specified normatively. The
fold’s result is the Output shape’s bytes, populated into the Grounded’s
value payload (per ADR-028).
The catamorphism’s evaluation environment threads five substrate
parameters per ADR-022 D5 + ADR-030 + ADR-036 + ADR-048: H: HostTypes
(host-platform witness type), B: HostBounds (host-platform capacity
bounds), A: AxisTuple + Hasher (substitution-axis tuple with the
canonical hash axis bound), R: ResolverTuple (resolver tuple
defaulting to NullResolverTuple), and C: TypedCommitment
(typed-bandwidth admission commitment defaulting to EmptyCommitment
per ADR-048). Per-variant fold-rules consult the substrate parameters as
their semantics require — combinatorial Term variants thread the type
parameters through their fold-rules without value-level state; the eight
resolver-bound ψ-Term variants per ADR-035 consult R at evaluation
time per ADR-036’s resolver-tuple mechanism; the resolver-free ψ-Term
variant (Betti) extracts directly from its operand’s byte serialization;
after ψ_9 emits the κ-label, C::evaluate(kappa_label) is consulted per
ADR-048 for the post-resolver typed-bandwidth admission decision. The
fold-rule pattern is uniform across all twenty-one variants — same
recursive evaluation, same TermValue carrier, same shape-violation
propagation through Term::Try per ADR-022 D3 G9. The verb body’s
ψ-residuals discipline per ADR-035 forbids Term::FirstAdmit and
Term::AxisInvocation emissions in verb-body terms (along with
byte-comparison and byte-concat PrimitiveOp emissions); these constructs
remain in the substrate’s Term vocabulary for non-verb-body contexts
(conformance-corpus generators, foundation-internal trace replay) but
are rejected at proc-macro expansion when emitted from verb bodies.
The per-variant rules:
-
Term::Literal { value, level }— emitvalueas the result at Witt levellevel. The literal’s bytes (in canonical big-endian form for the Witt level) are the variant’s carrier value; recursion does not enter the fold. -
Term::Variable { name_index }— look up the binding identified byname_indexin the CompileUnit’s bindings table. The binding’s bytes (per ADR-023’sIntoBindingValueserialization) are the variant’s carrier value.name_index = 0is the route input parameter (per ADR-022 D3 G2);name_index ∈ [1, …]arelet-introduced bindings (per ADR-022 D3 G10); the wildcard sentinelname_index = u32::MAXis reserved forTerm::Matcharms (G6) andTerm::Trydefault-propagation (G9). -
Term::Application { operator, args }— evaluate each arg inargs(recursive fold); applyoperator(aPrimitiveOpdiscriminant) to the args' results per the operator’s algebraic rule per the canonicalPrimitiveOpcatalog at any committed snapshot. Foundation 0.3.6’s catalog:Addfor arithmetic addition mod 2^level;Subfor subtraction;Mulfor multiplication;Xorfor bitwise xor;And/Orfor bitwise conjunction/disjunction;Negfor two’s-complement negation;Bnotfor bitwise complement;Succfor successor;Predfor predecessor;Le/Lt/Ge/Gtfor byte-level lexicographic comparison emittingLiteral(1)on true,Literal(0)on false (operands compared as big-endian unsigned byte sequences);Concatfor byte-sequence concatenation, result length equals sum of operand lengths bounded by<B as HostBounds>::TERM_VALUE_MAX_BYTESper ADR-037. Emit the result at the operator’s output Witt level (or, forConcat, at the byte-sequence representation whose length is the operands' summed length, with the catamorphism’s TermValue capacity per ADR-028 carrying the bytes). -
Term::Lift { operand_index, target }— evaluate operand (recursive fold); apply the canonical injection from operand’s Witt level totarget(zero-extend the operand’s bytes into a buffer oftargetwidth). The variant fails at evaluation iftarget ≤ operand’s Witt level(the closure-violation check from ADR-022 D3 G4 catches this at macro expansion; runtime evaluation enforces the same invariant). -
Term::Project { operand_index, target }— evaluate operand (recursive fold); apply the canonical surjection from operand’s Witt level totarget(truncate the operand’s bytes to a buffer oftargetwidth). The variant fails at evaluation iftarget ≥ operand’s Witt level(paralleling Lift; G5 from ADR-022 D3 catches this at macro expansion). -
Term::Match { scrutinee_index, arms }— evaluate scrutinee (recursive fold); match the scrutinee’s bytes against the arms' patterns (literal patterns by byte equality; the wildcard sentinelVariable { name_index = u32::MAX }matches unconditionally); evaluate the matching arm body (recursive fold) and emit. Match failure (no arm pattern matches and no wildcard arm provided) is aPipelineFailure::ShapeViolationper the closure-violation discipline at ADR-022 D3 G6; well-formed Term trees never exhibit match failure at evaluation time because the macro enforces wildcard arm exhaustiveness at expansion. -
Term::Recurse { measure_index, base_index, step_index }— evaluatemeasure(recursive fold); if the measure equals zero, evaluatebase(recursive fold) and emit; otherwise, evaluatestep(recursive fold) in extended scope where (a)RECURSE_PLACEHOLDER_NAME_INDEXbinds to aTermValuecarrying the result of evaluating the sameTerm::Recursewithmeasuredecremented by 1, AND (b)RECURSE_IDX_NAME_INDEXbinds to aTermValuecarrying the current measure value (the iteration counter at this descent) per ADR-034. The fold terminates when the measure reaches zero; well-foundedness is structurally guaranteed by the descent measure’s monotonic decrease. -
Term::Unfold { seed_index, step_index }— evaluate seed (recursive fold) into the initial state; evaluate step (recursive fold) with the state placeholder bound to the seed’s result; emit the step’s result (the unfold’s coalgebra structure is one-step-per-evaluation; multi-step unfolds are expressed by composingTerm::UnfoldwithTerm::Recurseper the closure-body grammar’s compositional commitments). -
Term::Try { body_index, handler_index }— evaluate body (recursive fold). On success, emit the body’s result. OnPipelineFailure, ifhandler_indexisu32::MAX(the default-propagation sentinel from ADR-022 D3 G9), propagate the failure unchanged through the catamorphism’s outer Result; otherwise, evaluate handler (recursive fold) with the failure as a bound input and emit its result. -
Term::AxisInvocation { axis_index, kernel_id, inputs }— evaluate each input term recursively (recursive fold) to produce a slice ofTermValues; dispatch through <A as AxisTuple>::dispatch(axis_index, kernel_id, &evaluated_inputs) per ADR-030 to the right axis impl’s kernel; emit the kernel’s result as the variant’s evaluation output. The variant delegates evaluation to the application’s chosen axis impls within the AxisTuple (per ADR-030); see Substitution-axis-realized verbs below for the closure-pattern context. The variant is emitted by theprism_model!macro from the closure-body axis-trait method call form (per ADR-026 G19). -
Term::ProjectField { source_index, byte_offset, byte_length }— evaluate the source term identified bysource_index(recursive fold) producing a TermValue; emit the byte slice[byte_offset .. byte_offset + byte_length]from the source’s evaluation result as the variant’s carrier value.byte_offset + byte_lengthmust be ≤ the source’s byte length; this is verified at proc-macro expansion time from the receiver shape’s structural metadata, so well-formed Term trees never exhibit out-of-bounds slicing at evaluation time. The variant is emitted by theprism_model!andverb!macros from the closure-body field-access form (per ADR-022 D3 G20 + ADR-033). -
Term::FirstAdmit { domain_size_index, predicate_index }— evaluatedomain_size_index(recursive fold) producing aTermValuecarrying a non-negative integer N at the smallest WittLevel that fits N per ADR-022 D3 G1’s u64-width commitment. Foridxin0..N(ascending from 0, sequentially): evaluatepredicate_index(recursive fold) in extended scope whereFIRST_ADMIT_IDX_NAME_INDEX(a foundation-fixed name index per ADR-034) binds to aTermValuecarryingidxat the same WittLevel as N’s; if the result is non-zero (per foundation’s existing zero/non-zero convention from ADR-029’s primitive-comparison fold-rules: any TermValue whose byte sequence is not all-zero is "true"), emit aTermValuecarrying the coproduct value(0x01, idx_bytes)(the "found" discriminator followed byidxpacked at the domain’s WittLevel byte width) and terminate the iteration. If noidxadmits across the full range[0, N), emit aTermValuecarrying the coproduct value(0x00, padding)(the "not-found" discriminator followed by idx-width zero bytes; the padding bytes have no semantic meaning, structural padding only). Well-foundedness is structurally guaranteed by the bounded domain (Nevaluations maximum). The variant is emitted by theprism_model!andverb!macros from the closure-bodyfirst_admit(<domain>, |<idx>| <predicate>)form per ADR-026 G16 + ADR-034. -
Term::Nerve { value_index }— evaluatevalue_indexproducing a per-value byte sequenceTermValue; consultR::nerve_resolver()per ADR-036 returning a&dyn NerveResolver<A>; callresolver.resolve(value_bytes, out_buffer)producing a SimplicialComplex byte serialization per ψ_1’s identityN(constraints) → SimplicialComplex; emit aTermValuecarrying the SimplicialComplex bytes. OnShapeViolation(RESOLVER_ABSENTfor aNullNerveResolver,CAPACITY_EXCEEDED, etc.), propagate throughTerm::Tryper ADR-022 D3 G9. Per ADR-035. -
Term::ChainComplex { simplicial_index }— evaluatesimplicial_indexproducing a SimplicialComplexTermValue; consultR::chain_complex_resolver(); callresolver.resolve(simplicial_bytes, out_buffer)producing a ChainComplex byte serialization per ψ_2’s identityC(K) → ChainComplex; emit aTermValue. Per ADR-035. -
Term::HomologyGroups { chain_index }— evaluatechain_indexproducing a ChainComplexTermValue; consultR::homology_group_resolver(); callresolver.resolve(chain_bytes, out_buffer)producing a HomologyGroups byte serialization per ψ_3’s identityH_k© = ker(∂k) / im(∂{k+1}); emit aTermValue. Per ADR-035. -
Term::Betti { homology_index }— evaluatehomology_indexproducing a HomologyGroupsTermValue; extract the Betti-number array directly from the HomologyGroups byte serialization per ψ_4’s identityβ_k = rank(H_k)(foundation-vetted extraction; no resolver consultation; no axis-as-hasher threading); emit aTermValuecarrying the BettiNumbers byte serialization per the substrate’s BettiNumbers shape. Per ADR-035. -
Term::CochainComplex { chain_index }— evaluatechain_indexproducing a ChainComplexTermValue; consultR::cochain_complex_resolver(); callresolver.resolve(chain_bytes, out_buffer)producing a CochainComplex byte serialization per ψ_5’s identityC^k = Hom(C_k, R); emit aTermValue. Per ADR-035. -
Term::CohomologyGroups { cochain_index }— evaluatecochain_indexproducing a CochainComplexTermValue; consultR::cohomology_group_resolver(); callresolver.resolve(cochain_bytes, out_buffer)producing a CohomologyGroups byte serialization per ψ_6’s identityH^k© = ker(δ^k) / im(δ^{k-1}); emit aTermValue. Per ADR-035. -
Term::PostnikovTower { simplicial_index }— evaluatesimplicial_indexproducing a SimplicialComplexTermValue(typically aTerm::Nerveemission); consultR::postnikov_resolver(); callresolver.resolve(simplicial_bytes, out_buffer)producing a PostnikovTower byte serialization per ψ_7’s identityKanComplex(N©) → PostnikovTower— the resolver performs Kan-completion perhomology:KanComplex/HornFilleras part of itsresolvesemantics, then computes the truncation towerπ_{≤k}fork = 0..dim(N©); verb authors do not construct KanComplex values explicitly. Emit aTermValue. Per ADR-035. -
Term::HomotopyGroups { postnikov_index }— evaluatepostnikov_indexproducing a PostnikovTowerTermValue; consultR::homotopy_group_resolver(); callresolver.resolve(postnikov_bytes, out_buffer)producing a HomotopyGroups byte serialization per ψ_8’s identity extractingπ_kfrom each truncation stage; emit aTermValue. Per ADR-035. -
Term::KInvariants { homotopy_index }— evaluatehomotopy_indexproducing a HomotopyGroupsTermValue; consultR::k_invariant_resolver(); callresolver.resolve(homotopy_bytes, out_buffer)producing a KInvariants byte serialization per ψ_9’s identity computingκ_kclassifying the Postnikov-tower extensions — the canonical maximum-discriminating structural witness per the verifiability commitment per ADR-001 + ADR-019. The terminal ψ-stage of the canonical k-invariants branch per ADR-035; the verb body’s outermost emission in the canonical composition. Emit aTermValue. Per ADR-035.
The fold’s result type is the Output shape’s bytes — the catamorphism’s terminal value. Foundation populates the bytes into the Grounded’s value payload (per ADR-028) before returning.
Catamorphism parameterization in (H, B, A, R, C): The fold-rules are
parametric in the five substrate parameters per ADR-022 D5 + ADR-030 +
ADR-036 + ADR-048. PrimitiveOp's algebraic rules are determined by H
(HostTypes' value semantics); the Witt-level transitions (Lift,
Project) are bounded by B::WITT_LEVEL_MAX_BITS; binding-table
lookups consult the bindings populated through IntoBindingValue impls
(whose serialization is the application’s canonical hash axis via
ADR-023’s content-addressing); resolver-bound ψ-Term fold-rules per
ADR-035 consult R's per-category accessors at evaluation time; the
post-resolver typed-bandwidth admission per ADR-048 consults
C::evaluate(kappa_label) after ψ_9 emits the κ-label. The
catamorphism’s identity as the unique morphism from Term to the
carrier is preserved within each fixed (H, B, A, R, C) selection;
different selections produce different output values from the same Term
tree because the carrier itself differs (the H-indexed family of
catamorphisms from ADR-019’s Consequences). The architectural
commitment is that within any fixed (H, B, A, R, C), the catamorphism
is unique and deterministic — the structural-determinism property the
framework’s "structural inference" claim depends on.
Substitution-axis-realized verbs (substrate context, not verb-body
context per ADR-035): The
Term::AxisInvocation { axis_index, kernel_id, inputs } variant per
ADR-030 carries axis-trait-method dispatch through the AxisTuple. Its
fold-rule is "evaluate each input term recursively to produce a slice of
TermValue s; dispatch through <A as AxisTuple>::dispatch(axis_index,
kernel_id, &evaluated_inputs) to the right axis impl’s kernel; emit the
kernel’s result." Axes span domains: cryptographic projections
(prism-crypto’s HashAxis with kernels for SHA-256, BLAKE3, etc.),
tensor operations (prism-tensor’s TensorAxis with kernels for matmul,
conv2d, etc.), homomorphic operations (prism-fhe’s FheAxis),
high-precision arithmetic (prism-numerics’s NumericAxis), and any
application-declared axis via axis!. Per ADR-035’s ψ-residuals
discipline, Term::AxisInvocation is forbidden in verb-body terms —
the canonical hash axis is consumed type-associatedly at certificate
emission (via <A as Hasher>::initial()) and internally by resolver
impls invoked through resolver-bound ψ-Term fold-rules per ADR-036.
Term::AxisInvocation remains a substrate construct for non-verb-body
contexts: resolver bodies invoke axis dispatch internally as part of
their resolve semantics; conformance-corpus generators and
foundation-internal trace replay may exercise the variant directly. The
variant is part of the substrate’s Term enum (the tenth variant;
Term::ProjectField per ADR-033 is the eleventh; Term::FirstAdmit per
ADR-034 is the twelfth — also restricted by ADR-035 to non-verb-body
contexts; the nine ψ-Term variants per ADR-035 are the thirteenth
through twenty-first), and ADR-013’s substrate-amendment-via-foundation
rule covers each variant’s addition. The catamorphism is parametric in
(H, B, A: AxisTuple + Hasher, R: ResolverTuple) per ADR-019 +
ADR-030 + ADR-036.
Consequences: pipeline::run becomes the catamorphism in fact, not
just in name. Input bindings flow in; the Term tree’s structural fold
produces output bytes; the bytes populate the Grounded’s value payload
(per ADR-028). A model’s verb body emits a Term tree composed of the
ψ-residual-free Term variants (combinatorial PrimitiveOp-level forms
plus the nine ψ-chain variants per ADR-035), which the catamorphism
evaluates by recursive fold — resolver-bound ψ-Term fold-rules consult
the model’s R: ResolverTuple per ADR-036 for per-value content;
Term::AxisInvocation is forbidden in verb-body terms by ADR-035’s
ψ-residuals discipline (the canonical hash axis is consumed by resolvers
and by the certificate-emission stage, not by verb-body composition).
The catamorphism returns Grounded<Output, Tag> whose output_bytes()
is the actual value the route produces — for the canonical k-invariants
branch, a constant-width κ-label classifying the input’s homotopy type
up to weak equivalence. The framework’s structural-determinism property
— same input + same substrate parameters → same output, by structural
functional dependence — is foundation-realized at the evaluation level,
not just claimed in the architecture document.
ADR-019’s catamorphism framing is now backed by per-variant evaluation
semantics; the categorical claim that pipeline::run is the unique
morphism from Term is observable at the value level (two routes that
produce the same output for all inputs in a fixed (H, B, A) selection
ARE the same Term tree up to closure-body-grammar normalization, by the
catamorphism’s uniqueness).
Rejected alternative 1: Keep pipeline::run as metadata-only; the
catamorphism’s evaluation semantics live in a separate function
(pipeline::evaluate). Rejected — pipeline::run IS the catamorphism
by ADR-019; introducing a separate evaluator makes the architecture’s
categorical claims (initial algebra, catamorphism, anamorphism for
replay) inconsistent with the implementation. The catamorphism’s
identity as pipeline::run is load-bearing for ADR-019’s monomorphism
property (Section 8, Compilation as Monomorphism) — a separate evaluator
would expose two morphisms into the carrier, violating uniqueness.
Rejected alternative 2: Implement evaluation only for non-recursive
Term variants (Literal, Variable, Application, Lift, Project). Rejected
— Term::Recurse, Term::Unfold, Term::Match, Term::Try, and
Term::AxisInvocation are first-class Term variants per ADR-022 D3
G6/G7/G8/G9 and ADR-026 G19; partial evaluation makes the closure-body
grammar non-conformant and reduces the typed-iso surface to a fragment
that cannot express routes whose structural decomposition exceeds simple
primitive composition (multi-round folds, alternation matches,
failure-promotion, substitution-axis-realized verbs). Every variant in
the Term enum admits a fold-rule per the catamorphism’s defining
property; partial coverage breaks the uniqueness commitment.
Rejected alternative 3: Have the substitution-axis lane (axis impls)
carry verb evaluation entirely; keep the Term tree as the identity.
Rejected — this would make the route’s Term tree vacuous (the route
declares no transformation; the axes do everything; the Grounded attests
path metadata only). The Term tree is the load-bearing structural
declaration per ADR-019 and ADR-020; the catamorphism evaluates it;
substitution-axis delegation through Term::AxisInvocation (G19) is a
first-class mechanism for verbs whose structure exceeds substrate
primitives, not a substitute for evaluation. The Term-tree-as-identity
reading would require ADR-019’s catamorphism claim to be retracted —
there would be nothing for the catamorphism to fold over.
Rejected alternative 4: Specify evaluation semantics only at the
prose level, leaving the per-variant rules to implementation discretion.
Rejected — ADR-019’s unique catamorphism property requires the
evaluation semantics to be normative; if two implementations disagree on
a Term variant’s fold-rule, they produce different carriers and the
morphism is no longer unique. The per-variant rules above are normative
for any conformant pipeline::run.
Status: Accepted.
Context: ADR-007 specifies three substitution axes — HostTypes,
HostBounds, Hasher — as the carrier of application-side parameters
that propagate through the substrate’s catamorphism. The first two
govern the substrate’s interpretation: how values at each Witt level are
represented, and which capacity bounds are in force. The third,
Hasher, is the substrate-extension lane: it admits a typed vocabulary
of operations the substrate’s PrimitiveOp set doesn’t directly
express, with Term::HasherProjection { input_index } as the
macro-emitted form (ADR-026 G19) and <A as
Hasher>::initial().fold_bytes(...).finalize() as the per-variant
fold-rule (ADR-029).
The Hasher trait’s shape is constrained: stateful through an associated
State type, fold-rule is bytes-in-bytes-out, output is bounded by
<B as HostBounds>::TERM_VALUE_MAX_BYTES per ADR-037. This shape works
for cryptographic projections — every hash function fits the signature —
but doesn’t generalize. Operations the substrate doesn’t directly
express span far more than hashing: tensor operations (matmul, conv2d,
pooling) for ML inference; linear-algebra primitives (Gaussian
elimination, eigendecomposition); finite-field arithmetic for
ZK-friendly compute; homomorphic operations on ciphertexts for FHE;
specialized cryptographic primitives (pairings, commitments,
signatures); approximate-arithmetic operations under specific rounding
regimes. Each of these is structurally a substrate-extending vocabulary;
each requires a typed contract distinct from Hasher's
bytes-in-bytes-out shape; each is application-domain-specific in a way
that makes hardcoding the trait family at the substrate level
antithetical to the framework’s parametric-in-axes commitment.
Without a meta-mechanism for declaring substrate-extension vocabularies,
the framework is constrained to one substrate-extension axis (Hasher)
and any new domain requires either substrate amendment (extending
PrimitiveOp per ADR-013/TR-08, which limits the framework to the
operator additions foundation chooses to bless) or smuggling axis-shaped
operations through the Hasher trait by reinterpreting it (which
conflicts with Hasher’s typed contract). Neither path supports the
framework’s universal-model-compiler scope: arbitrary domain crates
declaring arbitrary substrate-extension vocabularies, each closed under
the framework’s discipline, each composable with the others within a
single model.
Decision: Foundation provides the axis! SDK macro, paralleling the
verb! SDK macro from ADR-024. Domain crates declare axis trait
extensions through the macro; the macro emits the trait declaration, the
sealed-trait marker, the AxisExtension impl, the kernel-identifier
consts, and the dispatch glue the catamorphism uses. The architecture
commits to the meta-mechanism (the axis! macro’s emission pattern, the
closure check it performs at invocation, the AxisExtension trait
family’s bounds) rather than to specific axis traits.
The macro’s emission shape. For an application-declared axis trait:
axis! {
/// A linear-algebra axis providing matrix and tensor operations.
pub trait LinearAlgebra: AxisExtension {
type Element;
const MAX_OUTPUT_BYTES: usize;
fn matmul(a: &[u8], b: &[u8], dims: MatMulDims) -> [u8; Self::MAX_OUTPUT_BYTES];
fn conv2d(input: &[u8], filter: &[u8], params: Conv2DParams) -> [u8; Self::MAX_OUTPUT_BYTES];
// ... domain-specific kernel methods
}
}The macro emits, for each declared axis trait:
-
The trait declaration with the application-specified methods, marked
puband bounded onAxisExtension -
An impl __sdk_seal::Sealed for <every conforming impl> blanket gate, paralleling how
Hasheris sealed today and howFoundationClosedandPrismModelare sealed via ADR-022 D1 -
A blanket impl<T: <TraitName>> AxisExtension for T {} registering the trait as a sanctioned axis (with
AxisExtensionfoundation-defined as a sealed marker trait whose impl is gated by the macro lane) -
A
pub const AXIS_ADDRESS: ContentAddressfor content-addressing the axis trait itself, derived from the trait’s name + method signatures + bounds via the foundation’s content-addressing per ADR-017 -
A pub const KERNEL_<NAME>: u32 per method, identifying each kernel deterministically within the axis (the kernel_id used in
Term::AxisInvocation) -
A blanket impl<T: <TraitName>> AxisDispatch for T emitting a
dispatch_kernel(kernel_id: u32, inputs: &[TermValue]) → TermValuemethod generated from the trait’s method set, with a const-evaluable match onkernel_idmapping to the rightT::method(…)call
The Term enum’s commitment. Term::HasherProjection generalizes to
Term::AxisInvocation { axis_index: u32, kernel_id: u32, inputs: TermList }.
The Term enum stays at ten variants under this ADR — AxisInvocation
replaces HasherProjection — with subsequent variants added by
ADR-033/034/035. Hasher becomes the first axis declared via the new
meta-mechanism (the prism-crypto standard-library sub-crate per ADR-031
declares it as HashAxis). Under ADR-035’s ψ-residuals discipline,
Term::AxisInvocation is forbidden in verb-body terms; the canonical
hash axis is consumed type-associatedly at the certificate-emission
stage (via <A as Hasher>::initial() per ADR-022 D5 + ADR-036) and
internally by resolver impls invoked through resolver-bound ψ-Term
fold-rules (ADR-036). Term::AxisInvocation remains in the substrate’s
Term enum for non-verb-body contexts (resolver bodies,
conformance-corpus generators, foundation-internal trace replay) but is
rejected at proc-macro expansion when emitted from a verb body’s
closure-grammar parse. The hash(…) identifier remains a reserved
macro-vocabulary identifier per ADR-026 G12; its closure-body emission
lowers to Term::AxisInvocation (kernel_id = HashAxis::KERNEL_HASH),
which the ψ-residuals walk rejects when emitted from a verb body.
The substitution-axis triple’s structure. PrismModel’s signature
evolves from <H: HostTypes, B: HostBounds, A: Hasher> to <H:
HostTypes, B: HostBounds, A: AxisTuple>, where AxisTuple is a
foundation-defined trait impl’d for tuple types up to a foundation-fixed
maximum arity (MAX_AXIS_TUPLE_ARITY, paralleling other
foundation-fixed ceilings like ROUTE_INPUT_BUFFER_BYTES). The trait
carries the dispatch surface:
pub trait AxisTuple: __sdk_seal::Sealed {
fn dispatch(axis_index: u32, kernel_id: u32, inputs: &[TermValue]) -> TermValue;
}
impl<A1: AxisExtension> AxisTuple for (A1,) {
fn dispatch(axis_index: u32, kernel_id: u32, inputs: &[TermValue]) -> TermValue {
match axis_index {
0 => A1::dispatch_kernel(kernel_id, inputs),
_ => panic!(...),
}
}
}
impl<A1: AxisExtension, A2: AxisExtension> AxisTuple for (A1, A2) { /* ... */ }
// ... up to MAX_AXIS_TUPLE_ARITYFoundation provides AxisTuple impls for tuples up to the
foundation-fixed max arity. A model that uses three axes selects
A = (MyHasher, MyTensor, MyActivation); the macro emits
Term::AxisInvocation s with axis_index ∈ {0, 1, 2} per which axis each
operation invokes; the catamorphism dispatches through the tuple-typed
A::dispatch(…) to the right impl’s method. Static dispatch through
monomorphization at the model’s compile time — no runtime dispatch
table, no trait-object boxing.
The catamorphism’s per-variant fold-rule for AxisInvocation.
Foundation’s evaluate_term_tree<A: AxisTuple> extends with the
per-variant rule for Term::AxisInvocation: evaluate each input term
recursively to produce a TermValue slice; dispatch through
A::dispatch(axis_index, kernel_id, &evaluated_inputs) to the right
axis impl’s kernel; emit the result as the variant’s evaluation output.
The fold-rule replaces the existing Term::HasherProjection fold-rule
(which is now subsumed by the AxisInvocation rule with HashAxis as the
axis selection).
Closure check at axis! invocation. The macro verifies that the
trait’s bounds satisfy AxisExtension's contract: sealed via
__sdk_seal::Sealed; deterministic per fixed axis impl (no global
state, no thread-local state); #![no_std]-clean (no heap allocation
in kernel bodies); output-bounded (every kernel’s output fits within
MAX_OUTPUT_BYTES ≤ <B as HostBounds>::AXIS_OUTPUT_BYTES_MAX per
ADR-037); kernel count bounded (MAX_KERNELS_PER_AXIS, a
foundation-vetted type-system impl-table-style cap); method signatures
admissible (byte-slice inputs, byte-array output, no generic lifetimes
other than 'static, no associated types beyond foundation-sanctioned
ones). The trait is registered with a content-addressed AXIS_ADDRESS
derived from the trait’s structural fingerprint.
Closure check at prism_model! invocation. The model’s A
parameter is (A1, A2, …, An) for some n ≤ MAX_AXIS_TUPLE_ARITY. Each
axis-trait-method invocation in the closure body resolves to a known
(axis_index, kernel_id) pair: axis_index is determined by the
position in the model’s AxisTuple; kernel_id is determined by which
method is invoked (the axis! macro emits a KERNEL_<NAME> const for
each method). The closure-body grammar’s identifier-resolution order
extends with axis-trait method names per the canonical ordering
specified in ADR-026 G12: (1) reserved macro-vocabulary identifiers
(parallel, fold_n, tree_fold, first_admit, partition_product,
partition_coproduct, hash, plus the named grammar forms whose
identifiers are reserved per ADR-022 D3 — recurse for G7, unfold for
G8, lift for G4, project for G5, plus the ψ-chain Term grammar forms
per ADR-035 — nerve for G21, chain_complex for G22,
homology_groups for G23, betti for G24, cochain_complex for G25,
cohomology_groups for G26, postnikov_tower for G27,
homotopy_groups for G28, k_invariants for G29); (2) PrimitiveOp
identifiers per G3a from foundation’s canonical PrimitiveOp enum at
any committed snapshot per ADR-013/TR-08; (3) axis-trait method
identifiers from the model’s declared AxisTuple (this ADR’s addition
to the resolution order); (4) own-implementation verbs from
verb!-emitted set; (5) verbs from use_verbs! imports. Identifiers
matching none of these are closure violations. Binary-operator forms per
ADR-022 D3 G3b are recognized at expression syntax level before
identifier resolution and don’t participate in the resolution order.
Cross-axis composition. A model that uses operations from multiple
axes (e.g., LinearAlgebra::matmul + HashAxis::sha256) invokes both
through Term::AxisInvocation with different axis_indices. The
catamorphism evaluates each as a leaf in the term tree (with its inputs
evaluated first); the term tree’s flat structure carries the composition
without any axis impl needing to know about the others. Axis impls are
independently verifiable, no inter-axis dependencies, the term tree is
the only composition surface.
Per-axis output buffering. Each axis trait declares its
MAX_OUTPUT_BYTES const, bounded above by
<B as HostBounds>::AXIS_OUTPUT_BYTES_MAX per ADR-037 (migrated from
the prior foundation-fixed AXIS_OUTPUT_BYTES_CEILING; parallels
<B as HostBounds>::ROUTE_OUTPUT_BUFFER_BYTES from ADR-028
reconciliation). The catamorphism’s TermValue carries the output bytes
in a buffer sized to the AxisTuple’s max-output-bytes-across-all-axes.
Models declaring axes whose MAX_OUTPUT_BYTES exceeds the
application-selected ceiling are rejected at validation time with a
PipelineFailure::ShapeViolation carrying the IRI
https://uor.foundation/pipeline/AxisOutputShape/maxBytes.
Consequences: Foundation’s substrate-extension lane is universal.
Domain crates declare their axes through axis! and contribute them to
the ecosystem; applications compose axes from any number of domain
crates within a single model. The closure discipline applies per-axis at
compile time. The Term enum stays at ten variants under this ADR (the
original nine plus AxisInvocation replacing HasherProjection);
ADR-033 subsequently adds an eleventh variant ProjectField for
product-shape field access through TR-08’s substrate-amendment rule, and
ADR-034 adds a twelfth variant FirstAdmit for bounded search with
structural short-circuit. The catamorphism’s per-variant fold-rules
cover every substrate-extending operation through the single
AxisInvocation rule. Hasher migrates from special-case axis to one
axis among many — declared by the prism-crypto standard-library
sub-crate (per ADR-031) as the HashAxis trait, with concrete impls
(Sha256Hasher, Blake3Hasher, etc.) provided by the same sub-crate.
ADR-036 extends the model declaration’s parameter shape with a fourth
substrate parameter R: ResolverTuple, paralleling the AxisTuple
mechanism. Both parameters are tuple-of-bounded-types per the same
architectural pattern; the architectural separation is per-domain
operation kernels (AxisTuple — the substitution-axis mechanism for
application-domain extension; axis methods are type-associated; no
per-instance state) versus per-value content provision
(ResolverTuple — the resolver mechanism for resolver-bound substrate
operations per ADR-035; resolver resolve methods take &self;
resolver instances carry application-specific configuration). The
asymmetric threading through run_route reflects this separation: the
AxisTuple flows as a type parameter only (its methods are
type-associated; the canonical hash axis is invoked via
<A as Hasher>::initial()); the ResolverTuple flows as both a type
parameter and a value reference (resolvers: &R). ADR-035’s ψ-residuals
discipline forbids Term::AxisInvocation in verb-body terms — the
canonical hash axis is consumed by resolvers (the ResolverTuple per
ADR-036), not by verb-body composition; Term::AxisInvocation belongs
in resolver bodies, not in verb bodies.
The architecture admits the universal-model-compiler scope: tensor
compute (the prism-tensor standard-library sub-crate declares
TensorAxis, ActivationAxis); cryptographic compute (the prism-crypto
standard-library sub-crate declares HashAxis, CurveAxis,
SignatureAxis, CommitmentAxis); homomorphic encryption (the
prism-fhe standard-library sub-crate declares FheAxis); high-precision
arithmetic (the prism-numerics standard-library sub-crate declares
NumericAxis per arithmetic-domain). Architecture-specific compositions
(transformer blocks, convolutional networks, state-space models, etc.)
and format-import tools (graph-format-to-prism_model! translators for
ONNX, GGUF, TensorFlow GraphDef, PyTorch JIT, and others) are
third-party crates consuming the standard-library vocabularies — the
architecture admits them through the same Layer-3 closure pattern
without privileging specific formats or architectures. Each domain’s
vocabulary is a Layer-3 crate per ADR-024’s three-layer closure spine;
each vocabulary is closed under the framework’s discipline; the axis!
macro is the universal declaration mechanism.
Capacity-bound reconciliation per ADR-037. ADR-030 references two
foundation-fixed caps: MAX_AXIS_TUPLE_ARITY and
AXIS_OUTPUT_BYTES_CEILING. Per ADR-037, these are reconciled
differently:
-
AXIS_OUTPUT_BYTES_CEILINGis a data-shape cap (the per-axis kernel output byte-buffer ceiling). It migrated to<B as HostBounds>::AXIS_OUTPUT_BYTES_MAXper ADR-037’s clause (1). Superseded by ADR-060: this byte-width cap is removed — axis kernels emit a source-polymorphicTermValue(Inlineof foundation-derived width,Borrowed, orStream) with no separate output byte-width ceiling, andDefaultHostBoundsis removed. -
MAX_AXIS_TUPLE_ARITYis a type-system impl-table cap (foundation’sAxisTupleblanket-impl macro emission limit). Per ADR-037’s clause (2), it stays foundation-vetted with explicit Rust-language carve-out: Rust’s lack of variadic generics requires per-arity impl emission at foundation’s build time, which cannot be parametric on downstream applications'HostBoundsimpls. The cap is foundation-vetted, motivated by current standard-library Layer-3 sub-crate AxisTuple usages plus headroom. Foundation revision adjusts the value when standard-library or application needs evolve.
Rejected alternative 1: Keep Hasher as a special-case axis with
Term::HasherProjection as its dedicated Term variant; add a separate
Term::AxisInvocation variant for non-Hasher axes. Rejected — this
creates two parallel mechanisms for the same architectural concern
(substrate extension), violating the "one path" discipline the framework
otherwise holds to. The Term enum extends to eleven variants, the
architectural commitment to ten is broken, and the conformance check has
to handle two patterns where one would suffice.
Rejected alternative 2: Commit the architecture to a fixed family of
axis traits (Hasher, LinearAlgebra, Activation, NumericPrecision, etc.)
with each axis getting its own Term variant. Rejected — every new domain
that needs a substrate-extension lane requires foundation amendment per
ADR-013/TR-08, which is structurally too heavy a process for the
framework’s universal-model-compiler scope. The axis! meta-mechanism
keeps foundation small while admitting open-ended domain extension.
Rejected alternative 3: Generalize the Hasher trait to bundle multiple kernel methods, treating it as a single god-trait whose impls cover whatever an application needs. Rejected — loses per-kernel type safety (the Term variant carries opaque kernel_id rather than a typed reference); makes the trait’s method set unbounded; conflates conceptually-distinct axes (cryptographic projections, tensor operations, FHE operations) into one trait that no impl can cleanly satisfy.
Rejected alternative 4: Have axis impls compose with each other
directly (axis_a’s body calling axis_b’s methods). Rejected — admits
inter-axis dependencies that complicate the closure check (a cycle
through axis composition would require runtime detection paralleling the
EVALUATE_TERM_TREE_DEPTH_LIMIT mechanism that ADR-024 explicitly
rejected). Composition happens at the term-tree level: each axis impl
operates on byte slices and emits byte slices, with the term tree
carrying the composition through the catamorphism’s evaluation order.
ADR-031 — prism is the standard library: a façade over uor-foundation plus standard-library Layer-3 sub-crates published from the Prism repository
Status: Accepted.
Context: ADR-024 commits to three layers of algebraic closure with
implementation closure as Layer 3 — each implementation declares verbs
(named compositions of prism operators applied to substrate primitives)
and, per ADR-030, axes (substrate-extension vocabularies declared via
axis!). Layer-3 crates are how domain knowledge enters the framework:
a cryptographic-substrate crate declares cryptographic axes and verbs,
an FHE-substrate crate declares FHE axes, a tensor-compute crate
declares tensor axes. The architecture admits Layer-3 crates uniformly —
same closure discipline, same SDK-macro surface, same
content-addressing.
ADR-015 commits to a repository allocation: uor-foundation lives in
the UOR-Framework repository alongside the wiki; prism and
prism-verify live in the Prism repository. That allocation places
the architecture’s normative specification (the wiki) and its Rust
implementation (uor-foundation) in the same repository, and places the
Prism runtime + replay surface in their own repository. ADR-015 names
the split but does not yet specify what prism is relative to
uor-foundation — whether it is an independent crate carrying its own
concepts, or a façade re-exporting uor-foundation's vocabulary, or a
runtime layered atop uor-foundation.
Without a structural commitment about that relationship, two
ecosystem-organization gaps open. First, application authors cannot tell
whether to depend on uor-foundation, on prism, or on both, and what
is in scope for each. Second, the question of which Layer-3 crates are
foundation-maintained versus which are third-party is unanswered: every
application either declares its own axes (duplicating effort across
applications, breaking interoperability when two applications declare
structurally-different axes for the same conceptual operation) or pulls
from arbitrary third-party crates (with no guarantee of conformance, no
recommended-for-production status, no version coordination across the
ecosystem).
The pattern AGENTS.md §11 already commits to for prism::std_types
(foundation-maintained baseline-primitive types with explicit
inclusion/exclusion criteria) extends naturally: prism is the
standard library, hosted in the Prism repository, realized as a
façade crate plus Layer-3 sub-crates published alongside it. The façade
re-exports the prism architecture from uor-foundation together with
the built-in types and built-in axes the standard-library Layer-3
sub-crates declare. Third-party crates carry application-specific or
research-oriented extensions; the architecture treats standard-library
and third-party Layer-3 crates identically, with the distinction being
maintenance and conformance rather than structural.
Decision: The prism crate is the standard library. Per ADR-005,
prism carries the Prism runtime — the pipeline, the three
Prism-mechanism sealed types (Validated, Grounded, Certified), the
operation-declaration vocabulary, the standard type library, and the
replay component — all closed under uor-foundation's substrate
vocabulary per ADR-013. Per this ADR, prism additionally serves as a
standard-library façade over uor-foundation: it re-exports the
substrate’s vocabulary from uor-foundation (Term, PrismModel, the
AxisExtension/AxisTuple machinery, the SDK proc-macro entry points
exposed via uor-foundation-sdk per ADR-022, the four UOR-domain sealed
types, the wire-format type definitions, the mint primitives, the
substitution-axis trait surface) and re-exports the built-in types and
built-in axes the standard-library Layer-3 sub-crates declare. The
architectural commitment is closure under uor-foundation (per
ADR-013): every type prism exposes derives from foundation’s
substrate; the runtime mechanics, the standard type library, and the
standard-library sub-crates' built-ins all close under it. prism
introduces no new substrate concepts — its additions are runtime
mechanism (per ADR-005), pre-declared types built from foundation’s
vocabulary (per ADR-013’s standard-library commitment), and curated
re-exports (per this ADR).
The repository allocation. The UOR-Framework repository hosts the
architecture: the wiki (this document, the normative specification) and
the uor-foundation Rust crates (the architecture’s Rust
implementation, including any internal sub-crates such as
uor-foundation-sdk and uor-foundation-macros per Cargo packaging
detail). The Prism repository hosts the standard library: the prism
façade crate, the standard-library Layer-3 sub-crates that contribute
the built-in types and axes prism re-exports, and prism-verify (the
replay-surface façade per ADR-005). Per ADR-007 the three substitution
axes' definitional surface lives in uor-foundation (foundation
defines, prism bounds, author selects); the standard-library Layer-3
sub-crates contribute built-in selections an application author may
choose via the AxisTuple mechanism (per ADR-030), but the
substitution-axis trait surface itself is in uor-foundation.
The standard-library Layer-3 sub-crate category. A Layer-3 crate is
a standard-library sub-crate if and only if it is published from the
Prism repository under foundation maintenance and satisfies the
inclusion criteria below. The category is operational, not
architectural: the closure discipline applies the same way to
standard-library and third-party Layer-3 crates; the axis! macro
performs the same closure check; content-addressing is invariant. What
standard-library inclusion changes is maintenance responsibility,
conformance-test ownership, recommended-for-production status, and the
canonical-reference role for the axes the sub-crate declares.
Inclusion criteria. A Layer-3 sub-crate qualifies for inclusion in the standard library if and only if all of the following hold:
-
Application-neutral. The sub-crate’s axes and verbs are reusable across multiple unrelated applications. A canonical
HashAxisis reused across content-addressing, signature-verification, ZK proof systems, and any other application that consumes a content-address; a canonical compound-arithmetic verb is reused across any ring-arithmetic application. By contrast, a third-party crate’s application-specific verbs (verbs that target one specific application or one specific protocol) are not reusable in this sense and remain third-party rather than standard-library. The reusability criterion is substrate-faithful: under the UOR framework every operation decomposes to substratePrimitiveOpcompositions irrespective of any conventional library categorization, so "application-neutral" is the structural criterion; conventional groupings (numeric / cryptographic / tensor / FHE) are operational presentation conventions that help authors discover canonical references, not architectural partitions. -
Built on foundation primitives + uor-prism std_types + lower standard-library sub-crates. Each sub-crate’s axes and verbs decompose to operations from the substrate, the standard library’s baseline-primitive types, and the layered standard-library sub-crates structurally below it (per the dependency graph below). No standard-library sub-crate depends on third-party Layer-3 crates.
-
Content-addressed per ADR-017’s closure rule. The sub-crate’s axes use
axis!-emittedAXIS_ADDRESScontent-addressing; the sub-crate’s verbs useverb!-emitted content-addressing; the sub-crate’s shapes useoutput_shape!/etc. content-addressing per ADR-017. The Rust crate name is for the developer; the content-address is for the ecosystem. -
Conformance-tested against canonical reference vectors. The sub-crate maintains a conformance test suite analogous to the substrate’s catalog and transition tables (per ADR-025). Each axis impl in the sub-crate is checked against canonical input-output pairs (e.g., a SHA-256 impl is checked against FIPS-180-4 test vectors). The conformance suite is published as test data the application’s CI can replay.
-
Compile-time stable. All axis kernels resolve at compile time (per ADR-030’s static-dispatch commitment); no runtime allocation, no runtime trait dispatch.
-
#![no_std]-clean. Compiles without
allocorstdon embedded targets, paralleling theprism::std_typespolicy from AGENTS.md §11.1.
The standard-library sub-crate roster (operational organization).
The standard library’s current operational decomposition into Layer-3
sub-crates is listed below. The decomposition is operational, not
architectural: the substrate evaluates against the canonical reference
set (canonical shapes, canonical axes, canonical verbs) regardless of
which sub-crate publishes which canonical reference, and the substrate’s
PrimitiveOp vocabulary admits no notion of "domain" or "category." The
sub-crate boundaries are a packaging convention that helps developers
discover canonical references and that aligns maintenance responsibility
with subject-matter expertise; the architectural commitments — the
closure discipline per ADR-024, the content-addressing rule per ADR-017,
the conformance discipline per this ADR, the substrate-Term-verb-body
discipline per ADR-054 — apply uniformly across the roster. Reorganizing
the roster (splitting, merging, or renaming sub-crates) is admissible
operational policy so long as the canonical-reference set and the
disciplines above are preserved.
-
prism-numerics — the numerics-domain sub-crate. Per ADR-050 + ADR-053, substrate-native ring arithmetic on
Z/(2^n)Zis closed underPrimitiveOp::{Add, Sub, Mul, Div, Mod, Pow}evaluated at the full Witt tower; substrate-native hypercube arithmetic onF_2^nis closed underPrimitiveOp::{Xor, And, Or, Bnot}. These operations are substrate primitives — verbs in prism-numerics never re-implement them at the axis-kernel layer. The numerics sub-crate’s role shifts from "declaring arithmetic axes" to publishing shapes plus compound arithmetic verbs (modexp_p,polyeval,gcd,ext_euclidean,horner,newton_step,fma,field_add<P>,field_sub<P>,field_mul<P>,field_inv<P>). Each compound verb is a single named transformation composing multiple substrate primitives (per ADR-024); operations realizable as a single folding-transformation (Div,Mod,Pow) are substrate primitives per ADR-053, not verbs. TheBigIntAxis,FixedPointAxis,RingAxisdeclarations dissolve into the substrate’sPrimitiveOpcatalog at the appropriate Witt-level instantiation; theFieldAxislane is retained for prime parametricity (eachPrimeFieldNumeric<P>instantiation is a distinct axis instance per ADR-007, since prime-field arithmetic mod-p requires composition over substrate primitives that is not a single folding-transformation). Shape declarations remain:BigInt<MaxBits>,FixedPoint<I, F>,FieldElement<P>,Polynomial<MaxDegree, Coeff>. The dissolution is enabled by ADR-052’s axis-generic SDK emission (parametric Layer-3 axes that survive —MerkleRoot<H, LEAF_BYTES>,CpuI8MatmulSquare<DIM>,OneTimePadFhe<BLOCK_BYTES>,PrimeFieldNumeric<P>— drop their hand-writtenAxisExtensionboilerplate to the generic-form companion). -
prism-crypto — the cryptography-domain sub-crate. Carries
HashAxis(canonical hash families: SHA-2, SHA-3, BLAKE3, Poseidon),CurveAxis(elliptic-curve operations: scalar mul, point add, pairing),SignatureAxis(signing/verification: Ed25519, ECDSA, BLS, Schnorr),CommitmentAxis(Pedersen, KZG, Merkle). Concrete impls per primitive:Sha256Hasher,Sha512Hasher,Blake3Hasher,KeccakHasher,PoseidonHasher,Secp256k1,Ed25519Curve,Bls12_381,BN254. Verbs: HMAC, HKDF, ECDSA-with-RFC6979, Merkle-tree construction (via tree_fold). Shape declarations:Digest<32>,Digest<64>,Signature<64>,PublicKey<32>,MerkleProof<MaxDepth>. TheHashertrait that ADR-007 originally named becomes one axis among many — declared by prism-crypto asHashAxisand consumed through the AxisTuple mechanism. -
prism-tensor — the tensor-compute sub-crate. Carries
TensorAxis(matmul, conv2d, transposed-conv, pooling, normalization, reduction),ActivationAxis(element-wise nonlinearities). Multiple impls per axis:CpuFp32Tensor,CpuI8Tensor,CpuFixedPointTensor(the integer-arithmetic impls preserve bit-determinism per fixed (H, B, A); the floating-point impls do not, per ADR-030’s per-axis substitution-determinism note). Verbs for compositional tensor patterns whose decomposition is format-neutral: matrix-vector multiplication, batched matmul, softmax-with-cross-entropy, layer-normalization. Shape declarations:Tensor<Element, Shape>parameterized over element type and dimensional shape. The sub-crate carries domain-neutral tensor compute primitives; specific model-format imports (graph-format-to-prism_model!translation tools) and architecture-specific compositions (transformer blocks, convolutional networks, recurrent architectures, state-space models) live in separate third-party crates that consume prism-tensor’s vocabulary — not in the standard library itself. -
prism-fhe — the homomorphic-encryption sub-crate. Carries
FheAxis(homomorphic add, mul, rotation, key switching, bootstrapping). Multiple impls per FHE scheme:TfheBoolean,TfheInteger<N>,BgvLevelled<L>,CkksApproximate. Verbs: PBS-based comparison, encrypted lookup tables, polynomial evaluation over ciphertexts. Shape declarations:Ciphertext<Plaintext, Scheme>content-addressed by the plaintext type’s IRI plus the scheme parameters.
Conventional shape and axis naming. The standard library uses
conventional programming-language and mathematical-library names for
shapes and axes where they aid discoverability — BigInt<MaxBits>,
FixedPoint<I, F>, Tensor<Element, Shape>, Digest<N>, HashAxis,
FieldAxis, TensorAxis. These names are aliases for substrate-level
constructions: BigInt<MaxBits> is conventionally named after the
arbitrary-precision integer pattern but operationally is a
ConstrainedTypeShape over Z/(2^MaxBits)Z at the corresponding Witt
width; FixedPoint<I, F> is conventionally named after the fixed-point
arithmetic pattern but operationally is a ConstrainedTypeShape over
Z/(2^(I+F))Z with an interpretation convention for the radix point;
Digest<N> is conventionally named after the cryptographic-hash output
but operationally is a ConstrainedTypeShape over an N-byte sequence
with no algebraic-law commitment. The naming convention preserves
familiarity for application authors familiar with conventional
libraries; the substrate treats the constructions through the
ConstrainedTypeShape contract regardless of name. Authors implementing
custom shapes are free to use substrate-faithful names (RingValue<W>,
ByteSequence<N>) or conventional names interchangeably; the
content-address (per ADR-017) depends on structural content, not on the
chosen identifier.
Layered consumption pattern. The standard-library sub-crates form a
layered dependency graph: each sub-crate depends only on what’s
structurally below it. prism-numerics depends on uor-foundation only.
prism-crypto depends on uor-foundation and (for some verbs)
prism-numerics. prism-tensor depends on uor-foundation,
prism-numerics (for fixed-point and quantized arithmetic), and (for
cryptographic tensor commitments where applicable) optionally
prism-crypto. prism-fhe is independent (depends on uor-foundation
only; the cryptographic primitives an FHE scheme uses are
scheme-internal, not consumed from prism-crypto). The prism façade
depends on uor-foundation and on every standard-library sub-crate,
re-exporting the curated subset that constitutes the standard library’s
public surface. Cross-cutting standard-library sub-crates may exist; the
architecture admits them under the same inclusion criteria.
The prism façade’s re-export surface. prism re-exports from
uor-foundation the architecture’s public types and macros (Term,
PrismModel, AxisExtension, AxisTuple, the SDK proc-macro entry points
exposed via uor-foundation-sdk per ADR-022, the four UOR-domain sealed
types, the wire-format definitions, the mint primitives, the
substitution-axis trait surface). prism re-exports from each
standard-library sub-crate the built-in axes, axis impls, verbs, and
shape declarations the sub-crate publishes. Application authors write
use prism::* (or finer-grained imports such as
use prism::crypto::Sha256Hasher); they do not need to depend on
uor-foundation or on individual sub-crates directly. The façade
indirection is what lets the standard library evolve its sub-crate
decomposition without breaking application code: the re-export surface
stays the same; sub-crate refactors are invisible to application
authors.
Application crates (third-party Layer-3 implementations) depend on
prism for the standard-library vocabulary they consume and for the SDK
macros (themselves re-exported through prism) used to declare their
own axes and verbs. A protocol-specific application crate (e.g., a crate
targeting one cryptographic protocol or one search domain) depends on
prism and consumes the relevant standard-library axes
(prism::crypto, prism::numerics, etc.) while contributing its own
protocol-specific verbs as named compositions. Architecture-specific
compute crates (transformer-architecture crates, convolutional-network
crates, state-space-model crates, etc.) depend on prism and contribute
their architecture-specific verbs (e.g., a transformer-block verb
composing the standard-library tensor-axis primitives). Format-import
tools (graph-format-to-prism_model! translators for arbitrary external
model formats) consume prism::tensor as a target vocabulary; the
architecture admits any number of such tools without committing to
specific formats. Cross-domain applications combining e.g. tensor
inference with cryptographic commitments depend on prism (consuming
prism::tensor + prism::crypto together through a single AxisTuple).
Content-addressing across the ecosystem. The closure rule (per
ADR-017) makes IRIs content-deterministic. Each sub-crate’s axes have
content-derived AXIS_ADDRESS values; two crates declaring
structurally-identical axes (same trait name in the structural sense,
same method signatures, same bounds) content-address identically. The
standard-library sub-crate’s role is to be the canonical reference: when
prism-crypto declares HashAxis with specific method signatures, that
declaration becomes the canonical reference for that axis’s
content-address. Other crates that declare structurally-identical axes
content-address to the same identity; structurally-different axes
content-address differently. Standard-library inclusion is about who
maintains the canonical reference, not about who owns the IRI namespace.
Conformance vetting. Each standard-library sub-crate maintains a conformance test suite analogous to the substrate’s catalog and transition tables (per ADR-025). The conformance suite contains canonical input-output pairs per axis kernel, sourced from the relevant standards: prism-crypto’s HashAxis tests against FIPS-180-4 (SHA-256), FIPS-202 (SHA-3), RFC 7693 (BLAKE2/3), and the relevant published vectors per primitive; prism-numerics tests against multi-precision-arithmetic test corpora; prism-tensor tests against published reference vectors for canonical tensor operations (matmul correctness against BLAS reference outputs at integer precision; conv2d correctness against published reference impls); prism-fhe tests against the FHE scheme’s published correctness predicates. The conformance suite is the structural-reference for the sub-crate’s impls; impls that fail the conformance check are non-conformant.
Canonical axis impl body discipline (per ADR-054 + ADR-055 universal
enforcement). Every canonical axis implementation the standard-library
Layer-3 sub-crates publish carries a substrate-Term verb body. The
axis surface (declaration via axis! per ADR-030) remains as the
typed-extension contract; the body is realized as a verb!-emitted Term
composition over substrate PrimitiveOp s and prism operators per
ADR-024. This applies uniformly: prism-crypto’s HashAxis canonical
impls (Sha256Hasher, Sha512Hasher, Sha3_256Hasher, KeccakHasher,
Blake3Hasher) realize their compression functions as substrate-Term
verbs composing W32 / W64
PrimitiveOp::{Add, Xor, And, Or, Bnot, Div, Mul} plus rotate;
prism-numerics' FieldAxis canonical impl
(PrimeFieldNumericSecp256k1) realizes its kernel methods as
substrate-Term verbs composing the substrate’s six ring primitives at
W256 plus mod-P reduction; prism-tensor’s TensorAxis /
ActivationAxis canonical impls realize matmul / activation kernels as
substrate-Term verbs composing W8 / W16 / W32 substrate primitives plus
sign-extension verbs; prism-fhe’s FheAxis canonical impl
(OneTimePadFhe) realizes encrypt/decrypt as substrate-Term Xor
composition. Per ADR-055’s universal substrate-Term verb body
discipline, the body discipline extends to every AxisExtension
impl (standard-library AND application-author custom) via the
foundation-declared SubstrateTermBody sealed supertrait bound on
AxisExtension — axis impls that fail to provide a body_arena()
decomposition fail to satisfy the supertrait bound and fail to compile.
The discipline is the architectural mechanism that makes the
catamorphism’s structural reach extend to the leaf level across every
axis surface for every axis impl; there is no opaque axis-kernel
boundary anywhere in any conforming implementation.
Consequences: The architecture commits to a specific repository
allocation (architecture in UOR-Framework; standard library in
Prism) and to prism as a façade re-exporting uor-foundation's
architecture plus the standard-library sub-crates' built-in types and
built-in axes. The closure discipline applies uniformly across
standard-library and third-party Layer-3 crates. Application authors
writing models against prism consume foundation-vetted impls of the
axes their model uses; switching impls within an axis (e.g., from
Sha256Hasher to Blake3Hasher) is a substitution-axis selection that’s
structurally well-defined. The dependency graph from uor-foundation
through the standard-library sub-crates to applications is acyclic (per
ADR-024’s verb-graph acyclicity, extended to the sub-crate layering).
The standard-library ecosystem realizes prism’s universal-model-compiler
scope at the developer-facing surface: a developer writing a model
selects axes from the standard library (or from third-party crates
declaring their own axes), composes the model through the closure-body
grammar, and compiles to a foundation-sealed Grounded carrying the
typed-iso path attestation and the output value. The same
developer-facing surface compiles a content-addressing search (using
prism::crypto's HashAxis), a keyed-MAC computation (using
prism::crypto's HMAC verb composed over a HashAxis selection), a
tensor-compute inference (using prism::tensor's TensorAxis composed
with the architecture-specific verbs an architecture-specific crate
provides), or an FHE-encrypted computation (using prism::fhe's
FheAxis composed with prism::tensor's TensorAxis under the FHE
scheme’s homomorphic operations).
ADR-036 introduces resolver baselines as a parallel category to the
standard-library axis baselines. Per this ADR’s "prism is the standard
library" framing, the standard library’s sub-crates may contribute
application-neutral resolver baselines (e.g., a
ConstraintNerveResolver for numerical constraints contributed
alongside numerical canonical references; resolvers that compose with
cryptographic Hashers contributed alongside cryptographic canonical
references). The closure discipline applies identically to
standard-library and third-party resolvers — both are
application-provided, both go through the resolver! macro per ADR-036,
both are seal-checked at proc-macro expansion. Standard-library resolver
baselines have no foundation-special status; they are sub-crates of
prism with operational distinctions (maintenance, conformance test
ownership, recommended-for-production status) but no architectural
distinction.
Rejected alternative 1: Foundation maintains all Layer-3 crates; no third-party Layer-3 crates exist. Rejected — Layer-3 closure (per ADR-024) admits any conformant verb declaration; restricting to foundation-maintained crates would block the framework’s universality and require foundation to own every domain’s verbs (impossible at scale).
Rejected alternative 2: No standard-library sub-crates; all Layer-3
crates are third-party, and prism is just a re-export of
uor-foundation. Rejected — leaves the canonical-reference role for
axes uninstantiated; two third-party crates declaring SHA-256 axes with
subtly-different signatures would content-address differently and
fragment the ecosystem; applications would have no foundation-maintained
vocabulary to depend on for application-neutral domains.
Rejected alternative 3: prism is a single monolithic crate
carrying the standard-library vocabulary directly (rather than
re-exporting from sibling sub-crates). Rejected — couples the standard
library’s release cadence across all domains; adding a new domain’s
vocabulary requires editing prism itself rather than publishing a new
sibling sub-crate; #![no_std]-cleanliness guarantees become
per-feature-flag rather than per-crate. The façade-plus-sub-crates
structure preserves modularity (each domain ships its own crate) while
keeping the application-facing import surface unified (use prism::*).
Rejected alternative 4: Standard-library sub-crates own IRI
namespaces (e.g., https://prism-crypto.uor.foundation/axis/HashAxis).
Rejected — violates ADR-017’s closure rule (IRIs are content-derived,
not namespace-claimed). Two standard-library sub-crates that declared
the same axis under different namespace-claims would content-address
differently, breaking the structural-identity guarantee. The
standard-library sub-crate’s role is canonical maintenance, not
namespace ownership.
Rejected alternative 5: Each standard-library sub-crate has its own independent versioning and dependency graph (potentially circular). Rejected — the layered dependency graph (numerics → crypto, tensor; fhe independent) is structurally important: it preserves the closure discipline at the ecosystem level (cycles through sub-crates would mirror the cycles through verbs that ADR-024’s acyclicity check rejects); it enables consistent versioning (a sub-crate’s release coordinates with the layers below); it makes the ecosystem reasoning tractable.
ADR-032 — CYCLE_SIZE associated const on ConstrainedTypeShape: compile-time domain-cardinality introspection for first_admit
Status: Accepted.
Context: ADR-026 G16 specifies
first_admit(<domain_type>, |idx| <predicate_body>) as a prism-layer
operator that performs first-admission search over a parametric finite
ring. At ADR-032’s drafting the macro lowered first_admit to a
structural declaration:
Term::Recurse { measure_index, base_index, step_index } where the
measure is a Term::Literal carrying the domain’s cardinality (the
ring’s cycle size). (ADR-034 subsequently shifts the lowering target to
a dedicated Term::FirstAdmit variant with structural short-circuit on
first admission; the cardinality-introspection mechanism this ADR
introduces remains the source of the literal that ADR-034’s lowering
reads as domain_size_index.) For WittLevel::W8, the cardinality is
2^8 = 256; for WittLevel::W32, the cardinality is
2^32 = 4294967296; for product or coproduct domains, the cardinality
is derivable from the constituent shapes' cardinalities.
The SDK’s prism_model! and verb! proc-macros emit the lowered Term
arena at proc-macro expansion time. To emit the correct measure literal
for any declared domain, the proc-macro must determine the domain’s
cardinality at expansion time — but ConstrainedTypeShape (per
ADR-017 + ADR-022 D4) currently exposes only IRI, SITE_COUNT, and
CONSTRAINTS as associated constants. Cardinality is implicitly defined
by the shape’s (SITE_COUNT, CONSTRAINTS) pair (a Witt-level shape with
SITE_COUNT = N and empty CONSTRAINTS has cardinality 2^N; a product
shape’s cardinality is the product of factors' cardinalities), but the
implicit derivation isn’t compile-time-introspectable from a generic
Rust trait method without a stored associated const.
Without a compile-time-introspectable cardinality surface, the SDK
proc-macro must either hardcode a placeholder (the current SDK 0.3.6
emits Literal(256) — the W8 ceiling — regardless of declared domain)
or defer cardinality resolution to runtime (which conflicts with the
framework’s "compile-time everything" commitment per Section 4 + ADR-022
D2 + ADR-024). The placeholder shape is acknowledged in the SDK source
(codegen/src/sdk_macros.rs:2301-2307): "the macro doesn’t introspect
<DomainTy as ConstrainedTypeShape> at proc-macro time, so we encode
256 as the ceiling and let implementations override per ADR-024." The
implementation-runtime override is sanctioned by ADR-026 G16’s three-way
responsibility split, but the architectural shape — the structural
declaration’s measure literal IS the domain’s cardinality — is
undermined when the macro can’t emit the correct value.
Decision: ConstrainedTypeShape extends with an associated const
CYCLE_SIZE: u64 that every conforming impl declares. The associated
const’s value is the cardinality of the shape’s value-set: the number of
distinct byte-sequences the shape admits per its
(SITE_COUNT, CONSTRAINTS) declaration.
pub trait ConstrainedTypeShape: __sdk_seal::Sealed {
const IRI: &'static str;
const SITE_COUNT: usize;
const CONSTRAINTS: &'static [ConstraintRef];
const CYCLE_SIZE: u64;
}Cardinality derivation per shape kind:
-
Witt-level shape (e.g.,
W8,W16,W32):CYCLE_SIZE = 2^WITT_LEVEL_BITS. ForW8,CYCLE_SIZE = 256; forW16,CYCLE_SIZE = 65536; forW32,CYCLE_SIZE = 4294967296. Foundation primitive declarations (andprism::std_types's primitive types per AGENTS.md §11) emit the correct const directly. -
Product shape (declared via
partition_product!per ADR-026 G17):CYCLE_SIZE = product of factors' CYCLE_SIZEs, saturating atu64::MAXif the product overflows. The macro emits the multiplication at expansion time using a foundation-provided const-fn helper that performs the saturating-multiply. -
Coproduct shape (declared via
partition_coproduct!per ADR-026 G18):CYCLE_SIZE = sum of variants' CYCLE_SIZEs + 1for the discriminator, saturating atu64::MAX. The macro emits the saturating-sum at expansion time. -
Custom output shape (declared via
output_shape!per ADR-027): the application declaresCYCLE_SIZEexplicitly as part of the macro invocation, with foundation validating that the declared value is consistent with the shape’s(SITE_COUNT, CONSTRAINTS)declaration. For shapes whose CONSTRAINTS strictly reduce the value-set (e.g., comparison-bounded ranges), the application’s declaredCYCLE_SIZEis the post-constraint cardinality. -
Foundation-sanctioned identity shape (
ConstrainedTypeInput):CYCLE_SIZE = 1(the empty shape admits exactly one byte-sequence — the empty one).
Type bound for the u64 width. The CYCLE_SIZE const is
u64-typed (saturating semantics for shapes whose true cardinality
exceeds 2^64). For the universal-model-compiler scope, u64 is
sufficient: cardinalities exceeding 2^64 require
structurally-different evaluation strategies (the catamorphism’s
Term::Recurse evaluator iterates CYCLE_SIZE times, which is
impractical above ~2^32 for any wall-clock-bounded execution, and the
implementation-runtime override per ADR-026 G16 carries non-exhaustive
search strategies for large domains). The architectural commitment is to
the introspectable surface; specific u64 interpretation is a
foundation-parameter decision.
SDK proc-macro consumption. The prism_model! and verb! macros'
first_admit lowering reads <DomainTy as
ConstrainedTypeShape>::CYCLE_SIZE at proc-macro expansion time and
emits it as the Term::Literal measure value. The SDK 0.3.6 placeholder
(Literal(256) regardless of domain) is replaced with the introspected
value. The proc-macro emits
Term::Literal { value: CYCLE_SIZE, level: <smallest WittLevel that fits> }
— for CYCLE_SIZE values in [0, 2^8) at W8, in [2^8, 2^16) at W16,
in [2^16, 2^32) at W32, and otherwise at W64. ADR-022 D3 G1 already
commits Term::Literal to admit any integer literal parseable as u64,
so CYCLE_SIZE: u64 values flow through Term::Literal without
saturation; foundation’s Term::Literal value-field width follows G1’s
existing commitment.
Consequences: The SDK proc-macro emits the correct
domain-cardinality literal for first_admit against any declared
domain. ADR-026 G16’s structural-declaration commitment is realized at
proc-macro time without the implementation-runtime override carrying the
cardinality. A model that declares
first_admit(WittLevel::W32, |idx| …) over a 32-bit search domain
causes SDK to read WittLevel::W32::CYCLE_SIZE = 4294967296 and emit a
Term arena whose domain_size_index (per ADR-034’s
Term::FirstAdmit { domain_size_index, predicate_index } lowering)
references a
Term::Literal { value: 4294967296, level: WittLevel::W64 }.
Foundation’s catamorphism evaluate_term_tree iterates idx ascending
across [0, CYCLE_SIZE) per ADR-029’s Term::FirstAdmit fold-rule with
structural short-circuit on first admission (per ADR-034); the
implementation-runtime override per ADR-026 G16’s three-way split
becomes optional for strategy (sequential, parallel coset traversal,
etc.) rather than load-bearing for structural correctness.
ADR-013’s substrate-amendment-via-foundation rule (TR-08) covers the
trait extension. Foundation extends ConstrainedTypeShape with the new
associated const; existing impls extend (the foundation primitives,
prism::std_types's primitive types, the SDK shape macros' emissions);
applications consuming foundation update transparently because the const
is foundation-emitted via the macros that already produce their
ConstrainedTypeShape impls.
Rejected alternative 1: Have the proc-macro derive CYCLE_SIZE from
(SITE_COUNT, CONSTRAINTS) at expansion time without a stored
associated const. Rejected — CONSTRAINTS can include arbitrary
ConstraintRef variants whose cardinality impact is non-trivial to
evaluate at proc-macro time; the cleanest derivation is the
shape-declaration site (where the shape’s structure is known) emitting
CYCLE_SIZE directly. The stored-const form keeps proc-macro-time logic
minimal.
Rejected alternative 2: Keep the placeholder Literal(256) and rely
on the implementation-runtime override per ADR-026 G16 indefinitely.
Rejected — the architectural shape (the structural declaration’s measure
IS the cardinality) is undermined when the macro emits a placeholder.
ADR-026 G16’s three-way split sanctions implementation overrides for
runtime strategy (sequential vs parallel, cancellation policy,
cost-budget enforcement), not for structural-correctness gaps in the
macro’s emission. Closing the introspection gap is a separate concern
from the runtime override.
Rejected alternative 3: Introduce a parallel DomainShape trait
with CYCLE_SIZE as the only member, leaving ConstrainedTypeShape
unchanged. Rejected — bifurcates the trait family (every conforming type
would need to impl both); duplicates the sealed-trait mechanism; the
architectural concern is "what’s the shape’s cardinality" which is
structurally part of the shape’s content, not a separate contract.
Rejected alternative 4: Use a runtime-introspectable mechanism (a
foundation-provided fn taking &dyn ConstrainedTypeShape and returning
cardinality). Rejected — runtime introspection conflicts with the
"compile-time everything" commitment; the SDK proc-macro can’t consume
runtime-only surfaces; the Term arena emission must be const-evaluable
per ADR-024’s verb-inlining commitment.
ADR-033 — Field-access projection (G20) for product-of-shapes inputs: Term::ProjectField and the closure-body destructor surface
Status: Accepted.
Context: ADR-022 D3’s closure-body grammar (G1-G11) specifies the
substrate-level forms for route bodies. ADR-026 extends with G12-G19
covering prism operators including partition_product! (G17) and
partition_coproduct! (G18) for type-level shape composition.
The grammar admits structured types at the route boundary — an
Input shape can be partition_product!(A, B) or
partition_coproduct!(A, B) per ADR-022 D4 — but doesn’t admit
structured access in the route body. A model declaring
Input = partition_product!(Prefix, Nonce) can reference input as a
whole (G2 lowers to Term::Variable { name_index: 0 }) but has no
syntactic form for "the prefix component of the input" or "the nonce
component of the input."
The closure-body grammar’s existing forms cover scalar inputs (a single Witt-level value flowing through the route) and tuple-literal construction (G11, building a tuple from existing terms). Neither covers product-shape destruction (extracting components of a structured input). For application authors writing routes whose Input has multiple semantically-distinct components, the route body has no way to access the components separately through the typed-iso surface; the implementation runtime extracts components per the application’s wire-format knowledge, with the typed-iso surface treating the input as an opaque byte sequence.
A representative example is a verb that performs bounded first-admission search over a 32-bit candidate domain whose predicate combines a content-addressing axis with a product-shaped input. The verb body wants to express:
first_admit(WittLevel::W32, |candidate| {
hash(concat(input.prefix, candidate)) <= input.threshold
})with input being a product shape
partition_product!(PrefixShape, ThresholdShape). Without G20’s
field-access projection, the closure-body grammar has no recognition for
input.prefix or input.threshold syntax; the verb’s body would have
to use input as an opaque byte-shape token in two
semantically-distinct positions:
first_admit(uor_foundation::WittLevel::W32, |candidate| {
hash(concat(input, candidate)) <= input
})and the runtime layout (the Layer-3 crate’s Input shape carrying both
prefix and threshold in its IntoBindingValue byte serialization) would
carry the destructuring semantics outside the typed-iso surface.
Decision: ADR-022 D3’s closure-body grammar extends with G20:
field-access projection on product-of-shapes inputs. The grammar form
recognizes <expr>.<name> and <expr>.<index> in closure bodies when
<expr> has a statically-inferable shape that is a partition_product
(or a chain of such projections — input.outer.inner). The macro lowers
the form to a new Term variant
Term::ProjectField { source_index, byte_offset, byte_length } whose
fold-rule slices the field’s bytes from the source’s evaluation result.
The proc-macro computes byte_offset and byte_length at expansion
time from the receiver shape’s structural metadata; the catamorphism’s
runtime fold-rule is pure byte-slicing with no shape-metadata lookup.
The Term enum extends from ten variants to eleven per ADR-013’s
substrate-amendment-via-foundation rule.
Grammar form G20. The closure-body grammar admits:
// Numeric field access (positional, parallel to Rust tuple destructuring):
input.0 // first component of input's product shape
input.1 // second component
// ... up to (factor_count - 1)
// Named field access (when the product shape is declared with named fields):
input.prefix // named field "prefix"
input.target // named field "target"
// Chained field access (for nested products):
input.outer.innerThe macro’s recognition rule: when the closure-body parser encounters a
.field access expression, it infers the receiver expression’s shape
(via the binding scope, the route’s declared Input shape, or the
inferred shape of an enclosing expression), verifies the shape is a
partition_product, looks up the field by name or index in the shape’s
structural metadata, computes the field’s byte offset and byte length,
and emits Term::ProjectField with source_index set to the receiver’s
Term arena index and byte_offset / byte_length set to the computed
values.
Named-field resolution requires the product shape to declare field
names. The partition_product! macro extends to admit a named-tuple
form:
partition_product!(MyInputShape, prefix: PrefixShape, threshold: ThresholdShape);emitting a ConstrainedTypeShape whose structural metadata includes the
field names. Positional-form
partition_product!(MyInputShape, PrefixShape, ThresholdShape) emits
anonymous fields accessible only by index (input.0, input.1).
Named-field metadata mechanism. The named-tuple partition_product!
macro emits, in addition to the standard ConstrainedTypeShape impl, a
pub const FIELDS of type &'static [(&'static str, u32, u32)] where
each tuple is (field_name, byte_offset, byte_length). The proc-macro
reads this const at expansion time when resolving named-field access
(input.<name>) — looking up the name in the const and emitting the
corresponding byte_offset and byte_length in the
Term::ProjectField variant. Positional-field access (input.<index>)
uses byte-offset and byte-length values derivable from the shape’s
factor sequence: byte_offset for index i is the sum of <FactorTy_j as
IntoBindingValue>::MAX_BYTES for j ∈ [0, i); byte_length is
<FactorTy_i as IntoBindingValue>::MAX_BYTES. Both forms produce
identical Term::ProjectField emissions when applied to the same field;
the surface form is the application author’s choice.
Chained access lowering. input.outer.inner lowers to a chain of
Term::ProjectField invocations: input.outer emits a ProjectField
whose source_index references the Term::Variable { name_index: 0 }
for the route input and whose byte_offset / byte_length are computed
from input's shape; the second .inner emits another ProjectField
whose source_index references the prior ProjectField's arena
position and whose byte_offset / byte_length are computed from the
receiver’s (Outer’s) shape per the same FIELDS-or-positional rules. Each
.field access in the chain emits exactly one Term::ProjectField; the
catamorphism evaluates them sequentially, with each fold-rule slicing
from the prior result.
Term variant Term::ProjectField. The eleventh Term variant:
pub enum Term {
// ... existing 10 variants per ADR-029
ProjectField {
source_index: u32, // Term arena index of the source expression (Variable, Application, or another ProjectField)
byte_offset: u32, // proc-macro-computed byte offset within the source value's evaluation result
byte_length: u32, // proc-macro-computed byte length of the projected field
},
}Per-variant fold-rule (extending ADR-029):
Term::ProjectField { source_index, byte_offset, byte_length } —
evaluate the source term identified by `source_index` (recursive
fold) producing a TermValue; emit the byte slice
[byte_offset .. byte_offset + byte_length] from the source's
evaluation result as the variant's carrier value. byte_offset +
byte_length must be ≤ the source's byte length; this is verified
at proc-macro expansion time from the receiver shape's structural
metadata, so well-formed Term trees never exhibit out-of-bounds
slicing at evaluation time.
Catamorphism’s TermValue capacity for projections. The carrier
value’s byte length is the projected field’s byte count, which is
bounded by the source value’s byte length (a Term arena value, not
necessarily a binding — could be a route input via Term::Variable, a
let-binding’s RHS evaluation, or another Term::ProjectField). The
source value’s byte length is bounded by the TermValue capacity
foundation 0.3.4 raised to 4096 bytes (per ADR-028’s reconciliation);
the projected field’s bytes are necessarily ≤ the source’s byte length.
No new TermValue ceiling is required.
Closure check at prism_model! / verb! invocation. Field-access
projections are validated at proc-macro expansion time:
-
The receiver expression’s shape must be statically inferable at proc-macro expansion time (via the binding scope, the route’s declared Input shape, or the inferred shape of an enclosing expression for chained access).
-
The receiver’s inferred shape must be a
partition_product(or a chain of products for nested access via a chained.fieldexpression). -
The field name (for named access) must exist in the shape’s
FIELDSconst; the field index (for positional access) must be in[0, factor_count)wherefactor_countis the product shape’s factor count. -
Field-access on coproduct shapes is NOT admitted (coproduct destructuring goes through
Term::Matchper G6 — pattern matching on the discriminator); projection on a coproduct emits a closure-violation error.
Consequences: The closure-body grammar admits structured-input
destructuring without leaving the typed-iso surface. Routes whose Input
has multiple semantically-distinct components express the components'
use directly in prism vocabulary. The implementation runtime no longer
needs to carry wire-format knowledge for product-shape inputs — the
foundation catamorphism evaluates the field-access projections through
Term::ProjectField's fold-rule.
Combined with ADR-032’s CYCLE_SIZE introspection (so the SDK emits the
appropriate domain-cardinality measure literal) and foundation 0.3.5+'s
recursive Term::Recurse evaluator (per ADR-029), the entire
bounded-search inference flows through pipeline::run_route's
catamorphism. Layer-3 implementations that previously carried
out-of-band traversal helpers (e.g., a sequential or parallel
candidate-iteration runtime) can retire those helpers — the typed-iso
surface carries the inference end-to-end.
The eleven-variant Term enum (the original ten plus ProjectField;
ADR-034 subsequently adds FirstAdmit as the twelfth; ADR-035 adds the
nine ψ-chain variants as the thirteenth through twenty-first) keeps the
per-variant fold-rule pattern intact; ADR-029’s catamorphism uniqueness
property (per ADR-019) is preserved for all twenty-one variants. The
grammar’s identifier-resolution order extends with field-access
expressions: the receiver expression’s shape-inference check (per the
closure check above) happens before the existing G3-vs-G12
disambiguation per ADR-026.
ADR-013’s substrate-amendment-via-foundation rule (TR-08) covers the Term enum’s eleven-variant extension. Foundation extends the enum, the wire format (per the trace replay format) bumps the format-version constant. Existing models declaring scalar inputs (no product shapes, no field-access in route bodies) are unaffected — the new variant is reachable only through the new grammar form.
Rejected alternative 1: Generalize Term::Project (currently for
Witt-level projection) to also handle byte-slice projection from product
shapes. Rejected — overloads two semantically-distinct projection
operations into one Term variant. The fold-rule would branch on the
operand’s shape kind (Witt-level scalar vs product), which conflates two
architectural concerns and complicates per-variant reasoning.
Rejected alternative 2: Express field-access projection through
Term::Match patterns with destructuring. Rejected — Term::Match (per
ADR-022 D3 G6) is for coproduct destructuring (matching on a
discriminator); product destructuring is structurally a different
operation (always-emits one component, vs match-emits one of N
variants). Conflating them complicates G6’s semantic shape and breaks
the existing match-arm exhaustiveness check.
Rejected alternative 3: Carry field-access through
Term::Application with a PrimitiveOp::ProjectField discriminant.
Rejected — projection isn’t a binary arithmetic operation; the args
slice convention for Term::Application doesn’t fit the
(source_index, byte_offset, byte_length) operand structure naturally
(Term::Application’s args are themselves Term arena indices to other
terms, whereas byte_offset and byte_length are scalar bytespans, not
term references); the fold-rule for primitives is shape-uniform whereas
projection’s fold-rule is byte-slicing on a dynamically-sized source
value.
Rejected alternative 4: Keep field-access outside the closure-body grammar; require applications to declare each component as a separate route input. Rejected — breaks the typed-iso surface’s input-as-single-shape commitment per ADR-022 D4; structured types (products and coproducts) lose their architectural role; cross-component composition becomes externally-managed.
ADR-034 — Term::FirstAdmit variant and iteration-counter binding for Term::Recurse: structural search with early termination, bounded fold with iteration-counter access
Status: Accepted.
Context: Two operators in ADR-026’s prism operator set — fold_n
(G14) and first_admit (G16) — admit closure parameters that the
structural declaration must bind in the step/predicate body’s scope.
fold_n(n, init, |state, idx| step) binds state (the running
accumulator) and idx (the iteration counter, ranging 0..n).
first_admit(<domain>, |idx| <predicate>) binds idx (the candidate
value, ranging 0..<domain>::CYCLE_SIZE).
ADR-022 D3 G7’s Term::Recurse grammar form binds only <self_ident>
(the recursive-call placeholder) in the step body’s scope. ADR-029’s
per-variant fold-rule for Term::Recurse extends scope only with the
recursive-call placeholder via a foundation-fixed
RECURSE_PLACEHOLDER_NAME_INDEX. The iteration counter — the descending
measure value at each recursive call — has no Variable name in the
step body’s scope. Models compiled through ADR-026 G14’s fold_n
lowering for counts above <B as HostBounds>::FOLD_UNROLL_THRESHOLD per
ADR-037 (the unrolled-chain case has idx substituted at expansion time
per unroll position; the Term::Recurse case does not) emit Term arenas
where the step body’s idx reference resolves to nothing.
ADR-026 G16’s first_admit lowering compounds the gap: first_admit
lowers to Term::Recurse, but Term::Recurse's fold-rule is
unconditional bounded recursion — iterate measure times regardless
of step-body results. first_admit's semantics are bounded search
with early termination on admission — return the first idx for which
the predicate evaluates true; return a not-found sentinel if no idx
admits. These are structurally distinct: bounded recursion is a fold,
search is a partial function. Conflating them at the Term variant level
forces foundation’s evaluator into iterating the entire domain even when
the predicate has admitted, which makes first_admit infeasible
end-to-end at any nontrivial cardinality (e.g., a WittLevel::W32
search domain at 2^32 = 4294967296 candidates would require iterating
the full domain regardless of when the predicate first admits, taking
many hours of wall-clock time per call under unconditional iteration).
ADR-026 G16’s three-way responsibility split sanctions
implementation-runtime overrides for strategy (sequential vs parallel,
cancellation policy), but the search-vs-fold distinction is structural
correctness, not strategy.
Without architectural commitments closing both gaps, foundation’s
catamorphism cannot evaluate fold_n (large counts) or first_admit
end-to-end. The implementation runtime is required to thread the
iteration counter and to short-circuit on admission. ADR-026 G16’s
three-way responsibility split currently absorbs both as
implementation-runtime work; for Layer-3 implementations' bounded-search
runtime helpers to retire (so the typed-iso surface carries the
inference end-to-end), the architecture must commit to the missing
semantics structurally.
Decision: The architecture commits to two complementary mechanisms.
Name-index reservation. ADR-034 reserves two foundation-fixed u32
name-index values via the same pattern ADR-022 D3 commits to for the
existing name_index = 0 (G2 input parameter), name_index = u32::MAX
(G6 wildcard / G9 propagation handler), and foundation 0.3.5+'s
RECURSE_PLACEHOLDER_NAME_INDEX = u32::MAX - 1 and
UNFOLD_PLACEHOLDER_NAME_INDEX = u32::MAX - 2. The new reservations are
RECURSE_IDX_NAME_INDEX = u32::MAX - 3 (Mechanism 1) and
FIRST_ADMIT_IDX_NAME_INDEX = u32::MAX - 4 (Mechanism 2). These are
foundation-only — applications cannot emit
Term::Variable { name_index: … } with these values through the
closure-body grammar (the macro assigns fresh indices in declaration
order starting from 1 per ADR-022 D3 G10, never approaching the
foundation-reserved high range). The reservation pattern preserves
wire-format compatibility with existing Term arenas: pre-ADR-034 arenas
never emit Variables with these name-indices because foundation never
assigned them, so the new bindings are reachable only through new
emissions of Term::Recurse's extended scope-rule (Mechanism 1) or
Term::FirstAdmit's scope-rule (Mechanism 2).
Mechanism 1: Iteration-counter binding for Term::Recurse.
Foundation defines a second foundation-fixed RECURSE_IDX_NAME_INDEX
(e.g., u32::MAX - 3, paralleling the existing
RECURSE_PLACEHOLDER_NAME_INDEX = u32::MAX - 1 and
UNFOLD_PLACEHOLDER_NAME_INDEX = u32::MAX - 2). The Term::Recurse
data structure does not change; only the fold-rule’s scope-extension
extends. ADR-029’s per-variant fold-rule for Term::Recurse is updated
to: evaluate measure (recursive fold); if the measure equals zero,
evaluate base (recursive fold) and emit; otherwise, evaluate step
(recursive fold) in extended scope where (a)
RECURSE_PLACEHOLDER_NAME_INDEX binds to the result of evaluating the
same Term::Recurse with measure decremented by 1, AND (b)
RECURSE_IDX_NAME_INDEX binds to a TermValue carrying the current
measure value (the iteration counter at this descent). The fold
terminates when the measure reaches zero; well-foundedness is
structurally guaranteed by the descent measure’s monotonic decrease.
ADR-022 D3 G7’s grammar form extends to admit a two-parameter closure
shape:
recurse(<measure_expr>, <base_expr>, |<self_ident>, <idx_ident>| <step_expr>).
The single-parameter form (existing) remains valid — <idx_ident> is
optional. The SDK proc-macro lowers <idx_ident> references inside the
step body directly to
Term::Variable { name_index: RECURSE_IDX_NAME_INDEX } — the
foundation-fixed name index is the canonical lowering target. The
closure parameter <idx_ident> is a Rust source-level identifier the
application author chooses (paralleling <self_ident> for the
recursive-call placeholder); the macro treats it as an alias for the
foundation-fixed name during the step body’s lowering. Foundation’s
catamorphism resolves
Term::Variable { name_index: RECURSE_IDX_NAME_INDEX } references
within the enclosing Term::Recurse's step subtree to the current
iteration counter per the variant’s fold-rule.
Mechanism 2: Term::FirstAdmit variant. The Term enum extends
from eleven variants (after ADR-033’s ProjectField) to twelve with
Term::FirstAdmit:
pub enum Term {
// ... existing 11 variants per ADR-029 + ADR-030 + ADR-033
FirstAdmit {
domain_size_index: u32, // Term arena index of the domain cardinality (typically Term::Literal { value: <Domain>::CYCLE_SIZE })
predicate_index: u32, // Term arena index of the predicate body (closure body whose result indicates admission)
},
}Result-value convention. Term::FirstAdmit's evaluation result is a
foundation-defined coproduct value at TermValue level: a single
discriminator byte (0x00 for "not found", 0x01 for "found") followed by
the candidate idx packed at <Domain>'s WittLevel byte width. The
discriminator encodes the architectural answer to "did any idx admit?"
without conflating with any in-range idx value (the discriminator-byte
sentinel is structurally distinct from the idx payload). Models that
consume the result destructure through the existing Term::Match per
ADR-022 D3 G6 (the typed-iso surface admits coproduct destructuring
through G6’s pattern-match form). The architectural commitment is that
Term::FirstAdmit's output shape is the coproduct shape
partition_coproduct!(NotFound, Found(<Domain>)) per ADR-026 G18 —
foundation emits the coproduct-shape declaration alongside the variant’s
fold-rule.
Per-variant fold-rule (extending ADR-029):
Term::FirstAdmit { domain_size_index, predicate_index } —
evaluate domain_size_index (recursive fold) producing a TermValue
carrying a non-negative integer N at WittLevel sufficient to
represent N (per ADR-022 D3 G1's u64-width commitment: the smallest
WittLevel that fits N). For idx in 0..N (ascending from 0,
sequentially): evaluate predicate_index (recursive fold) in extended
scope where FIRST_ADMIT_IDX_NAME_INDEX (a foundation-fixed name
index per ADR-034) binds to a TermValue carrying idx at the same
WittLevel as N's; if the result is non-zero (interpreted via
foundation's zero/non-zero convention per ADR-029's existing
primitive-comparison fold-rule for Le/Lt/Ge/Gt: any TermValue
whose byte sequence is not all-zero is "true"), emit a TermValue
carrying the coproduct value `(0x01, idx_bytes)` (the "found"
discriminator followed by idx packed at the domain's WittLevel
byte width) and terminate the iteration. If no idx admits across
the full range [0, N), emit a TermValue carrying the coproduct
value `(0x00, padding)` (the "not-found" discriminator followed
by idx-width zero bytes; the padding bytes have no semantic
meaning, structural padding only).
The fold-rule is structurally short-circuiting: the catamorphism stops
iterating at the first idx for which the predicate admits.
Well-foundedness is structurally guaranteed by the bounded domain (N
evaluations maximum).
ADR-026 G16’s grammar form admits a single-parameter closure:
first_admit(<domain_type>, |<idx_ident>| <predicate_body>). The SDK
proc-macro lowers <idx_ident> references inside <predicate_body>
directly to Term::Variable { name_index: FIRST_ADMIT_IDX_NAME_INDEX }
— the foundation-fixed name index is the SDK’s canonical lowering target
for this binding, not a fresh per-invocation index. The closure
parameter <idx_ident> is a Rust source-level identifier the
application author chooses (a name that reads naturally for the
search-domain semantic — candidate, key, index, etc.); the macro
treats it as an alias for the foundation-fixed name during the predicate
body’s lowering. Foundation’s catamorphism resolves
Term::Variable { name_index: FIRST_ADMIT_IDX_NAME_INDEX } references
within the enclosing Term::FirstAdmit's predicate subtree to the
candidate idx per the variant’s fold-rule. Per the Name-index
reservation paragraph above, applications cannot emit Variables with
FIRST_ADMIT_IDX_NAME_INDEX outside of macro-recognized first_admit
forms — the closure-body grammar’s fresh-index assignment per ADR-022 D3
G10 starts from 1 and never approaches the foundation-reserved high
range.
ADR-026 G16’s structural-declaration commitment changes: the lowering
target shifts from Term::Recurse to Term::FirstAdmit. The macro
emits
Term::FirstAdmit { domain_size_index: <Term::Literal carrying <Domain>::CYCLE_SIZE per ADR-032, at the smallest WittLevel that fits the cardinality per the wiki’s existing G1 commitment to literals parseable as u64>, predicate_index: <predicate body’s Term arena index> }.
The implementation-runtime override per the three-way responsibility
split remains available for strategy (sequential vs parallel coset
traversal, cancellation policy on first admission, cost-budget
enforcement); it is no longer load-bearing for structural correctness.
Cross-axis composition. Models that use first_admit over a domain
whose predicate_index body invokes axis-trait methods (e.g., a
content-addressing search predicate that calls HashAxis::sha256 per
ADR-031’s prism-crypto sub-crate) compose cleanly: the catamorphism’s
per-variant fold-rules cover Term::AxisInvocation per ADR-029 +
ADR-030, and Term::FirstAdmit's fold-rule evaluates predicate_index
recursively, so axis-trait calls inside the predicate body resolve
through the AxisTuple dispatch surface as they would in any other
predicate position. The domain_size_index is bounded by ADR-032’s
per-shape-kind CYCLE_SIZE derivation table (Witt-level / product /
coproduct / output_shape! / identity) — the existing derivation paths
cover every shape the typed-iso surface admits as a search domain.
TermValue capacity for FirstAdmit. The carrier value’s byte length
is one byte (the discriminator) plus <Domain>'s WittLevel byte width
(the idx payload, packed at the domain’s level). For a
WittLevel::W32 search domain, the result is 5 bytes: 1 discriminator
byte + 4 idx bytes. The value is bounded by the substrate’s existing
TermValue ceiling (4096 bytes per ADR-028’s reconciliation); no new
ceiling required.
Closure check at prism_model! / verb! invocation.
Term::FirstAdmit is emitted only by the macro’s recognition of ADR-026
G16’s first_admit(<domain>, |<idx>| <pred>) form. The macro verifies:
(a) <domain> resolves to a ConstrainedTypeShape impl with
CYCLE_SIZE > 0 per ADR-032; (b) <idx> is a fresh identifier (not
shadowing an existing binding); (c) <pred> evaluates to a TermValue
whose byte sequence the catamorphism interprets via the standard
zero/non-zero convention (any all-zero byte sequence is "false"; any
other byte sequence is "true") — paralleling ADR-029’s existing
fold-rule for byte-level comparison primitives (Le/Lt/Ge/Gt) which emit
at the operand’s WittLevel and are interpreted by the same convention;
the predicate body composing comparison primitives, axis-trait method
calls, or other Term forms is admissible without WittLevel restriction.
Consequences: Foundation’s catamorphism evaluates first_admit
end-to-end with structural short-circuit; the implementation-runtime
override per ADR-026 G16’s three-way split becomes optional for strategy
rather than load-bearing for structural correctness. Layer-3
implementations whose previous bounded-search runtime helpers
(sequential or parallel candidate-iteration loops outside the typed-iso
surface) carried the search semantics can retire those helpers — a verb
body of the shape
first_admit(WittLevel::W32, |candidate| { hash(concat(input.left, candidate)) ⇐ input.threshold })
over
Input = partition_product!(MyInputShape, left: LeftShape, threshold: ThresholdShape)
flows through pipeline::run_route's catamorphism, with foundation
iterating candidate ascending across the half-open range [0, 2^32)
and short-circuiting at the first admitting candidate. ADR-026 G16’s
three-way responsibility split’s implementation-runtime override remains
available for strategy (parallel coset traversal, cancellation policy,
cost-budget enforcement) but the typed-iso surface carries the
structural commitment.
Foundation’s catamorphism evaluates fold_n end-to-end for both
unrolled and Term::Recurse-lowered cases: the iteration-counter
binding extension to Term::Recurse lets the step body reference idx
for counts above <B as HostBounds>::FOLD_UNROLL_THRESHOLD per ADR-037.
Models declaring fold_n with parametric counts
(substitution-axis-derived associated constants) flow through the
catamorphism without unroll-vs-Recurse semantic divergence.
The Term enum extends from eleven variants to twelve. ADR-013’s substrate-amendment-via-foundation rule (TR-08) covers the variant addition. Foundation extends the enum, the wire format (per the trace replay format) bumps the format-version constant, the catamorphism’s per-variant fold-rules extend with the new variant.
Rejected alternative 1: Extend Term::Recurse to admit a
short-circuit predicate, generalizing it to "primitive recursion with
optional early termination" (one variant covering both fold_n and
first_admit). Rejected — conflates two semantically-distinct
operations into one Term variant. The fold-rule branches on whether the
short-circuit predicate is present, complicating per-variant reasoning.
Each Term variant should have one clear semantic; primitive recursion
(fold) and bounded search (find) are categorically distinct
(catamorphism vs partial function).
Rejected alternative 2: Keep first_admit's lowering as
Term::Recurse and rely on the implementation-runtime override per
ADR-026 G16 indefinitely. Rejected — the typed-iso surface cannot carry
the inference end-to-end; foundation’s catamorphism iterates 2^32 times
unconditionally for WittLevel::W32 (many hours of wall-clock per
call). The implementation-runtime override is sanctioned for strategy
selection, not for structural correctness gaps that make foundation’s
catamorphism infeasible. Layer-3 implementations' bounded-search runtime
helpers cannot retire under this alternative.
Rejected alternative 3: Add Term::FoldIter as a separate variant
for fold_n (with iteration-counter binding) AND Term::FirstAdmit for
search (with iteration-counter binding plus short-circuit), so
Term::Recurse stays single-purpose for raw primitive recursion.
Rejected — adds two variants to the Term enum where one variant addition
(FirstAdmit) plus a fold-rule extension (Term::Recurse's scope)
suffices. The iteration-counter binding is a small generalization of
Term::Recurse's existing scope-extension mechanism (the
dependent-types primitive-recursion eliminator binds both predecessor’s
result AND iteration counter — the canonical mathematical shape); making
it implicit via foundation-fixed name indices keeps Term::Recurse's
data structure stable.
Rejected alternative 4: Replace Term::Recurse entirely with
Term::FirstAdmit and have fold_n lower through Term::FirstAdmit
with a predicate that always returns false (so search iterates the full
domain) plus an accumulator threaded through the predicate’s scope.
Rejected — semantically incorrect: Term::FirstAdmit returns a
coproduct value (discriminator, idx) per ADR-034’s result-value
convention; fold_n returns the accumulator after n iterations at the
accumulator’s declared shape. The result shapes differ structurally;
conflating them via predicate-tricks breaks the catamorphism’s
uniqueness property and conflicts with ADR-019’s initial-algebra
commitment.
Rejected alternative 5: Carry the iteration counter through an
explicit Term::Application with a PrimitiveOp::IterIndex
discriminant that the catamorphism interprets as "current iteration
counter at the enclosing Recurse/FirstAdmit." Rejected — PrimitiveOp
is the substrate’s first-order operation vocabulary; IterIndex is a
binding-resolution mechanism, not a primitive operation. Smuggling a
binding through PrimitiveOp violates the architectural separation
between Term variants (which carry binding semantics) and PrimitiveOp
discriminants (which carry first-order operations).
ADR-035 — Canonical ψ-pipeline + ψ-chain Term variants + ψ-residuals discipline on verb body composition
Status: Accepted.
Context: The framework’s op:InferenceOperation is ι = P ∘ Π ∘ G
— the ψ-pipeline composed (per spec/src/namespaces/op.rs). The
ψ-pipeline (ψ_1..ψ_6) is the resolution arm: Ring → Constraints → Sites
→ Partition → Refinement, delivering a partition of the ring per
resolved type per the ontology’s op:Pipeline verification domain. The
ψ-chain (ψ_1..ψ_9, per spec/src/namespaces/op.rs and
spec/src/namespaces/homology.rs) is the structural-witness arm: nine
ontology-defined identity maps composing into a structural-correctness
pipeline that witnesses the partition’s homology-class identities. Both
arms compose op:InferenceOperation.
The closure-body grammar’s twelve combinatorial Term variants (Literal,
Variable, Application, Lift, Project, Match, Recurse, Unfold, Try,
AxisInvocation, ProjectField, FirstAdmit) admit the ψ-pipeline’s
resolution mechanics — combinatorial operations on byte-level operands
evaluate Term arenas to byte values. None of them is a ψ-map. The
closure-body grammar admits no syntactic form lowering to "construct the
constraint nerve," "perform Postnikov truncation," "extract homotopy
groups," "compute k-invariants," or any other ψ-pipeline operation. Verb
bodies cannot witness the structural-correctness arm of
op:InferenceOperation through prism vocabulary.
The framework’s verifiability commitment per ADR-001 + ADR-019 —
canonical computational equivalences as homology classes; uniqueness of
catamorphism evaluation; pipeline as a valuation map from Term arenas to
homology-class-witnessed values — requires the ψ-chain to be reachable
from verb bodies. Without ψ-Term variants, verb authors must encode
admission as a runtime predicate that Term::FirstAdmit enumerates over
a value domain, recovering the structural-witness relationship by
brute-force search rather than by structural witness. The closure-body
grammar’s structural-correctness shape (admission IS a property of the
value’s structural homology) is unstated in prism vocabulary.
Conceptual model. The compiled binary IS the canonical circuit. The
data representation is minimal — the substrate is coordinates (the ring
R_n per ADR-001; typed sites per op:ConstrainedType); the client
(the prism model) decomposes complexity through its hierarchical
modeling. The client is conceptually larger than the data representation
it operates on. A complete model fuses into a single reference: one
verb-body term-arena evaluation producing one label that classifies an
equivalence class of values sharing the same canonical structural
witness. That single operation manages infinite complexity — a
constant-width label naming an equivalence class whose cardinality is
bounded only by the value space the substrate admits.
Decision: The architecture commits three coupled amendments:
(1) Nine ψ-chain Term variants. The substrate’s Term enum extends
with nine new variants — one per ontology-defined ψ-map (ψ_1..ψ_9). The
Term enum extends from twelve variants (after ADR-034’s FirstAdmit) to
twenty-one. ψ-Term variants are uniform with combinatorial Term variants
— the catamorphism’s per-variant fold-rule pattern is the same; eight of
the nine consult the model declaration’s R: ResolverTuple per ADR-036
(Nerve, ChainComplex, HomologyGroups, CochainComplex, CohomologyGroups,
PostnikovTower, HomotopyGroups, KInvariants); one (Betti) is
resolver-free pure computation on already-resolved homology groups.
(2) Canonical ψ-pipeline composition: the k-invariants branch. The
architecture commits the k-invariants branch ψ_1 → ψ_7 → ψ_8 → ψ_9
as the canonical composition for the framework’s verifiability
commitment. The k-invariants κ_k are the universal classifying
invariants of the Postnikov tower per homology:KInvariant; they
classify Postnikov-tower extensions and thereby the homotopy type up to
weak equivalence — the maximum-discriminating structural invariant in
the ψ-chain. Two values are computationally equivalent per ADR-001 +
ADR-019 iff their k-invariants match.
Narrower invariants — ψ_4 BettiNumbers (rank only), ψ_3 HomologyGroups (abelian-group structure), ψ_6 CohomologyGroups (UCT-equivalent to homology), ψ_8 HomotopyGroups alone (non-abelian without classification of extensions) — are strictly weaker. The canonical compiled form produces the maximum-discriminating witness with the minimum number of resolver-bound stages (four: ψ_1, ψ_7, ψ_8, ψ_9). All nine ψ-Term variants remain in the substrate for narrower compositions; applications whose admission relations are naturally expressible at narrower invariants compose with the corresponding ψ-Term variants. Foundation’s catamorphism is optimized against the canonical composition; the wire format is calibrated against the κ-label width; the conformance corpus enumerates verb-body shapes whose canonical composition is the k-invariants branch.
Why the k-invariants branch is the optimal compiled form. The κ-invariants compress the full Postnikov-tower classification into a constant-width label — one operation managing the equivalence-class assignment of values sharing the same homotopy type. The compiled binary’s verifiability commitment is the strongest discriminating witness; producing a weaker invariant from the same verb body wastes the compilation budget on an extraction that does not carry the canonical equivalence information. The architectural separation is preserved by retaining all nine ψ-Term variants in the substrate (narrower applications compose with them); the architectural commitment is that the canonical composition — the one the verifiability commitment is calibrated against — is ψ_1 → ψ_7 → ψ_8 → ψ_9.
(3) ψ-residuals discipline on verb body composition. The verb body’s term composition is pure-prism — it composes ψ-Term variants and combinatorial Term variants over the input’s structural decomposition. The following Term forms are ψ-residuals — the vocabulary of ψ-enumeration where admission is decomposed into a runtime predicate over a value-bytes domain — and do not appear in verb-body term composition:
-
Term::FirstAdmitper ADR-034 — ψ-enumeration over a counter domain. -
Term::AxisInvocationper ADR-030 — axis-trait-method dispatch from verb-body terms (the canonical hash axis is consumed by resolvers, not by verb-body composition;Term::AxisInvocationbelongs in resolver bodies as part of their internal computation, not in the verb body’s structural composition). -
Term::Application { operator: PrimitiveOp::Le | PrimitiveOp::Lt | PrimitiveOp::Ge | PrimitiveOp::Gt, .. }— byte-comparison residuals of search-based admission predicates. -
Term::Application { operator: PrimitiveOp::Concat, .. }— byte-concatenation residuals of byte-shape-aware admission.
The canonical compiled form is structural: admission is a property of
the value’s k-invariant signature, not a search predicate over byte
values. The verb body composes ψ-Term variants and the ψ-residual-free
combinatorial Term variants: Term::Literal, Term::Variable,
Term::Application with arithmetic-and-bitwise PrimitiveOps from the
wiki’s canonical catalog excluding the ψ-residual ops — i.e.,
Add/Sub/Mul/Xor/And/Or/Neg/Bnot/Succ/Pred per
ADR-029 + ADR-022 D3 G3a (the ψ-residual ops
Le/Lt/Ge/Gt/Concat are excluded), Term::Match,
Term::Recurse, Term::Unfold, Term::Try, Term::Lift,
Term::Project, Term::ProjectField. The ψ-residuals discipline is
enforced at proc-macro expansion: the SDK’s verb! and prism_model!
macros walk the closure body’s term arena and reject ψ-residual
emissions with a closure-violation error citing the ψ-residual category
and the verb’s name.
The nine ψ-chain Term variants (paralleling ψ_1..ψ_9 per
spec/src/namespaces/op.rs and spec/src/namespaces/homology.rs):
pub enum Term {
// ... existing 12 variants per ADR-029 + ADR-030 + ADR-033 + ADR-034
/// ψ_1: Constraints → SimplicialComplex (nerve construction).
/// Maps the per-value byte sequence to its nerve simplicial complex
/// per ψ_1's identity `N(constraints) → SimplicialComplex`. The
/// NerveResolver receives the per-value bytes and constructs the
/// per-value constraint nerve; the resolver's resolve method encodes
/// the application's "what constraints does this value induce?"
/// semantics — for example, an admission-by-homology application's
/// NerveResolver receives the value bytes and produces a constraint
/// nerve whose β-structure encodes the application's admission
/// criterion (e.g., a relational predicate over the bytes) as
/// constraint-nerve topology.
/// Lowers from `nerve(<value_expr>)` closure-body form (G21).
/// Resolver-bound: consults the ResolverTuple's NerveResolver per ADR-036.
Nerve {
value_index: u32,
},
/// ψ_2: SimplicialComplex → ChainComplex (chain functor).
/// Lowers from `chain_complex(<simplicial_expr>)` (G22).
/// Resolver-bound: ChainComplexResolver per ADR-036.
ChainComplex {
simplicial_index: u32,
},
/// ψ_3: ChainComplex → HomologyGroups (homology functor): H_k(C) = ker(∂_k) / im(∂_{k+1}).
/// Lowers from `homology_groups(<chain_expr>)` (G23).
/// Resolver-bound: HomologyGroupResolver per ADR-036.
HomologyGroups {
chain_index: u32,
},
/// ψ_4: HomologyGroups → BettiNumbers (extraction functor): β_k(K).
/// Pure computation on resolved homology groups; no resolver consultation.
/// Lowers from `betti(<homology_expr>)` (G24).
Betti {
homology_index: u32,
},
/// ψ_5: ChainComplex → CochainComplex (dualization functor): C^k = Hom(C_k, R).
/// Lowers from `cochain_complex(<chain_expr>)` (G25).
/// Resolver-bound: CochainComplexResolver per ADR-036.
CochainComplex {
chain_index: u32,
},
/// ψ_6: CochainComplex → CohomologyGroups (cohomology functor): H^k(C) = ker(δ^k) / im(δ^{k-1}).
/// Lowers from `cohomology_groups(<cochain_expr>)` (G26).
/// Resolver-bound: CohomologyGroupResolver per ADR-036.
CohomologyGroups {
cochain_index: u32,
},
/// ψ_7: SimplicialComplex → PostnikovTower (Kan-completion + Postnikov truncation):
/// π_{≤k} for k = 0..dim(N(C)). The PostnikovResolver performs the Kan-completion
/// (per the homology namespace's KanComplex / HornFiller surface) as part of its
/// resolve semantics; the application provides a SimplicialComplex receiver
/// (typically a `Term::Nerve` emission), not a KanComplex. The ontology's ψ_7
/// identity (KanComplex → PostnikovTower) is preserved at the resolver-internal
/// level; the closure-body grammar surfaces the input/output of the composition
/// (SimplicialComplex → PostnikovTower) so verb authors do not need to construct
/// KanComplex values explicitly.
/// Lowers from `postnikov_tower(<simplicial_expr>)` (G27).
/// Resolver-bound: PostnikovResolver per ADR-036.
PostnikovTower {
simplicial_index: u32,
},
/// ψ_8: PostnikovTower → HomotopyGroups (homotopy extraction): π_k from each truncation stage.
/// Lowers from `homotopy_groups(<postnikov_expr>)` (G28).
/// Resolver-bound: HomotopyGroupResolver per ADR-036.
HomotopyGroups {
postnikov_index: u32,
},
/// ψ_9: HomotopyGroups → KInvariants (k-invariant computation): κ_k classifying the Postnikov tower.
/// Lowers from `k_invariants(<homotopy_expr>)` (G29).
/// Resolver-bound: KInvariantResolver per ADR-036.
KInvariants {
homotopy_index: u32,
},
}Per-variant fold-rules (extending ADR-029). Each ψ-Term variant’s
fold-rule follows the established per-variant pattern: evaluate operands
recursively, perform the variant’s content operation (foundation API
delegation, ResolverTuple consultation, or pure computation), emit a
TermValue carrying the result. The eight resolver-bound variants (Nerve,
ChainComplex, HomologyGroups, CochainComplex, CohomologyGroups,
PostnikovTower, HomotopyGroups, KInvariants) consult the model
declaration’s R: ResolverTuple per ADR-036 to retrieve the
application-provided resolver instance for the corresponding ontology
category; the catamorphism’s evaluation environment carries the
ResolverTuple alongside the AxisTuple. Resolver consultation is
parameterized by the model’s H-axis per ADR-022 D5: each resolver trait
is Resolver<H> (e.g., NerveResolver<H>, ChainComplexResolver<H>);
the catamorphism’s evaluation environment threads the H-axis alongside
the ResolverTuple, and the resolver-bound fold-rules invoke the
resolver’s resolve method on the ResolverTuple’s accessor for the
appropriate category. The one resolver-free variant (Betti) is pure
computation on already-resolved homology groups; no resolver
consultation, no H-axis threading needed for its fold-rule.
The fold-rule details for the nine variants are normatively specified in ADR-029’s per-variant fold-rule list (extended by Block B per this ADR).
Composition along the ψ-chain. The catamorphism evaluates ψ-Term
arenas through normal recursive fold; nested emissions compose along the
chain. The canonical k-invariants branch lowers from the closure-body
form k_invariants(homotopy_groups(postnikov_tower(nerve(input)))) to a
Term arena where Term::KInvariants references Term::HomotopyGroups
references Term::PostnikovTower references Term::Nerve references
the per-value input — the catamorphism evaluates inside-out per the
standard recursive fold pattern, with each ψ-Term variant’s fold-rule
consuming its inner emission’s byte serialization. The chain composes
uniformly with the ψ-residual-free combinatorial Term variants (ψ-Term
arenas can include Term::Match, Term::Application with
arithmetic-and-bitwise PrimitiveOps, Term::ProjectField over the byte
serializations as the application’s structural logic requires).
Closure-body grammar forms G21..G29. ADR-022 D3’s grammar extends from G1..G20 to G1..G29 with nine new forms recognizing the ψ-Term variants:
-
G21 —
nerve. Rust syntax:nerve(<value_expr>)where<value_expr>evaluates to a per-value byte sequence (typicallyinputfor a route input, or aTerm::ProjectFieldemission extracting a specific field, or any other byte-shaped expression). Emitted:Term::Nerve { value_index }. The macro verifies<value_expr>resolves to a byte-shaped receiver (resolution-time check; non-byte-shaped receivers fail with closure-violation error). The NerveResolver consumes the per-value bytes and produces a constraint nerve whose β-structure encodes the application’s "what constraints does this value induce?" semantics — the constraint nerve is per-value (varies with the value’s bytes through the resolver), not value-independent.nerveis a reserved macro-vocabulary identifier. -
G22 —
chain_complex. Rust syntax:chain_complex(<simplicial_expr>). Emitted:Term::ChainComplex. Receiver-shape check:<simplicial_expr>must resolve to a simplicial-complex-shaped expression (typically anerve(…)invocation).chain_complexis a reserved macro-vocabulary identifier. -
G23 —
homology_groups. Rust syntax:homology_groups(<chain_expr>). Emitted:Term::HomologyGroups. Receiver-shape check: chain-complex-shaped.homology_groupsis a reserved macro-vocabulary identifier. -
G24 —
betti. Rust syntax:betti(<homology_expr>). Emitted:Term::Betti. Receiver-shape check: homology-groups-shaped. The result is a[u32; <B as HostBounds>::BETTI_DIMENSION_MAX]byte sequence per ADR-037; subsequentTerm::ProjectFieldemissions extract individual β-numbers viabyte_offset = 4 * k,byte_length = 4forkin[0, <B as HostBounds>::BETTI_DIMENSION_MAX).bettiis a reserved macro-vocabulary identifier. -
G25 —
cochain_complex. Rust syntax:cochain_complex(<chain_expr>). Emitted:Term::CochainComplex. Receiver-shape check: chain-complex-shaped.cochain_complexis a reserved macro-vocabulary identifier. -
G26 —
cohomology_groups. Rust syntax:cohomology_groups(<cochain_expr>). Emitted:Term::CohomologyGroups. Receiver-shape check: cochain-complex-shaped.cohomology_groupsis a reserved macro-vocabulary identifier. -
G27 —
postnikov_tower. Rust syntax:postnikov_tower(<simplicial_expr>). Emitted:Term::PostnikovTower { simplicial_index }. Receiver-shape check: simplicial-complex-shaped (typically aTerm::Nerveemission). The PostnikovResolver performs Kan-completion (per the homology namespace’sKanComplex/HornFillersurface) as part of itsresolvesemantics, then computes the truncation tower per ψ_7’s identity; verb authors do not need to construct KanComplex values explicitly.postnikov_toweris a reserved macro-vocabulary identifier. -
G28 —
homotopy_groups. Rust syntax:homotopy_groups(<postnikov_expr>). Emitted:Term::HomotopyGroups. Receiver-shape check: Postnikov-tower-shaped.homotopy_groupsis a reserved macro-vocabulary identifier. -
G29 —
k_invariants. Rust syntax:k_invariants(<homotopy_expr>). Emitted:Term::KInvariants. Receiver-shape check: homotopy-groups-shaped.k_invariantsis a reserved macro-vocabulary identifier.
Closure-body grammar’s identifier-resolution order extension.
ADR-026 G12 disambiguation, TR-12, and ADR-030’s Closure check at
prism_model! invocation paragraph all enumerate the same five-step
identifier-resolution order. ADR-035 extends step (1)'s reserved
macro-vocabulary identifier set with nine new identifiers: nerve,
chain_complex, homology_groups, betti, cochain_complex,
cohomology_groups, postnikov_tower, homotopy_groups,
k_invariants. The full reserved-identifier set after ADR-035 is twenty
identifiers — the eleven existing (parallel, fold_n, tree_fold,
first_admit, partition_product, partition_coproduct, hash,
recurse, unfold, lift, project) plus the nine ψ-chain
identifiers above.
Closure check at verb! / prism_model! invocation. Each ψ-Term
variant is emitted only by the macro’s recognition of its corresponding
closure-body grammar form (G21..G29). The macro verifies, per the
per-variant grammar form’s resolution rules:
-
Receiver-shape compatibility per the variant’s domain (G21 takes a byte-shaped per-value sequence; G22 takes simplicial-complex; G23/G25 take chain-complex; G24 takes homology-groups; G26 takes cochain-complex; G27 takes simplicial-complex; G28 takes Postnikov-tower; G29 takes homotopy-groups). Resolution-time checks against the receiver expression’s statically-inferable shape; mismatches fail with closure-violation error.
-
ψ-residuals discipline: the verb body’s term arena is walked at proc-macro expansion; any
Term::FirstAdmit,Term::AxisInvocation, orTerm::ApplicationwithPrimitiveOp::Le/Lt/Ge/Gt/Concatemissions fail with a closure-violation error citing the ψ-residual category and the verb’s name. The canonical hash axis is consumed by resolvers (ResolverTuple per ADR-036), not by verb-body terms. -
ResolverTuple presence per ADR-036: the enclosing
prism_model!declaration’sR: ResolverTupleparameter satisfies the marker-trait bounds for each resolver-bound ψ-Term variant the verb body emits.Term::Bettiis resolver-free and emits without ResolverTuple validation. -
Foundation capacity caps per the underlying homology surface:
Term::Bettioutputs are bounded by the substrate’s BettiNumbers byte serialization cap; resolver-bound ψ-Term outputs are bounded by the substrate’s per-category capacity table per the homology bridge’s Handle/Record/Resolved triplet pattern. Outputs exceeding the substrate’s TermValue ceiling (per ADR-028’s reconciliation) propagateCAPACITY_EXCEEDEDshape-violations throughTerm::Try.
Cross-axis composition. ψ-Term emissions compose with the
ψ-residual-free combinatorial-Term emissions in the same Term arena
under one uniform fold pattern. ψ-Term emissions can be operands of
combinatorial-Term variants (e.g., Term::ProjectField extracting a
byte slice from a Term::KInvariants emission;
Term::Application { operator: PrimitiveOp::Eq } comparing two
Term::KInvariants emissions for k-invariant equality);
combinatorial-Term emissions can be operands of ψ-Term variants (the
per-value input to Term::Nerve is typically a Term::Variable
emission or a Term::ProjectField emission extracting a structural
component from the route input).
Substrate-amendment-via-foundation rule. ADR-013/TR-08 covers the
nine new variants and the ψ-residuals discipline. Foundation extends the
Term enum with the nine ψ-Term variants, the catamorphism’s
per-variant fold-rules cover them per the above semantics, the wire
format bumps the format-version constant for the substrate amendment,
the SDK’s verb! and prism_model! macros enforce the ψ-residuals
discipline at proc-macro expansion. Foundation also extends
pipeline::run_route's evaluation environment with the ResolverTuple
per ADR-036 (the architectural co-commitment); this ADR depends on
ADR-036’s mechanism for the resolver-bound variants' fold-rules.
Consequences: Verb bodies express the framework’s full ψ-chain — the
structural-witness arm of op:InferenceOperation — directly through
prism vocabulary. The framework’s verifiability commitment per ADR-001 +
ADR-019 is realized at the closure-body grammar layer: the Term arena’s
evaluation produces homology-class-witnessed values; canonical
computational equivalences flow through the typed-iso surface; the
catamorphism evaluates the ψ-chain alongside the ψ-pipeline through one
uniform fold pattern.
The canonical compiled form is the k-invariants branch ψ_1 → ψ_7 → ψ_8 → ψ_9 — four resolver-bound stages producing a constant-width κ-label that classifies the value’s homotopy type up to weak equivalence. A complete model fuses into a single reference: one verb-body term-arena evaluation producing one label that classifies an equivalence class of values sharing the same canonical structural witness. The data representation is minimal (input bytes + κ-label); the client (the prism model with its typed feature hierarchy, ψ-chain composition, resolvers, substrate) is conceptually larger than the data it operates on.
The ψ-residuals discipline ensures the compiled binary is purely
structural — admission is a property of the value’s k-invariant
signature, not a search predicate. The brute-force Term::FirstAdmit
enumeration retires from verb bodies; Term::FirstAdmit remains in the
substrate for non-verb-body contexts (e.g., conformance-corpus
generators, foundation-internal trace replay) but is not part of the
verb-body term composition vocabulary.
ADR-039 commits the inhabitance verdict realization mapping for the
canonical k-invariants branch. For typed feature hierarchies whose
admission relations are inhabitance questions: a successful
Grounded<Output> IS a cert:InhabitanceCertificate envelope, carrying
the κ-label (the Term::KInvariants emission at ψ_9) as
homotopy-classification structural witness, a concrete cert:witness
ValueTuple derivable from Term::Nerve's 0-simplices at ψ_1, and
cert:searchTrace realized as Grounded::derivation().replay(); an
Err(PipelineFailure) realizes a
cert:InhabitanceImpossibilityCertificate envelope, carrying
proof:InhabitanceImpossibilityWitness as proof payload with
proof:contradictionProof as the canonical-form encoding of the failure
trace. The κ-label and cert:witness are different witness
granularities (homotopy classification vs. concrete ValueTuple); the
canonical k-invariants branch produces both, at the ψ_9 and ψ_1 stages
respectively. The canonical k-invariants branch is therefore the
framework’s verdict-production mechanism for inhabitance questions, with
no separate substrate machinery required.
Rejected alternative 1: Generalize an existing Term variant (e.g.,
Term::Application with new PrimitiveOp discriminants like
PrimitiveOp::NerveBetti) to absorb the ψ-pipeline operations. Rejected
— PrimitiveOp is the substrate’s first-order operation vocabulary
(arithmetic / bitwise / comparison / packing on byte-shaped operands).
The ψ-pipeline operations operate on shape-typed receivers (the nerve’s
source is a constraint-set, not a byte-shaped operand) and produce
structurally-rich outputs (simplicial complexes, chain complexes,
homology groups, etc.). Smuggling them through PrimitiveOp violates
the architectural separation between Term variants (which carry binding
semantics and shape-typed evaluations) and PrimitiveOp discriminants
(which carry byte-shaped first-order operations).
Rejected alternative 2: Introduce a single Term::PsiPipeline
variant with a discriminator field naming the specific ψ-map. Rejected —
conflates nine semantically-distinct operations into one Term variant
with branching fold-rule. Each ψ-map has its own operand structure
(Nerve takes constraints; ChainComplex takes a simplicial complex; Betti
takes homology groups; KInvariants takes homotopy groups; etc.); a
unified variant would need a sum-type-shaped field structure, which
doesn’t fit the architecture’s per-variant fold-rule pattern (each
variant has fixed-arity operands and one fold-rule).
Rejected alternative 3: Express ψ-pipeline operations as axis-trait
methods (per ADR-030) — define a HomologyAxis trait with methods
nerve, chain_complex, etc., and have each prism_model! declaration
include a HomologyAxis in its AxisTuple. Rejected — ψ-pipeline
operations are foundation-vetted substrate machinery defined in the
ontology (spec/src/namespaces/op.rs +
spec/src/namespaces/homology.rs), not domain-specific axes. The
substitution-axis mechanism per ADR-030 is for application-domain
extension (axes carry domain-specific semantics like "which hash
function to use"); the ψ-pipeline IS substrate (the ontology-defined
structural-witness arm of op:InferenceOperation). Architecturally,
ψ-Term variants are first-class substrate constructs paralleling
combinatorial-Term variants. The ResolverTuple per ADR-036 is the
per-value content provision mechanism for ψ-pipeline operations;
resolvers are not axes (resolvers carry per-value content, axes carry
per-domain operation kernels).
Rejected alternative 4: Lower ψ-pipeline operations to combinations
of existing combinatorial-Term variants — encode the nerve construction
as Term::Recurse over the constraint-set graph traversal, the chain
complex as a Term::Match-tree over simplicial dimensions, etc.
Rejected — the ψ-pipeline mathematics is non-trivially complex (Smith
normal form for boundary operator rank, persistence-pair computation for
chain complexes, Kan-condition completion for simplicial complexes,
Postnikov-level k-invariant extraction); encoding in combinatorial-Term
variants would require Term arenas hundreds-to-thousands of nodes deep
per closure invocation, dominated by structural plumbing rather than
mathematical content. The architectural shape — ψ-pipeline operations as
primitive Term variants delegating to foundation’s existing surface
(with per-value content provided through the ResolverTuple per ADR-036)
— keeps the Term arena minimal and the fold-rule per variant
straightforward; the complexity lives in foundation’s existing API
rather than in unrolled Term arena structure.
Rejected alternative 5: Commit only a subset of the nine ψ-Term variants. Rejected — the ontology defines all nine maps as a connected chain; ADR-035 commits to the full chain so the architectural shape is coherent. The canonical k-invariants branch uses four of the nine (Nerve, PostnikovTower, HomotopyGroups, KInvariants); the other five (ChainComplex, HomologyGroups, Betti, CochainComplex, CohomologyGroups) serve narrower compositions. Partial coverage gates the framework’s verifiability commitment on which ontology-defined operations a future ADR happens to land; full coverage commits the architecture once.
Rejected alternative 6: Commit the homology branch (ψ_1 → ψ_2 → ψ_3 → ψ_4 ending at Betti numbers) as the canonical composition. Rejected — β_k extracts rank information only. Two values with the same Betti profile but distinct homology-group structure are indistinguishable under β-equality; two values with the same homology profile but distinct homotopy-group structure are indistinguishable under H-equality. The framework’s verifiability commitment per ADR-001 + ADR-019 is canonical computational equivalences as homology classes; the strongest discriminating witness in the ψ-chain is the k-invariants. The canonical composition is the maximum-discriminating witness with the minimum number of stages.
Rejected alternative 7 (scope refined by ADR-056): Permit
ψ-residuals in verb-body composition. Rejected — ψ-residuals decompose
admission into a runtime predicate enumerated over a value-bytes domain,
recovering the structural-witness relationship by brute-force search
rather than by structural witness. The framework’s verifiability
commitment is canonical computational equivalences as homology classes;
the compiled binary must produce the structural witness directly, not
search for it. The ψ-residuals discipline forces the compiled binary
into the canonical form. ψ-residuals (Term::FirstAdmit,
Term::AxisInvocation, byte-comparison PrimitiveOps, byte-concat
PrimitiveOps) remain in the substrate for non-verb-body contexts
(conformance-corpus generators, foundation-internal trace replay) but
are not part of the verb-body term composition vocabulary. Scope
refined by ADR-056: implementer experience proved the "verb-body"
scope ambiguous across the wiki’s four verb-body categories (route
bodies, compound verb bodies, axis impl bodies, resolver bodies).
ADR-056 restricts the discipline to the route body’s syntactic
surface — the prism_model!-declared route function’s closure body.
Compound verbs declared via verb! per ADR-024 (which fold-fuse into
the route’s evaluation per ADR-054), axis impl bodies per ADR-055, and
resolver bodies per ADR-046 may all use the full substrate vocabulary
including ψ-residual constructs internally. The discipline’s purpose —
keeping admission structurally shaped at the typed-iso surface — is
preserved at the route-body layer where it matters; canonical compound
operations (SHA padding, HMAC, Merkle, tensor saturation) are now
substrate-Term-decomposable per ADR-055’s universal discipline.
Discipline-scope boundary (refined by ADR-056). The ψ-residuals
discipline applies to the route body’s syntactic surface per ADR-056
— the closure body the author writes directly in the
prism_model!-declared route function. Three categories of "verb
body" the wiki recognizes are outside the discipline’s scope: (1)
compound verbs declared via verb! per ADR-024 (their internal Term
arenas fold-fuse into the route’s evaluation per ADR-054 but are
syntactically distinct from the route’s direct emissions); (2) axis impl
bodies per ADR-055’s universal substrate-Term verb body discipline (the
body clause emitted by axis! per ADR-030 + ADR-052); (3) resolver
bodies per ADR-036 (arbitrary Rust function bodies implementing the
substrate’s typed-carrier structural transform; the iterative-resolution
discipline per ADR-043 specifies the resolver-internal computational
pattern). All three categories may use the full substrate vocabulary
including byte-comparison/concat PrimitiveOps and Term::AxisInvocation
internally. The disciplines reside at different layers without
contradiction — route-body composition is structural inference at the
typed-iso surface (ADR-035 + ADR-056); compound-verb and axis-impl-body
composition is fold-fusion-realized substrate work the catamorphism’s
evaluation transparently inlines (ADR-054 + ADR-055); resolver-body
realization is the substrate’s structural-transform mechanism the
catamorphism’s resolver-bound fold-rules dispatch to (ADR-043).
ADR-036 — ResolverTuple substrate parameter: per-value content provision for resolver-bound substrate operations
Status: Accepted. Resolver-trait surface amended by ADR-060. The
eight ψ-stage resolver traits change from the writer-style
fn resolve(&self, input: &[u8], out: &mut [u8]) → Result<usize, ShapeViolation>
to returning a TermValue directly:
fn resolve(&self, input: TermValue<'a, {carrier_inline_bytes::<B>()}>) → Result<TermValue<'a, {carrier_inline_bytes::<B>()}>, ShapeViolation>.
The resolver constructs whichever carrier variant its output requires
(Inline / Borrowed / Stream) rather than writing into a
caller-supplied buffer and returning a byte count; the per-ψ-stage
output byte-width ceilings (*_OUTPUT_BYTES_MAX) are removed (carrier
widths derive from foundation const fn). The ResolverTuple mechanism,
the marker-trait accessors, and the per-value-content-provision
architecture are otherwise unchanged. Read this ADR’s writer-style
resolve signature as superseded by ADR-060.
Context: The ontology defines resolvers as Bridge-space constructs
(spec/src/namespaces/resolver.rs): "Resolvers implement the map Π :
T_n → Part(R_n), transforming a type declaration into a partition of the
ring. Resolution requests come from user-space; execution occurs in the
kernel." Foundation’s homology bridge implements the resolver pattern as
Handle/Record/Resolved triplets — the application provides a
Resolver<H> instance parameterized by the model’s canonical hash axis;
the resolver maps a content-addressed input byte sequence to a per-value
output byte sequence; the catamorphism consults the resolver at
evaluation time when per-value content is needed.
ADR-035 introduces nine ψ-Term variants whose fold-rules consult
resolvers at evaluation time — eight resolver-bound variants (Nerve,
ChainComplex, HomologyGroups, CochainComplex, CohomologyGroups,
PostnikovTower, HomotopyGroups, KInvariants) and one resolver-free
variant (Betti). The resolver-bound variants require the catamorphism’s
evaluation environment to carry resolver instances accessible during
fold-rule evaluation. The current evaluation environment per ADR-022
D5 + ADR-030 carries H: HostTypes, B: HostBounds,
A: AxisTuple + Hasher (the substrate parameters identifying the host
platform, the host capacity bounds, and the substitution-axis tuple with
the canonical hash axis bound); it has no provision for resolver
instances.
The architectural shape is established by precedent. ADR-030’s AxisTuple
mechanism committed the parallel pattern for axis-trait-method dispatch:
a tuple-of-bounded-types parameter on the model declaration; a
tuple-position determines an axis_index for dispatch; a
KERNEL_<NAME> const determines a kernel_id for method selection
within an axis; the catamorphism consults the AxisTuple at evaluation
time. The ResolverTuple mechanism parallels this pattern for
resolver-bound substrate operations: a tuple-of-bounded-types parameter
on the model declaration; a tuple-position determines a resolver_index
for dispatch; the catamorphism’s resolver-bound ψ-Term fold-rules
consult the ResolverTuple at evaluation time.
The architectural separation between AxisTuple and ResolverTuple:
AxisTuple carries per-domain operation kernels — axis methods are
type-associated (kernel selection via const IDs, hasher methods invoked
via <A as Hasher>::initial()); axis instances are conceptually
witnesses of the type-level structure with no per-instance state to
thread through value parameters. ResolverTuple carries per-value
content provision — resolver methods are instance-associated (the
resolver’s resolve method takes &self); resolver instances carry
application-specific configuration and per-call state, and a &R
reference threads through the catamorphism’s evaluation environment.
Decision: The architecture commits the ResolverTuple substrate
parameter as a fourth model-declaration parameter alongside
H: HostTypes, B: HostBounds, A: AxisTuple + Hasher. The model
declaration’s parameter shape extends from <H, B, A> to <H, B, A, R>
where R: ResolverTuple carries application-provided resolver instances
for the resolver-bound substrate operations. R defaults to
NullResolverTuple so model declarations that emit no resolver-bound
ψ-Term variants can omit the parameter; declarations that emit any
resolver-bound ψ-Term variant must declare the parameter explicitly (the
SDK proc-macro’s ψ-residuals walk per ADR-035 detects resolver-bound
emissions and rejects the declaration if R is the NullResolverTuple
default).
The PrismModel trait shape. Foundation extends the PrismModel
trait with the ResolverTuple parameter:
pub trait PrismModel<H, B, A, R = NullResolverTuple>
where
H: HostTypes,
B: HostBounds,
A: AxisTuple + Hasher,
R: ResolverTuple,
{
type Input;
type Output;
type Route;
fn forward(input: Self::Input) -> Result<Grounded<Self::Output>, PipelineFailure>;
}The trait is sealed per ADR-022 D1 (SDK-seal mechanism); the associated-type shape-typing bounds are foundation-vetted at trait declaration (foundation chooses the specific bounds when reconciling — the architectural commitment is that the model’s Input, Output, and Route types are substrate-conformant per the established shape-typing surface).
The ResolverTuple trait. Foundation declares a sealed
ResolverTuple trait paralleling AxisTuple per ADR-030:
/// Sealed trait for tuple-of-resolvers parameters on the model declaration.
/// Applications declare ResolverTuple impls through the SDK's `resolver!` macro.
/// Sealed per ADR-022 D1.
pub trait ResolverTuple {
/// Number of resolver positions in this tuple. Bounded by
/// MAX_RESOLVER_TUPLE_ARITY.
const ARITY: usize;
/// Resolver category at each tuple position.
const CATEGORIES: &'static [ResolverCategory];
}
pub enum ResolverCategory {
/// ψ_1 — per-value bytes → SimplicialComplex.
Nerve,
/// ψ_2 — SimplicialComplex → ChainComplex.
ChainComplex,
/// ψ_3 — ChainComplex → HomologyGroups.
HomologyGroup,
/// ψ_5 — ChainComplex → CochainComplex.
CochainComplex,
/// ψ_6 — CochainComplex → CohomologyGroups.
CohomologyGroup,
/// ψ_7 — SimplicialComplex → PostnikovTower.
Postnikov,
/// ψ_8 — PostnikovTower → HomotopyGroups.
HomotopyGroup,
/// ψ_9 — HomotopyGroups → KInvariants.
KInvariant,
// Future categories per ADR-013/TR-08 substrate amendments.
}
/// Foundation-internal byte-level discriminator emitted by every
/// Null<Category>Resolver impl. The catamorphism's resolver-bound
/// fold-rule receives the discriminator from the resolver's
/// shape-violation result and propagates it through Term::Try per
/// ADR-022 D3 G9 (the verb body's outer Term::Try handler recovers
/// the resolver-absent case). The specific byte value is
/// foundation-vetted at reconciliation; the architectural commitment
/// is that a single foundation-internal discriminator byte exists.
pub const RESOLVER_ABSENT_DISCRIMINATOR: u8;Resolver trait shape — uniform byte-buffer surface. Each resolver
category has a corresponding sealed Resolver trait declared by
foundation. The eight resolver traits share a uniform writer-style
resolve method signature — byte-sequence input plus byte-buffer output
plus byte-count return — so the catamorphism’s evaluation environment
threads byte buffers between ψ-stages with no allocation and no
*Record<H> typed-return surface:
pub trait NerveResolver<H: Hasher> {
/// ψ_1: per-value bytes → SimplicialComplex serialization.
/// Returns the number of bytes written to `out`. Errors with a
/// ShapeViolation on capacity-exceeded, resolver-absent
/// (NullNerveResolver returns RESOLVER_ABSENT via the
/// `https://uor.foundation/resolver/RESOLVER_ABSENT` shape IRI),
/// or other resolution failure modes. Sealed per ADR-022 D1.
fn resolve(
&self,
input: &[u8],
out: &mut [u8],
) -> Result<usize, ShapeViolation>;
}
pub trait ChainComplexResolver<H: Hasher> {
/// ψ_2: SimplicialComplex serialization → ChainComplex serialization.
/// Sealed per ADR-022 D1.
fn resolve(&self, input: &[u8], out: &mut [u8]) -> Result<usize, ShapeViolation>;
}
// ... and analogously for HomologyGroupResolver, CochainComplexResolver,
// CohomologyGroupResolver, PostnikovResolver, HomotopyGroupResolver,
// KInvariantResolver — eight resolver traits total. Each is parameterized
// by H: Hasher (the model's canonical hash axis per ADR-022 D5 + ADR-030,
// the A: AxisTuple + Hasher substrate parameter); resolver impls compute
// content-addressed fingerprints using the model's hash axis.
// Each declares the same writer-style resolve method shape.The uniform byte-buffer surface is the architectural commitment for
resolver-bound substrate operations. ResolverCategory variants
distinguish the eight ψ-stages at the type-trait level (each resolver
trait is a distinct sealed type); the resolve method’s signature is
uniform across all eight so the catamorphism’s evaluation environment
can thread byte buffers between ψ-stages without per-stage allocation.
Resolver impls that need per-call structural intermediates allocate them
internally; the byte-buffer surface is the resolver/catamorphism
interface.
Resolver impls are typically stateless. The resolver’s data is the
per-call input byte sequence; the resolver’s parameterization is the
model’s canonical hash axis (H: Hasher). Configuration that varies per
resolver invocation flows through the verb body’s input (the value the
verb body operates on); configuration that varies per model deployment
flows through the resolver impl’s construction. The canonical resolver
impl pattern is a stateless type that delegates the resolve body to a
stateless byte-transformation function; foundation chooses the specific
stateless-type idiom at reconciliation.
Has<Category>Resolver<H> marker traits. Foundation declares one
marker trait per ResolverCategory variant, each providing the typed
accessor for that category:
pub trait HasNerveResolver<H: Hasher>: ResolverTuple {
fn nerve_resolver(&self) -> &dyn NerveResolver<H>;
}
pub trait HasChainComplexResolver<H: Hasher>: ResolverTuple {
fn chain_complex_resolver(&self) -> &dyn ChainComplexResolver<H>;
}
// ... and analogously for HasHomologyGroupResolver, HasCochainComplexResolver,
// HasCohomologyGroupResolver, HasPostnikovResolver, HasHomotopyGroupResolver,
// HasKInvariantResolver — eight marker traits total.Null resolver baselines. Foundation provides eight
Null<Category>Resolver<H> impls — one per resolver category. Each
Null* impl’s resolve method returns a ShapeViolation carrying the
https://uor.foundation/resolver/RESOLVER_ABSENT shape IRI and the
RESOLVER_ABSENT_DISCRIMINATOR byte. Foundation also provides a
NullResolverTuple impl satisfying every Has<Category>Resolver<H>
marker trait by returning the corresponding Null* resolver from each
accessor. Verbs whose ψ-Term emissions consult resolver-bound categories
with the NullResolverTuple default fail at evaluation time with
RESOLVER_ABSENT propagated through Term::Try per ADR-022 D3 G9.
The resolver! SDK macro. Application authors declare ResolverTuple
impls through a new SDK macro paralleling axis! per ADR-030. The macro
recognizes a fixed field-name-to-category mapping — foundation defines
the eight canonical field names; applications must use these names; the
macro emits all eight Has<Category>Resolver<H> impls so the resulting
struct satisfies run_route's where-clause unconditionally (declared
fields delegate to the user’s resolver; undeclared categories delegate
to NullResolverTuple's Null* impls):
// Foundation-canonical field-name-to-category mapping:
// field name | ResolverCategory variant | resolver trait
// --------------------+--------------------------+--------------------------
// nerve | Nerve | NerveResolver<H>
// chain_complex | ChainComplex | ChainComplexResolver<H>
// homology_groups | HomologyGroup | HomologyGroupResolver<H>
// cochain_complex | CochainComplex | CochainComplexResolver<H>
// cohomology_groups | CohomologyGroup | CohomologyGroupResolver<H>
// postnikov | Postnikov | PostnikovResolver<H>
// homotopy_groups | HomotopyGroup | HomotopyGroupResolver<H>
// k_invariants | KInvariant | KInvariantResolver<H>
resolver! {
pub struct MyApplicationResolvers<H: Hasher> {
nerve: MyNerveResolver<H>,
postnikov: MyPostnikovResolver<H>,
homotopy_groups: MyHomotopyGroupResolver<H>,
k_invariants: MyKInvariantResolver<H>,
// ... only the categories the application's verbs require;
// undeclared categories delegate to NullResolverTuple's
// Null* impls at runtime (RESOLVER_ABSENT recoverable via
// the catamorphism's Term::Try handler if the verb body
// wraps the ψ-Term emission).
}
}The macro emits: the struct definition with the declared fields; the
ResolverTuple impl with ARITY = declared-field count and
CATEGORIES = declared-field-category array; for each of the eight
resolver categories an impl block satisfying the corresponding
Has<Category>Resolver<H> marker trait — the accessor delegates to the
user’s declared field when present, and to NullResolverTuple's Null*
impl when the category is undeclared; the SDK seal satisfactions per
ADR-022 D1.
Field-name validation is at proc-macro expansion: unrecognized field
names fail with a closure-violation error citing the recognized
field-name set. The resolver! macro’s "emit all eight impls" pattern
is what makes the model declaration’s prism_model! invocation compose
with run_route's where-clause: run_route requires all eight
Has<Category>Resolver<A> bounds unconditionally on the resolver tuple,
regardless of which ψ-Term variants the model’s verb body emits; the
runtime check for resolver-absence fires through the RESOLVER_ABSENT
shape-violation when the catamorphism’s fold-rule consults a category
whose accessor returns the Null* resolver.
Foundation pipeline integration — run_route signature. Foundation
extends pipeline::run_route to thread the resolver tuple through the
catamorphism’s evaluation environment. The function signature carries
five type parameters and one value parameter beyond the input:
pub fn run_route<H, B, A, M, R>(
input: M::Input,
resolvers: &R,
) -> Result<Grounded<M::Output>, PipelineFailure>
where
H: HostTypes,
B: HostBounds,
A: AxisTuple + Hasher,
M: PrismModel<H, B, A, R>,
R: ResolverTuple
+ HasNerveResolver<A>
+ HasChainComplexResolver<A>
+ HasHomologyGroupResolver<A>
+ HasCochainComplexResolver<A>
+ HasCohomologyGroupResolver<A>
+ HasPostnikovResolver<A>
+ HasHomotopyGroupResolver<A>
+ HasKInvariantResolver<A>,
<M as PrismModel<H, B, A, R>>::Route: AsRef<&'static TermArena>,
{ /* ... */ }The five type parameters carry: H (the host-platform witness type),
B (the host-platform capacity bounds), A (the substitution-axis
tuple with the canonical hash axis bound — the resolver-trait
parameterization), M (the prism model whose route the call invokes),
R (the application-provided resolver tuple). The signature takes no
axes value parameter: axis methods are type-associated and invoked
through <A as Hasher>::initial() per ADR-022 D5; only the resolver
tuple flows as a value parameter.
The where-clause requires all eight Has<Category>Resolver<A> bounds
unconditionally on the resolver tuple. The resolver! macro’s "emit all
eight impls" pattern satisfies this requirement; applications need not
enumerate the bounds. The architectural commitment is that run_route
is uniform across verb-body ψ-Term emission profiles — the same
signature handles verbs emitting one resolver-bound ψ-Term variant and
verbs emitting all eight, with the runtime check for resolver-absence
firing at the catamorphism’s fold-rule consultation point for undeclared
categories.
Application-side resolver instantiation. The application
instantiates its ResolverTuple impl and passes the instance to
pipeline::run_route (or to the model’s forward method, whose
canonical body forwards to run_route per ADR-022 D5). The resolver
tuple’s lifetime is the application’s responsibility; run_route
borrows &R and returns the route’s output. Resolver resolve methods
take &self; resolvers that need mutable internal state use interior
mutability per Rust’s standard pattern, with the application accepting
any thread-safety implications.
Standard library resolver baselines. The standard library (per
ADR-031’s "prism IS the standard library" framing) contributes
application-neutral-within-domain resolver baselines paralleling axis
baselines. Standard-library sub-crates publish resolver impls that
compose with common ψ-stages over common typed-feature-hierarchy shapes;
the closure discipline applies identically to standard-library and
third-party resolvers (both go through the resolver! macro and are
seal-checked at proc-macro expansion). Standard-library resolver
baselines have no foundation-special status; they are sub-crates of
prism with operational distinctions (maintenance, conformance test
ownership, recommended-for-production status) but no architectural
distinction.
ResolverTuple arity cap. ResolverTuple arity is bounded by
MAX_RESOLVER_TUPLE_ARITY, a foundation-vetted type-system impl-table
cap per ADR-037’s clause (2). The architectural lower bound is
card(ResolverCategory) — the cardinality of the resolver-category
enumeration (8 per ResolverCategory's variants: Nerve,
ChainComplex, HomologyGroup, CochainComplex, CohomologyGroup,
Postnikov, HomotopyGroup, KInvariant) — plus headroom for any
ADR-013/TR-08 substrate amendments that revise ResolverCategory. The
architecture binds the lower bound to card(ResolverCategory)
structurally: if a substrate amendment revises the enumeration’s
cardinality (adding or removing a resolver-bound substrate operation),
foundation revision adjusts the emitted value accordingly. The cap is
foundation-vetted (Rust-language carve-out: per-arity impl emission
cannot be parametric on downstream applications' HostBounds impls);
the architectural commitment is to the structural derivation, not to the
specific number.
Substrate-amendment-via-foundation rule. ADR-013/TR-08 covers the
ResolverTuple substrate amendment. Foundation declares the
ResolverTuple trait, the ResolverCategory enum, the eight resolver
traits per ADR-035, the eight marker traits, the
MAX_RESOLVER_TUPLE_ARITY const, the RESOLVER_ABSENT_DISCRIMINATOR
const, the eight Null* resolver impls, and the NullResolverTuple
impl. Foundation extends pipeline::run_route with the
five-type-parameter signature and the
eight-Has<Category>Resolver<A>-bound where-clause. Foundation’s wire
format bumps the format-version constant for the substrate amendment.
The SDK declares the resolver! macro with the
eight-canonical-field-name table.
Consequences: The closure-body grammar’s evaluation environment
carries application-provided resolver instances accessible from ψ-Term
variant fold-rules per ADR-035. Per-value structural admission
witnessing — the framework’s load-bearing capability — flows through the
typed-iso surface end-to-end. The application provides resolver impls
through the resolver! macro; the model declares the ResolverTuple
parameter; foundation’s catamorphism evaluates ψ-Term variants by
consulting the ResolverTuple at evaluation time.
The framework’s op:InferenceOperation (ι = P ∘ Π ∘ G, the ψ-pipeline
composed) is fully realized at the closure-body grammar layer: the
ψ-pipeline’s resolution arm flows through combinatorial Term variants
per the existing substrate; the ψ-chain’s structural-witness arm flows
through ψ-Term variants per ADR-035 with per-value content provided
through the ResolverTuple per ADR-036. The canonical compiled form
(k-invariants branch per ADR-035) consumes four resolvers
(NerveResolver, PostnikovResolver, HomotopyGroupResolver,
KInvariantResolver); applications that compose other ψ-Term branches
consume the corresponding additional resolvers from their resolver!
declaration.
Rejected alternative 1: Carry resolver instances through the
AxisTuple by introducing a dedicated ResolverAxis trait whose method
names match resolver categories. Rejected — conflates two
architecturally-distinct concerns. AxisTuple methods are type-associated
(no per-instance state to thread); ResolverTuple methods are
instance-associated (resolver resolve takes &self; resolvers carry
application-specific configuration). The architectural separation per
ADR-030 and ADR-036 is calibrated against this difference.
Rejected alternative 2: Use typed *Record<H> return values for
the resolver resolve methods. Rejected — typed return values force
per-stage allocation in the catamorphism’s evaluation environment. The
resolver’s output surface is writer-style &mut [u8] (zero allocation);
typed discrimination of resolver inputs (the prior ψ-stage’s output) is
carried by zero-allocation #[repr(transparent)] newtype views per
ADR-041, not by typed returns.
Rejected alternative 3: Thread resolvers through
pipeline::run_route as ad-hoc parameters per resolver category.
Rejected — the function signature would extend with one parameter per
resolver category, growing unboundedly with each substrate amendment.
The tuple-of-bounded-types pattern per ADR-030 is specifically designed
to handle this — one parameter (R: ResolverTuple) carries an
arbitrary-arity collection of resolver instances.
Rejected alternative 4: Make resolvers globally accessible through a
thread-local or singleton mechanism. Rejected — global state breaks the
framework’s pure-functional commitment; pipeline::run_route is a
deterministic mapping from inputs to outputs, and global resolver state
would introduce hidden inputs.
Rejected alternative 5: Provide resolver implementations as part of foundation rather than application-provided. Rejected — the ontology classifies resolvers as Bridge-space constructs ("user-requested, kernel-executed"); resolution is application-content-bound by ontology design (the per-value content is application-specific). Foundation provides the trait surface, the Handle/Record/Resolved triplet pattern, and Null* resolver baselines for resolver-absent contexts; applications provide concrete resolver impls for their per-value content. The standard library contributes application-neutral-within-domain baselines per ADR-031, but these are still application-provided in the architectural sense (the prism standard library is, per ADR-031, just a set of sub-crates with no foundation-special status).
ADR-037 — HostBounds-parametric capacity bounds: completing ADR-018’s commitment for data-shape capacities
Status: Accepted. Superseded in part by ADR-060. The byte-width
subset of branch (1) — the 12 byte-width capacity constants
(TERM_VALUE_MAX_BYTES, AXIS_OUTPUT_BYTES_MAX,
ROUTE_INPUT_BUFFER_BYTES, ROUTE_OUTPUT_BUFFER_BYTES, and the 8
ψ-stage *_OUTPUT_BYTES_MAX ceilings) — and DefaultHostBounds are
removed by ADR-060: downstream implementation proved the byte-width caps
a stable-Rust workaround (a pinned literal absent generic_const_exprs)
whose application-overridability was fictional (foundation internals
read the width through the hardcoded DefaultHostBounds path). ADR-060
replaces them with the source-polymorphic TermValue carrier (derived
inline width, uncapped Borrowed/Stream carriers) and per-ψ-stage carrier
widths derived by foundation const fn. The 10 retained migrated
constants (the structural counts BETTI_DIMENSION_MAX,
NERVE_CONSTRAINTS_MAX, NERVE_SITES_MAX, JACOBIAN_SITES_MAX,
AFFINE_COEFFS_MAX, CONJUNCTION_TERMS_MAX and the catamorphism/trace
bounds FOLD_UNROLL_THRESHOLD, RECURSION_TRACE_DEPTH_MAX,
OP_CHAIN_DEPTH_MAX, UNFOLD_ITERATIONS_MAX), the 4 pre-existing
constants, and branch (2)'s type-system impl-table caps remain in force.
The rest of this ADR is preserved as the historical record of the
migration commitment; read its byte-width-cap and DefaultHostBounds
content as superseded by ADR-060.
Context: ADR-018 commits the load-bearing principle that
HostBounds carries every capacity bound that varies along the
principal data path, and that the architectural surface admits no
capacity bound outside HostBounds. The decision treats
foundation-fixed caps "as a defect, not a tradeoff." The closing
sentence — "every signature in prism's and uor-foundation's public
API that admits a value with a capacity-bounded width parameterizes that
width through the application’s selected HostBounds" — is the
architectural surface commitment.
At the foundation’s current snapshot, HostBounds carries four
associated constants (FINGERPRINT_MIN_BYTES, FINGERPRINT_MAX_BYTES,
TRACE_MAX_EVENTS, WITT_LEVEL_MAX_BITS); fourteen further data-shape
capacity caps remain as free-standing pub const usize declarations
across the foundation’s pipeline and enforcement components —
TERM_VALUE_MAX_BYTES, AXIS_OUTPUT_BYTES_CEILING,
FOLD_UNROLL_THRESHOLD, MAX_BETTI_DIMENSION, NERVE_CONSTRAINTS_CAP,
NERVE_SITES_CAP, JACOBIAN_MAX_SITES, RECURSION_TRACE_MAX_DEPTH,
MAX_OP_CHAIN_DEPTH, AFFINE_MAX_COEFFS, CONJUNCTION_MAX_TERMS,
ROUTE_INPUT_BUFFER_BYTES, ROUTE_OUTPUT_BUFFER_BYTES,
UNFOLD_MAX_ITERATIONS — plus the eight ψ-stage resolver output
byte-buffer ceilings on the per-ψ-stage resolver traits per ADR-036.
Plus two type-system tuple-impl-table caps: MAX_AXIS_TUPLE_ARITY (per
ADR-030) and MAX_RESOLVER_TUPLE_ARITY (per ADR-036).
Each data-shape cap is a capacity bound that varies along the principal
data path: an application whose typed feature hierarchy is deeper, whose
ψ-stage resolver outputs are wider, whose Postnikov-tower truncation
requires more iterations, whose constraint conjunction admits more bound
predicates, or whose nerve construction’s constraint geometry is richer
than the foundation-vetted default cannot vary the cap by selecting
HostBounds — the cap is foundation-fixed and collapses the
substitution axis at that bound. This is exactly the defect ADR-018
commits the architecture against.
Type-system impl-table caps (MAX_AXIS_TUPLE_ARITY,
MAX_RESOLVER_TUPLE_ARITY) are structurally different. They bound the
arity of tuple types for which foundation’s blanket-impl macros emit
AxisTuple / ResolverTuple impls. Rust currently lacks variadic
generics; per-arity impl emission is required, and the emission set must
be committed at foundation’s build time (Rust macros emit at
foundation’s build, not at downstream applications' builds). These caps
are foundation’s per-arity emission limits, not application-varying
capacity bounds. ADR-018’s "every capacity bound that varies along the
principal data path" most naturally applies to data-shape capacity
surfaces; type-system impl-table emission limits are structurally
bounded by the Rust language and require their own architectural
commitment.
Decision: ADR-037 commits the two-branch architectural cleanup:
(1) Data-shape capacity caps migrate to HostBounds associated
constants. All 14 free-standing pub const usize capacity caps plus
the eight ψ-stage resolver output byte-buffer ceilings migrate.
HostBounds extends:
pub trait HostBounds {
// Existing associated constants (preserved verbatim):
const FINGERPRINT_MIN_BYTES: usize;
const FINGERPRINT_MAX_BYTES: usize;
const TRACE_MAX_EVENTS: usize;
const WITT_LEVEL_MAX_BITS: u32;
// ADR-037 migrations from foundation-fixed pub const usize to
// HostBounds associated constants:
/// Catamorphism's per-variant TermValue byte-buffer capacity.
/// Migrated from foundation-fixed TERM_VALUE_MAX_BYTES (ADR-029).
const TERM_VALUE_MAX_BYTES: usize;
/// Per-axis kernel output byte-buffer capacity.
/// Migrated from foundation-fixed AXIS_OUTPUT_BYTES_CEILING (ADR-030).
const AXIS_OUTPUT_BYTES_MAX: usize;
/// `fold_n` unroll-vs-recurse threshold.
/// Migrated from foundation-fixed FOLD_UNROLL_THRESHOLD (ADR-029).
const FOLD_UNROLL_THRESHOLD: usize;
/// BettiNumbers byte-serialization dimension cap.
/// Migrated from foundation-fixed MAX_BETTI_DIMENSION (ADR-035).
const BETTI_DIMENSION_MAX: usize;
/// Nerve-stage constraint-set capacity.
/// Migrated from foundation-fixed NERVE_CONSTRAINTS_CAP.
const NERVE_CONSTRAINTS_MAX: usize;
/// Nerve-stage site-set capacity.
/// Migrated from foundation-fixed NERVE_SITES_CAP.
const NERVE_SITES_MAX: usize;
/// Jacobian-stage site-set capacity.
/// Migrated from foundation-fixed JACOBIAN_MAX_SITES.
const JACOBIAN_SITES_MAX: usize;
/// Recursion trace depth ceiling.
/// Migrated from foundation-fixed RECURSION_TRACE_MAX_DEPTH.
const RECURSION_TRACE_DEPTH_MAX: usize;
/// Op chain depth ceiling.
/// Migrated from foundation-fixed MAX_OP_CHAIN_DEPTH.
const OP_CHAIN_DEPTH_MAX: usize;
/// `ConstraintRef::Affine` fixed-array coefficient count cap.
/// Migrated from foundation-fixed AFFINE_MAX_COEFFS.
const AFFINE_COEFFS_MAX: usize;
/// `ConstraintRef::Conjunction.conjuncts` fixed-array term count cap.
/// Migrated from foundation-fixed CONJUNCTION_MAX_TERMS.
const CONJUNCTION_TERMS_MAX: usize;
/// Route input buffer byte-size.
/// Migrated from foundation-fixed ROUTE_INPUT_BUFFER_BYTES.
const ROUTE_INPUT_BUFFER_BYTES: usize;
/// Route output buffer byte-size.
/// Migrated from foundation-fixed ROUTE_OUTPUT_BUFFER_BYTES.
const ROUTE_OUTPUT_BUFFER_BYTES: usize;
/// `Term::Unfold` iteration ceiling.
/// Migrated from foundation-fixed UNFOLD_MAX_ITERATIONS.
const UNFOLD_ITERATIONS_MAX: usize;
// Eight ψ-stage resolver output byte-buffer ceilings (per ADR-036's
// eight resolver-bound ψ-Term variants per ADR-035). Migrated from
// foundation-internal byte-buffer ceilings on each resolver trait.
const NERVE_OUTPUT_BYTES_MAX: usize;
const CHAIN_COMPLEX_OUTPUT_BYTES_MAX: usize;
const HOMOLOGY_GROUPS_OUTPUT_BYTES_MAX: usize;
const COCHAIN_COMPLEX_OUTPUT_BYTES_MAX: usize;
const COHOMOLOGY_GROUPS_OUTPUT_BYTES_MAX: usize;
const POSTNIKOV_TOWER_OUTPUT_BYTES_MAX: usize;
const HOMOTOPY_GROUPS_OUTPUT_BYTES_MAX: usize;
const K_INVARIANTS_OUTPUT_BYTES_MAX: usize;
// Future data-shape capacities added per ADR-018's "any further
// capacity" clause migrate here; foundation does not add new
// free-standing pub const usize capacity caps.
}Foundation’s DefaultHostBounds impl extends to carry the foundation’s
prior fixed values as defaults across the 22 newly-migrated associated
constants (14 free-standing data-shape caps plus 8 ψ-stage resolver
output ceilings), bringing the total HostBounds surface to 26
associated constants when combined with the 4 pre-existing constants per
ADR-018 (FINGERPRINT_MIN_BYTES, FINGERPRINT_MAX_BYTES,
TRACE_MAX_EVENTS, WITT_LEVEL_MAX_BITS). Applications selecting
DefaultHostBounds see no observable change beyond type-parameter
threading. Applications whose typed feature hierarchies need different
ceilings declare their own HostBounds impl; foundation’s pipeline
signatures parameterize on B: HostBounds and consume
<B as HostBounds>::CONST_NAME.
The migration shapes the variant data structures parametrically.
ConstraintRef::Conjunction.conjuncts becomes
[LeafConstraintRef; <B as HostBounds>::CONJUNCTION_TERMS_MAX];
ConstraintRef::Affine's coefficient array becomes parameterized by
<B as HostBounds>::AFFINE_COEFFS_MAX; ψ-stage resolver impls write
into byte buffers sized by the corresponding
<B as HostBounds>::*_OUTPUT_BYTES_MAX; route input/output buffers,
recursion trace depth, op chain depth, Unfold iteration ceiling,
Jacobian site count, and Nerve constraint/site data shapes all
parameterize on B: HostBounds.
The discipline is testable architecturally: the conformance corpus
enumerates, for each capacity-bounded width in the substrate API
surface, the test "this signature parameterizes the bound through
<B as HostBounds>." Free-standing pub const usize capacity caps in
the foundation’s pipeline and enforcement components are non-conforming.
(2) Type-system impl-table caps stay foundation-vetted with structural
justification. MAX_AXIS_TUPLE_ARITY and MAX_RESOLVER_TUPLE_ARITY
are foundation’s macro-emission limits for AxisTuple / ResolverTuple
blanket-impl generation. Rust’s lack of variadic generics requires
per-arity emission at foundation’s build time; the emission set cannot
be parametric on downstream applications' HostBounds impls. The
architectural commitment per ADR-037:
-
MAX_AXIS_TUPLE_ARITY. Foundation-vetted, currently emitted at a foundation-chosen arity. Motivated by current standard-library Layer-3 sub-crate AxisTuple usages plus reasonable headroom. Foundation revision adjusts the value when standard-library or application needs evolve. Applications declaring AxisTuples of arity greater than the foundation-vetted ceiling are rejected at the type-system level (noAxisTupleimpl exists for tuples beyond the emitted set). -
MAX_RESOLVER_TUPLE_ARITY. Foundation-vetted. Structurally bounded below bycard(ResolverCategory)— the count of resolver-bound substrate operations per ADR-035 (8 perResolverCategory's variants:Nerve,ChainComplex,HomologyGroup,CochainComplex,CohomologyGroup,Postnikov,HomotopyGroup,KInvariant) plus headroom for any ADR-013/TR-08 substrate amendments that revise the enumeration’s cardinality. The cap is structurally derived, not arbitrary; the prior ADR-036 framing of "= 16, twice the AxisTuple cap" retires — the lower bound iscard(ResolverCategory), not a coincidence withMAX_AXIS_TUPLE_ARITY. ADR-013/TR-08 substrate amendments that reviseResolverCategoryautomatically adjust the lower bound; foundation revision adjusts the emitted value accordingly.
Rust-language carve-out from ADR-018. Type-system impl-table
emission limits are not capacity bounds in the ADR-018 sense — they are
foundation’s per-arity impl emission machinery limits, structurally
bound to Rust’s compilation model. ADR-018’s commitment about no
capacity bound outside HostBounds applies to application-varying
capacity bounds (data-shape capacities); type-system impl-table emission
limits are foundation’s implementation scope, vetted by foundation
revision with structural justification (card(ResolverCategory) lower
bound; standard-library AxisTuple usage motivation). The carve-out is
explicit, bounded, and language-conditioned: it applies under Rust’s
current absence of variadic generics. If variadic generics stabilize in
Rust, the impl-table caps become amenable to the same
HostBounds-parametric treatment under this ADR’s discipline; the
migration follows the ADR-013/TR-08 substrate-amendment-via-foundation
rule.
The foundation-internal RESOLVER_ABSENT_DISCRIMINATOR byte constant
(per ADR-036) is not a capacity bound — it is a discriminator value
with no architectural variation across applications. It stays
foundation-fixed (ADR-018’s discipline does not apply).
Consequences: The data-shape capacity surface is
HostBounds-parametric end-to-end. Applications size their data flows
by their selected HostBounds. ADR-018’s commitment is restored across
the substrate’s API surface for all data-shape capacities. The
Conjunction variant’s fixed-size array, the Affine operand’s fixed-size
array, the route input/output buffer sizes, the eight ψ-stage resolver
output byte buffers, the Postnikov-tower / Jacobian / nerve data shapes,
the recursion trace depth, the op chain depth, the Unfold iteration
ceiling, and the catamorphism’s per-variant TermValue byte buffer all
parameterize on B: HostBounds.
Type-system impl-table caps are explicitly foundation-vetted with
structural justification: MAX_AXIS_TUPLE_ARITY motivated by current
usage; MAX_RESOLVER_TUPLE_ARITY ≥ card(ResolverCategory) with
headroom. The architecture admits the Rust-language carve-out and names
it explicitly rather than papering over it with a non-functional
macro-emission story.
The closed-catalog ConstraintRef variant set is unchanged; only the
fixed-array sizes within variants gain HostBounds parameterization.
The substrate’s API surface remains generic over B: HostBounds; the
application’s HostBounds impl’s associated constants drive variant
data shapes at the application’s compile time.
Rejected alternative 1: Keep all caps foundation-fixed and admit class exceptions to ADR-018. Rejected — ADR-018 treats foundation-fixed data-shape caps as a defect. The two-branch reconciliation honestly distinguishes data-shape capacities (subject to ADR-018, all 14 + 8 migrate) from type-system impl-table emission limits (Rust-language carve-out, structurally bounded).
Rejected alternative 2: Migrate type-system impl-table caps to
"HostBounds-driven macro emission" (foundation’s macro reads downstream
HostBounds impls). Rejected — Rust macros emit at foundation’s build
time, not at downstream applications' builds; the mechanism is
incoherent with Rust’s compilation model. The honest commitment is that
impl-table caps are foundation’s per-arity emission limits, vetted by
foundation revision.
Rejected alternative 3: Raise data-shape caps without migrating.
Rejected — the magic number remains, just at a larger value. ADR-018’s
commitment is no capacity bound outside HostBounds, not "capacity
bounds outside HostBounds are fine if they’re generous."
Rejected alternative 4: Express data-shape caps through a separate
CapacityBounds substitution axis (a fifth substrate parameter
alongside HostTypes, HostBounds, AxisTuple, ResolverTuple).
Rejected — HostBounds is already the substitution axis for capacity
bounds per ADR-018; introducing a parallel axis bifurcates the bound
surface and adds an unnecessary type parameter to every substrate API
signature.
Rejected alternative 5: Runtime-configurable caps via constructor
parameters on PrismModel / pipeline::run_route. Rejected — runtime
parameterization violates TC-01 (zero-cost runtime) and ADR-006
(type-system-as-enforcement). The caps must be compile-time-resolvable,
which is what HostBounds associated constants provide.
Architecture Decisions continues → ADR-038 onward (the chapter is split across two pages to stay within GitHub's ~512 KiB per-page rendering limit).
Generated from sources at UOR-Framework.wiki. Do not edit pages directly via the GitHub web UI — edits are overwritten by the next build. See README for the authoring workflow.