H-CRSPV: Preventing Semantic Omission in Late-Bound Large Language Model Releases

H-CRSPV: Preventing Semantic Omission in Late-Bound Large Language Model Releases Weijie Miao∗ , Henry Hong-Ning Dai† , and Ming Li∗ ∗ Department of Industrial and Systems Engineering, The Hong Kong Polytechnic University, Hong Kong † Department of Computer Science, Hong Kong Baptist University, Hong Kong

arXiv:2610.05989v1 [cs.CR] 5 Oct 2026

Corresponding author: Ming Li

Abstract—Large-language-model release pipelines increasingly combine commitments, signatures, provenance records, and heterogeneous verification backends. Yet validating every submitted object does not establish that a release realizes every requirement of its registered transformation. An untrusted realization proposer may omit a required relation, propose an unauthorized evidencesharing assignment, or bind valid evidence to the wrong object. We term this verification-boundary failure Semantic Omission under Valid Evidence (SOVE). Hybrid Cryptographic Relation-based Semantic Plan Verification (H-CRSPV) is a replicated admission layer that enforces required-set completeness before release consumption. Before evidence selection, an authorized registration entity commits an authenticated authority record. The record fixes a closed, typed RelationIR specification, output identities, admissible evidence policies, and lifecycle rules; it is not an online planning role. The untrusted realization proposer later selects evidence methods and sharing assignments according to current availability. Validators independently derive the required-obligation multiset, check exact entry-occurrence coverage, validate proposal-induced evidence sharing, and bind admissible groups one-to-one to keeperresolved objects. Backend-specific verification runs only after these structural checks succeed. Evidence remains provisional until the challenge window closes and an atomic finalizer activates the release. The analysis establishes structural exactness and conditional semantic guarantees under explicit assumptions. Across 36 omission artifacts, submitted-object validation accepts all 36 because every submitted object passes its backend-specific verifier; H-CRSPV rejects all 36 while accepting all six honest releases. The prototype also validates six restricted source-to-RelationIR bindings and rejects all 60 tested mutations. In a continuous four-validator Qwen2.5-1.5B workflow, the same authority record remains fixed across three legal releases with different postregistration availability states. No re-registration is required, and all four validators agree in rejecting four targeted attacks. Perobject validity therefore does not establish complete, correctly bound, and finalized release evidence.

I. I NTRODUCTION Training a frontier-scale large language model is a substantial capital investment. Recent estimates place hardware and staff expenses for GPT-4- and Gemini-class systems in the tens of millions of dollars and project that the largest training runs could exceed one billion dollars by 2027 [1]. A growing market prices model access through hosted inference APIs, while open-weight ecosystems support local reuse and derivative releases [2]. Model weights and their derivatives are therefore economically valuable, versioned production artifacts.

That value does not stop at a base checkpoint. Lowrank adapters, sparse updates, merged checkpoints, quantized releases, and sharded model files may be produced, certified, published, and consumed by different parties. Their release pipelines increasingly combine commitments, signatures, provenance records, and fraud proofs from several evidence backends. Those mechanisms establish whether a submitted opening, equation, trace step, or signature is valid. They do not by themselves establish that the release contains every statement required by the declared transformation. This gap appears when evidence realization is selected after task registration. Consider a fixed-point merge of a base checkpoint and two LoRA adapters. The release must bind affine composition, signed ranges, rounding, adapter-to-output reindexing, and the consumer-visible output. An untrusted proposer can submit a valid KZG relation for the affine part, a valid BLS aggregate over the local relations it chose, and valid availability metadata, yet omit a required range or reindex relation or point a proof to a stale intermediate object. Every visible cryptographic check succeeds for its submitted statement, but the release has not realized the registered transformation. We term this interface failure Semantic Omission under Valid Evidence (SOVE). The vulnerable abstraction quantifies over submitted objects; the required security judgment quantifies over the registered obligation set and its concrete realization. Mixed-backend pipelines make the distinction consequential because a single release may distribute obligations across direct checks, commitment proofs, and committee-certified local relations. H-CRSPV makes this completeness boundary a replicated admission decision (Fig. 1). At registration, an authenticated authority fixes the program, output identities, required obligations, admissible backends, batching policy, and challenge policy. Evidence and availability may change later, so the proposer chooses how to realize each obligation and which entries propose to share evidence. Validators reconstruct that proposed grouping from complete keys and accept it only when the registered batching policy permits every group. Each accepted group then binds to exactly one concrete object resolved from replicated state. Native verification runs over those objects, and only a finalized release becomes active for downstream use. a) Novelty and contributions: SOVE as a verificationboundary failure. Late-bound evidence orchestration exposes

(a) Submitted-object validation Proposer-selected Γ′ omits required o∗

submitted set only

∀e ∈ Γ′ : Verify(e) = 1

ACCEPT

o∗ is outside the verifier’s quantifier

(b) H-CRSPV exact-realization admission Authenticated ρ and the same Γ′

Exact multiset comparison ρ (πobl )# Occ(M ) ̸= R

R = Req(ρ) M = Norm(Γ′ )

REJECT BEFORE BACKEND DISPATCH

Fig. 1. Submitted-object validation quantifies only over evidence in Γ and therefore cannot detect an omitted requirement. H-CRSPV independently reconstructs Req(ρ) and rejects an entry-multiset mismatch before backend dispatch.

a security-critical boundary: every submitted object may pass The boundary arises when semantics induce finite requirebackend verification while the realization still fails to cover the ments, a later actor chooses their concrete realizations, and obligation multiset derived from the registered transformation. component verifiers quantify only over submitted objects. In a SOVE formalizes this gap between per-object validity and com- PEFT/LoRA workflow, base and adapter tensors pass through plete release realization. Authority-owned exact-realization merge, sharding, and publication; late adapter-shard or backend admission. A closed, typed RelationIR profile and deterministic selection can omit a reindex, range, or rounding obligation. constructor derive a canonical, multiplicity-preserving obliga- In a quantized release, calibration produces scales and tensor tion multiset independently of proposer evidence. H-CRSPV bundles; a late manifest can omit a tensor or cross-bind its carries this requirement set through policy-checked evidence scale. In a zkML marketplace, individually valid subgraph sharing, keeper-resolved object binding, and lifecycle-gated proofs can fail to cover the registered graph [3]–[5]. admission. Replicated end-to-end enforcement. A Python, Formally, an authenticated authority ρ determines the finite Rust, and Cosmos/CometBFT prototype integrates restricted required obligation multiset PEFT/Safetensors bindings with native KZG and BLS evidence Rρ := Req(ρ) ∈ MSet(Uρ ). (1) and evaluates omission, illegal sharing, object-binding failure, dynamic late binding, lifecycle safety, replica agreement, and At release time, an untrusted proposer submits q, containing a fair completeness baselines. realization proposal, evidence payloads or authenticated object b) Key results: The restricted frontend binds six source references, and a candidate output. The abstract judgment programs and rejects 60/60 source mutations. Submitted-object evaluates q against the authenticated admission-time keeper validation accepts 36/36 loadable omission artifacts; H-CRSPV snapshot. Let SubObj(q) be the distinct set of objects resolved and three fair complete baselines reject all 36 while accepting for that release. Submitted-object validation is all six honest runs. For one provenance-bound Qwen2.5-1.5B ^ artifact under a fixed authority, all three releases finalize, and all SubmittedValidρ,ℓ (q) := Verifyobj ρ,be (σe , e) = 1. four validators reject all four attacks. H-CRSPV adds concretee∈SubObj(q) object coverage and replicated activation. (2) Our claims cover the closed R ELATION IR-C ORE V 1 profile This predicate may contain strong syntax, cryptographic, and and the evaluated declarative PEFT/Safetensors subset; backend context checks; its quantifier nevertheless ranges only over soundness, cross-commitment co-reference, and optimistic objects selected by q. finalization retain the explicit assumptions stated in Sec. III. B. Semantic Omission and the Completeness Boundary II. BACKGROUND AND P ROBLEM S TATEMENT Complete realization is independent of any backend data A. Late-Bound Evidence Pipelines structure. For each e ∈ SubObj(q), the partial function A task creator or governance registers an immutable authority Covρ,ℓ (q, e) denotes the exact obligation multiset that e is that fixes the execution context, profile and typed program, structurally authorized to realize in the current task, release, policy and catalogs, tensor and commitment descriptors, con- candidate-output, and binding context. It is undefined for crosssumer output, production setup, certifier epoch and quorum, and bound or orphan objects, unauthorized sharing, duplicate object workflow identity. Evidence may repeat those fields for binding keys, or any object with no authority-scoped role. This is a but cannot replace consensus task state. After registration, an structural association, not a semantic-truth claim. Define untrusted proposer selects realizations, batching, and witnesses. A submitted-object stack then checks the normalized relations it receives. That check is necessary, but its quantifier ranges over a proposer-selected set rather than every requirement derived from the authority; Sec. IV formalizes the distinction.

CovDefinedρ,ℓ (q) := ∀e ∈ SubObj(q) : Covρ,ℓ (q, e)↓, CompleteRealizationρ,ℓ (q) := CovDefinedρ,ℓ (q) ] ∧ Covρ,ℓ (q, e) = Rρ . e∈SubObj(q)

(3)

2

The two clauses reject missing or duplicated occurrences, unauthorized overlap, cross-context association, and objects with no registered role. They neither require one object per obligation nor assert semantic truth or finality. For an interface I, abstract SOVE acceptance and consumer safety are

authority may be registered by a release owner or governance, but its semantic adequacy remains explicitly in the TCB. Authentication of ρ establishes namespace integrity, immutability, and the identity of the candidate objects under audit. It does not assert that the candidate output equals Eval(P, X), that its manifest is complete, or that a submitted semantic relation is true. The static workflow authorization binds the I I SOVEAcceptρ,ℓ (q) := Acceptρ,ℓ (q) consumer file hash and frozen workflow scope but deliberately ∧ SubmittedValidρ,ℓ (q) does not sign release-specific realization or payload fields; ∧ ¬CompleteRealizationρ,ℓ (q), the keeper derives those fields from the unsigned proposer envelope and registered state. CertifiedLocal state jointly binds ConsumableIρ,ℓ (q, s) =⇒ SubmittedValidρ,ℓ (q) the canonical file hash, canonical stream hash, and KZG root. ∧ CompleteRealizationρ,ℓ (q). The current prototype still trusts registration/certification to (4) establish file–vector and KZG–Merkle co-reference; it does not The first predicate distinguishes SOVE from backend un- provide a cryptographic equality proof between independently soundness; the second separates evidence validity and exact supplied commitments. realization from lifecycle finality. Cov is not an added oracle. The remaining parties are artifact producers, an authorized Section IV instantiates it through proposal-induced groups that publisher, an untrusted realization proposer, provers or certifiers, pass GroupOK and the keeper-resolved ObjectBind bijection; replicated keepers, watchers, and a data-availability provider. Lemma V-A proves the correspondence. The proposer may be fully malicious. The optimistic model A faithful complete circuit, deterministic replay, or trusted also permits a semantic-signing quorum to sign a false complete planner already closes the omission gap. The missing local statement: BLS authenticates its members, exact digest, judgment appears only when an adversary selects the statement authorization, and economic responsibility, but does not itself set and the verifier has neither a trusted complete set, a recon- establish local semantic truth. We therefore make watcher comstruction procedure, nor a proof of set equality. Composition petence explicit. The premise WatcherComplete (ℓ) requires ρ preserves the validity of received objects; it cannot reveal an that, for every false CertifiedLocal statement bound to release object never requested. ℓ, an honest watcher can obtain the retained material, detect A fixed semantic inspector can close identifier-set omission the falsehood, construct and submit a valid typed challenge by comparing the authority-derived and submitted requirement by the deadline, and have it included before finalization. Final IDs. H-CRSPV carries a stronger field-level check through safety additionally assumes a sound and complete local fraudregistered-policy validation of proposer grouping, concrete proof judge and the configured CometBFT safety and liveness object binding, native evidence, workflow binding, and finaliza- threshold. tion. Section IV refines these predicates operationally; Table I The adversary may alter backend choices, group membership, summarizes the resulting ownership boundary. payload association, message-carried RelationIR copies, workflow submissions, DA tuples, and replay attempts. It may omit C. Why Late Binding Matters or overlap obligations, merge incompatible groups, reuse a valid Late binding matters when proof availability, caches, quorum object across task/release/epoch boundaries, prove an unrelated or DA state, or cost changes after registration. The authority canonical statement, withhold challenge material, or submit fixes what; the untrusted proposer chooses only how. A trusted malformed disputes. It cannot rewrite an existing authority, complete planner or deterministic replay can enforce the same break the assumed cryptographic primitives, or exceed the requirement coverage. H-CRSPV is designed for the case in consensus threshold. Bugs in semantic registration, supported which realization crosses a trust boundary and consumption lowering, canonicalization, file/vector co-reference, requirement requires a shared replicated decision. construction, exact binding, and local interpretation are explicit TCB failures rather than cryptographic error terms. III. T HREAT M ODEL AND S ECURITY G OALS A. Parties and Adversary Before any manifest is accepted, the keeper loads the task Verification Authority from consensus task state. It authenticates H(P ), H(Σ), H(C), H(D), H(I), every input/output descriptor and root mapping, the consumer-visible output identity, SRS/backend allowlists, the four-member certifier set, epoch and quorum, and the workflow layout/key. Updating any of these fields creates a new authority version; a proposer cannot create, replace, or downgrade the authority for an existing task by repeating different values in an evidence message. The

B. Structural and Semantic Safety Events Let R = Req(ρ) and, when normalization is defined, let M = Norm(Γ), G = Occ(M )/∼mat , and Oρ (E, K) be the actual typed evidence-object set reconstructed from submitted payloads and keeper state. Let η = (Γ, E, K). The registered inputs are the unique canonical tensor stream X = X(ρ) selected by the authenticated input descriptors and root mapping in ρ; neither the proposer nor an evidence object may replace

3

TABLE I R ESPONSIBILITY BOUNDARIES OF THE EVALUATED COMPLETENESS MECHANISMS . Boundary decision

Submitted-object validation

Fixed semantic inspector

H-CRSPV keeper

Required-set owner Entry-set check Grouping decision

Proposer manifest None Backend-local

Fixed policy Requirement-ID equality Not checked

Object binding Native evidence Consumability

Submitted handle Per-backend contracts External to interface

Inspector-visible input Inspector predicate External to interface

Consensus authority Exact normalized multiset Registered-policy validation of proposed quotient Keeper-resolved bijection Context-bound contracts Replicated challenge and atomic finalization

X. Define

IV. H-CRSPV D ESIGN

RealizationGap := ¬EntryCompleteρ (R, M )

A. System Overview

∨ ¬MaterializationCompleteρ (R, M, G)

H-CRSPV enforces one invariant from registration to activation: each obligation occurrence maps to one realization-entry (5) occurrence; the proposer expresses possibly singleton evidenceIf Norm(Γ) is undefined, structural acceptance is false sharing groups through complete keys; validators reconstruct and AdmissionSOVEρ (η) cannot occur; the displayed event and policy-check those groups; each admissible group binds is therefore evaluated only on the well-typed normaliza- one concrete evidence object; and only a finalized release is tion branch. Here StructureAcceptρ (Γ, E, K) means that the active. Figure 2 assigns each step to a single owner. Task creation authenticates a versioned authority ρ containing requirement-derived entry, group, and actual-object phases the transformation profile and program, output identities, reof CheckPlan accept. Let χ = (Γ, E, K, Aout ), where K quirement root, backend/SRS/DA policy, certifier set, challenge is the authenticated release-scoped keeper-resolution snapwindow W , and workflow key. The requirement constructor shot. Let Recordedρ (ℓ, χ, s) mean that release ℓ’s immutable derives R = Req(ρ) without reading the proposal. An untrusted AdmissionRecord in s binds the authority-scoped manifest, proposer later emits a finite realization multiset Γ using realization, materialization, evidence/certificate, workflow, and the evidence available at release time; complete keys in output commitments derived from exactly χ. We separate the those entries propose the concrete grouping. Every validator structural admission event from semantic release correctness: normalizes Γ, reconstructs the resulting quotient, checks each AdmissionSOVEρ (η) := StructureAcceptρ (Γ, E, K) proposed group against the registered batching relation, resolves ∧ RealizationGap, the release-scoped objects from payloads and replicated keeper state, and only then invokes native evidence interfaces. Backend FalseReleaseρ (ℓ, χ, s) := Reachρ (s) ∧ Recordedρ (ℓ, χ, s) verifiers establish facts about these resolved objects; they ∧ Consumableρ (Aout , ℓ, s) neither select obligations, choose the grouping, nor activate a ∧ ¬AuditOKρ (Γ, E, Aout ) release.
∨ Aout ̸= Eval(P, X) . We use the state names P ENDING, P ROVISIONAL, and (6) ACTIVE throughout. ACTIVE is always paired with an accepted The predicate AdmissionSOVEρ is a deterministic exact- AdmissionRecord; no consumer-facing query treats P ENDING realization invariant relative to the authenticated authority and or P ROVISIONAL as usable. structural checker TCB; it does not depend on whether a bound evidence statement is true. The predicate FalseReleaseρ is the conditional semantic event and additionally depends B. Exact-Realization Contract on backend soundness, registered co-reference, DA, watcher, The complete authenticated authority is inclusion, fraud-judge, and consensus assumptions. Moving a false claim to P ROVISIONAL is not a false release because that ρ = (ctx , Πv , P, Σ, C, D, I, Aout , state is non-consumable and remains challengeable. SRS , DA, CertSet, e, t , W, ∨ ¬ObjectBindρ (G, E, K).

cert

Workflow ).

C. Non-Goals The core result excludes legal authorship, model quality, arbitrary floating-point behavior, and unrestricted frameworkto-RelationIR equivalence. Optimistic local relations retain their stated data-availability, watcher, judge, and inclusion assumptions.

It covers the execution context, closed profile and typed DAG, policy and catalogs, tensor and commitment descriptors, consumer output, production setup, DA policy, certifier epoch and quorum, the authority-frozen window W , and workflow layout and key. Given submitted realizations Γ and evidence E,

4

(a) Exact obligation-to-object admission CONCRETE ADMISSIBLE AUTHORITY OBJECTS VALIDATOR PROPOSER GROUPS required one per occurrence proposed groups policy check EntryComplete ObjectBind one-to-one realization-entry registered-policy obligation binding quotient by κρ occurrences GroupOKρ ∼ occurrences R µ : G −→ Oρ

NATIVE VERIFY proof or certificate for bound statement

R EJECTED: entry, grouping, binding, or native-evidence failure

(b) Replicated release lifecycle P ROVISIONAL ACTIVE P ENDING h > d; guarded finalizer accepted for submitted, inactive exact admissionverified, challengeable, inactive downstream use

I NVALID challenge upheld upheld challenge h ≤ d

R EJECTED or E XPIRED

Fig. 2. H-CRSPV ownership and state flow. (a) The proposer selects a late-bound realization and proposes evidence sharing through complete keys; validators reconstruct the quotient, validate every group under registered policy, bind concrete objects, and then run native verification. (b) Only the guarded atomic finalizer changes a verified release into an active release; dashed branches show rejection, expiry, or an upheld challenge from P ENDING or P ROVISIONAL.

a component-only stack, on the defined normalization branch, computes ^ ComponentAccept(ρ, Γ, E) = Verifyρ (r, Er ), (7)

and the entry’s backend, version, and assurance profile to belong to the authority’s allowlist for o. Exact entry coverage requires one correctly bound entry occurrence for every obligation occurrence and no extras: EntryCompleteρ (R, M ) :=
ρ ∀o ∈ Uρ : mult(πobl (8) )# Occ(M ) (o) = multR (o)
ρ ∧ ∀m ∈ Occ(M ) : ExactEntryBindρ (m, πobl (m)) .

r∈Norm(Γ)

which validates received objects but does not establish equality with the authority-derived requirement set. We distinguish six objects throughout the paper. The requirement set R is the authority-derived multiset. An obligation This obligation–entry bijection rejects omission, duplicate o ∈ R is one required typed predicate. A realization entry is one coverage, unmatched entries, assurance downgrade, and identity proposed evidence assignment for one obligation occurrence. A substitution without requiring one proof object per obligation. materialization group, or shared-evidence group, is a possibly For an entry occurrence m, let κρ (m) be its complete singleton equivalence class of occurrence-tagged entries with MaterializationKey: backend/version, actual handle, task, the same complete materialization key. It is admissible only if release, candidate, artifact, output, epoch, profile, statement the registered batching relation authorizes its exact obligation schema, and registered batching class. Define m ∼mat m′ ⇐⇒ multiset to share one evidence object. A concrete evidence κρ (m) = κρ (m′ ). Because it is induced by equality, ∼mat object is the payload or certificate resolved from replicated state. is reflexive, symmetric, and transitive. By choosing the alIts statement is the canonical claim verified by the selected lowed materialization-key fields in its entries, the proposer backend. proposes a concrete evidence-sharing partition. Each validator Normalization is a partial, fail-closed operation: if parsing, deterministically reconstructs the occurrence-level quotient typing, or canonicalization fails, structural acceptance is false. G = Occ(M )/∼ . At this point the classes in G are mat Otherwise it produces the entry multiset M = Norm(Γ). Let proposed groups, not yet admissible groups. For each class Occ(M ) be its finite set of occurrence-tagged entries, so g ∈ G, define its exact obligation multiset as O = (π ρ ) g; g obl # equal entries remain distinct occurrences. Occurrence tags the common value of κ on g is MaterializationKey (g). Then ρ ρ are assigned by the canonical entry encoding and a duplicate MaterializationCompleteρ (R, M, G) := ordinal after canonical sorting; they are therefore deterministic and cannot be chosen by the proposer. Let Uρ be the finite typed G = Occ(M )/∼mat universe of canonical obligation identities generated by the (9) ∧ OccPart(Occ(M ), G) ] ^ registered DAG, block partition, profile, and admissible relation ρ ∧ Og = R ∧ GroupOKρ (g). families under ρ. The projection πobl : Occ(M ) → Uρ removes g∈G g∈G materialization fields and returns the obligation identity encoded ρ by an entry. For an occurrence subset Q ⊆ Occ(M ), (πobl )# Q Here OccPart states that every entry occurrence belongs denotes its pushforward multiset. Let EntryBindρ (m) be the to exactly one class. A proposed group becomes admissible canonical semantic-binding tuple encoded by m. We define only when GroupOKρ (g) holds. That predicate evaluates the ExactEntryBindρ (m, o) to require EntryBindρ (m) = Bindρ (o) complete obligation multiset Og under the authority-registered

5

batching relation and authorizes every occurrence in g to share the one materialization named by their common key. It does not bind or verify the evidence object. Unknown, mixedassurance, or otherwise incompatible combinations evaluate to false. Singleton classes are valid proposed groups and require the same policy check. Thus batching can reduce object count only through a typed, complete, occurrence-disjoint partition; repeated obligation identities retain their multiplicity. The resolver constructs Oρ (E, K) from all typed payloads supplied or referenced by the release and all authenticated release-scoped certificates; any malformed, duplicate-key, or untyped object causes resolution to fail rather than disappearing from this set. For each group, its binding context is GroupBindρ (g) := Task, Release, Candidate, Artifact, Output, Epoch, Profile, Backend, SRS, DA,
MaterializationKeyρ (g) .

C. Lifecycle and Consumability Candidate submission creates a P ENDING release under a unique (task , release) identity. Admission performs authority lookup, requirement reconstruction, entry exactness, quotient reconstruction, GroupOK, object binding, workflow binding, canonical-statement derivation, and native verification in that order. Success creates only a non-consumable P ROVISIONAL record. Certificate registration and evidence admission must each leave the authority-defined window W before the challenge deadline d: max(hcert , hverify ) + W ≤ d. A valid typed challenge through d moves the release to I N VALID; deterministically malformed evidence moves P ENDING to R EJECTED; and incomplete certificate-bearing admission expires after d. When the deadline has elapsed, every group is eligible, and no dispute remains, the finalizer atomically writes ACTIVE, the accepted AdmissionRecord, finalized certificate states, and bond settlement. Replay and immutability guards prevent duplicate settlement or terminal-state mutation. A replacement is a new release and cannot shorten the prior challenge window.

(10)

After every proposed group is admissible, the concrete-object contract requires a bijection and two independent equalities: ObjectBindρ (G, E, K) := ∼

∃µ : G − → Oρ (E, K) s.t.

D. Requirement Construction and RelationIR The closed R ELATION IR-C ORE V 1 profile is a finite typed DAG. Its versioned profile is

∀g ∈ G : (11) Statement(µ(g)) = Canonρ (Og , GroupBindρ (g)) ∧ ObjectKeyρ (µ(g)) = MaterializationKeyρ (g).

Πv = (OpSet, TypeRules, SemRules,

ReqRules, CanonRules, EvidenceRules). The first equality binds semantic content; the second binds the concrete object that carries it. Totality assigns one object to The profile admits three node families: n ::= AffineCombine((ai , di )i ) every group, injectivity forbids cross-group object reuse, and surjectivity forbids resolved orphan objects. Together the checks | LocalMap(g, d) | Reindex(π, d), reject missing payloads, proof swaps, unrelated statements, g ::= DropRescaleMask | ElementwiseScale stale handles, and cross-task, cross-release, cross-candidate, | RoundDiv | QuantizeUniform. cross-epoch, or cross-output reuse. The evaluated profile illustrates the distinction. Its 320 Certi- Tensor descriptors bind shape, layout, fixed-point scale, signed fiedLocal entry occurrences carry one complete materialization width, range, field, domain, and commitment layout. RangeOK key and therefore form one proposed quotient class. GroupOK is derived by the checker, and Reindex covers chunk-aligned admits that class only if the registered policy permits its permutations. Dependencies must point to earlier typed nodes, exact Og to share a certificate. The bijection µ then binds maps must be total, and every output must be reachable. The the class to one keeper-resolved BLS certificate whose relation- production profile excludes unknown operators and DENSITY set digest commits to the canonical statement for exactly the sampling. For example, the running adapter merge contains dropcorresponding Og . BLS verification authenticates the 3-of-4 quorum statement; semantic truth still depends on the registered rescale, affine, and rounding nodes: data-availability, watcher, challenge, judge, and finalization Zi = DropRescale(∆i ; mi , pi ), assumptions. N = Sw X0 + aA ZA + aB ZB , Let τbρ,Γ,E,Aout be the candidate typed trace determined by Y = RoundDiv(N, Sw ). authenticated registration and admitted evidence. For o ∈ R, the judgment τbρ,Γ,E,Aout |= o means that the exact operational The constructor emits obligations for the affine relation, signed predicate bound by o holds. We define range, rounding rule, registered reindexing, dependencies, and consumer output. Writing n1 , . . . , nm for topological order, AuditOKρ (Γ, E, Aout ) := ∀o ∈ R, τbρ,Γ,E,Aout |= o. m ] CheckPlan establishes that every obligation has a legal, objectNρ = NodeReq(nj , ρ), (12) bound realization. VerifyEvidence establishes predicate truth j=1 only under the selected backend and its stated assumptions. Req(ρ) = CanonSort(Nρ ⊎ OutputReq(ρ)).

6

Construction depends only on the registered authority, not on Γ. Every entry is bound to a canonical semantic identity

TABLE II G UARANTEE LADDER : CONCLUSIONS AND ADDITIONAL ASSUMPTIONS . Layer

Conclusion

Structural

No omission, overlap, Authority; constructor; normalizer; orphan, or cross-binding grouper; resolver Consumable output Structural layer; backend satisfies the registered adequacy; co-reference; DA; program watcher; judge; consensus Output satisfies the Semantic layer; trusted supported source checked-frontend correspondence semantics

Bindρ (o) = (H(ρ), nodeId , rel , prim, (inCommit, inBlock )i , outCommit, outBlock , H(params),

Finalized semantic

(13)

Source-level TCB transfer

H(deps), interpV ). H(ρ) covers the profile, program, descriptors, root mapping, policy, and consumer-visible output. Block coordinates come from verified registered descriptors rather than witness-selected fields. Consequently, a valid object for one program, parameter set, dependency, coordinate range, commitment domain, or interpreter cannot satisfy another obligation.

Additional assumptions

Occ(M )/∼mat . The fixed inspector and the keeper acceptance predicates at a committed consensus state s are InspectorOKρ (Γ) := ReqIds(Req(ρ)) = ReqIds(Norm(Γ)), HAcceptρ (ℓ, χ, s) := Reachρ (s) ∧ Recordedρ (ℓ, χ, s) ∧ EntryCompleteρ (R, M ) ∧ MaterializationCompleteρ (R, M, G)

E. Restricted Frontend and Native Backends

∧ ObjectBindρ (G, E, K)

For the evaluated declarative PEFT/Safetensors LoRA subset, a restricted frontend compiles source metadata and tensor headers into a typed program and a lowering certificate:

∧ WorkflowOKρ (ℓ, Γ, Aout , s) ∧ EvidenceOKρ (ℓ, G, E, K, s) ∧ FinalAcceptρ (ℓ, s).

Compile(S) → (P, πlower ), CheckLower(H(S), P, πlower ) = 1.

ReqIds returns a multiplicity-preserving identifier multiset; the Recordedρ predicate above prevents substituting a different manifest, object set, keeper state, or output after admission. InspectorOK compares identifiers; it neither proves fieldlevel entry binding nor owns grouping, object resolution, or consumability. HAccept composes those checks with the finalacceptance predicate formalized in Sec. V.

(14)

The certificate binds the base revision, immutable tensor hashes, rank, alpha, orientation, target modules, shapes, dtypes, library versions, consumer port, and output map. CheckLower reparses these fields before realization and compares the R ELATION IRC ORE V 1 reference output with the registered declarative source V. S ECURITY A NALYSIS semantics. The security argument has three layers (Table II). Each layer The evidence layer has mandatory deterministic bindings, adds assumptions rather than silently promoting a structural production KZG for the global affine statement, and direct set check into an end-to-end semantic claim. The closed or BLS-certified local relations. The keeper derives every R ELATION IR-C ORE V 1 specification provides the grammar, statement from authority-owned RelationIR and accepts only type and obligation rules, canonical identities, and backend registered backend, SRS, and DA profiles. A CertifiedLocal admissibility policy used below. aggregate proves that three distinct authorized members signed the exact group statement; semantic truth additionally relies A. Coverage, Binding, and Finalization on retained challenge data, watcher completeness, and the Fix an authority version ρ. Its replicated lifecycle is the typed fraud-proof judge. The mixed KZG/Merkle path binds labeled transition system both roots through one authenticated registrar transcript. This registrar supplies the explicit co-reference premise used by Tρ = (Sρ , s0ρ , ∆ρ ), ∆ρ ⊆ Sρ × Aρ × Sρ . Proposition 1. a The checker performs Eqs. (8)– (11) before expensive We write u − →ρ v for (u, a, v) ∈ ∆ρ and Reachρ (s) iff backend dispatch. Unknown backend labels, malformed tran- there exist k ≥ 0, states s0 = s0ρ , . . . , sk = s, and actions ai scripts, policy downgrades, unrelated statements, and DA/SRS a0 , . . . , ak−1 with si − →ρ si+1 for every i < k. We write mismatch reject. Here EvidenceOKρ means that each keeper- u ⪯ρ s when a (possibly empty) ∆ρ path leads from u to s. resolved object is accepted by its registered native interface, Each accepted transaction is one action in the CometBFT total while WorkflowOKρ binds the candidate and consumer output order, including transactions within the same block. to the registered release workflow. The initial state contains no active release or accepted For comparison, on the defined normalization branch, let AdmissionRecord. Only admission may create P ROVISIONAL; χ = (Γ, E, K, Aout ), R = Req(ρ), M = Norm(Γ), and G = only the finalizer may create ACTIVE with an accepted record.

7

No transition admits a challenge from terminal ACTIVE or reopens its dispute counter. The lifecycle predicates deliberately separate exact admission, eligibility to finalize, and final acceptance. Let ExactAdmissionρ (ℓ, s) abbreviate the conjunction of Eqs. (8)– (11) with the explicit WorkflowOK and EvidenceOK arguments under release ℓ’s registered context. Admission stores the canonical inputs, derived roots, group set, object keys, check results, and output identity in one immutable AdmissionRecord; later states read this record rather than re-evaluating mutable external data. Let Gℓ be the immutable admitted group set. Then

Only the atomic finalizer may establish Eq. (16), and it may do so only when the guard in Eq. (15) holds. Thus P ROVISIONAL is never consumable. Determinism Lemma (Replica-consistent reconstruction). For a fixed authority snapshot ρ, canonical proposal bytes, evidence bytes, and release-scoped keeper snapshot, every correct replica computes the same R, M , G, resolved object set, and structural decision. Proof sketch. Requirement construction and normalization are total deterministic functions on their accepting domains; all sets are ordered by canonical encodings; occurrence tags use canonical order and duplicate ordinals; equality of the complete materialization key induces a unique quotient; and the resolver reads the same authenticated state snapshot. No consensus decision depends on host map iteration or arrival order. The complete argument appears in Appendix F. □ Lemma 1 (Exact Obligation Coverage). For authenticated ρ, let R = Req(ρ) and M = Norm(Γ). If the entry phase of CheckPlan accepts, then EntryCompleteρ (R, M ) holds. Proof sketch. The checker derives R independently of Γ and enforces multiplicity equality plus exact field binding for every entry. Appendix F gives the accepting-path argument. □ Lemma 2 (Materialization Binding). If the materialization phase accepts after Lemma 1, then materialization completeness (Eq. (9)) and object binding (Eq. (11)) both hold. Proof sketch. Complete keys in the entries induce the proposer’s unique proposed quotient. Each validator reconstructs that quotient, checks its disjoint complete union, applies the registered batching relation, and resolves exactly one contextand statement-bound object per admissible group. Detailed branch coverage appears in Appendix F. □ Bridge Lemma (Operational–abstract correspondence). Let OpRepρ,ℓ (q, K) = (Γ, E, Aout ) mean that q is the release submission for (ρ, ℓ), contains realization proposal Γ, binds candidate output Aout , and selects the supplied or authenticatedreference inputs E when evaluated against authenticated keeper snapshot K. If EntryComplete, MaterializationComplete, and ObjectBind hold for this same operational instance, the unique bijection µ in Eq. (11) instantiates

FinalizeGuardρ (ℓ, s) := States (ℓ) = PROVISIONAL ∧ ExactAdmissionρ (ℓ, s) ∧ WindowBoundρ (W, ℓ, s) ∧ h(s) > dℓ

(15)

∧ AllEligibleρ (Gℓ , ℓ, s) ∧ NoDisputeρ (ℓ, s), NoDisputeρ (ℓ, s) ⇐⇒ OpenDisputeCounts (ℓ) = 0. Every predicate is evaluated under the same registered task, release, candidate, artifact, output, epoch, profile, backend, SRS, DA, and challenge context. Here WindowBound requires both certificate registration and evidence verification to leave the authority-frozen W blocks before the deadline. A valid challenge action is enabled while h(s) ≤ dℓ and moves P ENDING or P ROVISIONAL to terminal I NVALID; a finalize action is enabled only when h(s) > dℓ . Thus a challenge included at h = dℓ is ordered and applied before any later finalize(ℓ) enabled finalizer. When Eq. (15) holds, s −−−−−→ρ s′ atomically establishes States′ (ℓ) = ACTIVE, AdmissionRecords′ (ℓ) = ACCEPTED, for every c ∈ Certs(ℓ) : CertStates′ (c) = FINALIZED, BondStates′ (c) = AVAILABLE.

SubObj(q) := Oρ (E, K),

No other action may establish either active or accepted, and terminal release, certificate, and settlement fields are immutable. Define the historical finalization predicate and current final acceptance as follows; for compactness, AdmRecs (ℓ) abbreviates AdmissionRecords (ℓ).

Covρ,ℓ (q, µ(g)) := Og

(g ∈ G),

(17)

and OpRepρ,ℓ (q, K) = (Γ, E, Aout ) ∧ EntryComplete ∧ MaterializationComplete ∧ ObjectBind =⇒ CompleteRealizationρ,ℓ (q).

finalize(ℓ)

Finalizedρ (ℓ, s) := ∃u, v : u −−−−−→ρ v ∧ Reachρ (u) ∧ v ⪯ρ s ∧ AdmRecv (ℓ) = ACCEPTED,

(18)

Proof sketch. Surjectivity of µ defines coverage for every resolved submitted object; injectivity and unique complete object keys make coverage single-valued. Exact entry binding, GroupOK, and the statement, context, and object-key equalities make the coverage authority-scoped. Reindexing the U disjoint multiset union in Eq. (9) through µ gives e∈SubObj(q) Covρ,ℓ (q, e) = Rρ , proving both clauses of Eq. (3). Appendix F expands the resolver branches. □

FinalAcceptρ (ℓ, s) := States (ℓ) = ACTIVE ∧ AdmRecs (ℓ) = ACCEPTED, Consumableρ (Aout , ℓ, s) := ReleaseOutputs (ℓ) = Aout ∧ FinalAcceptρ (ℓ, s). (16)

8

Theorem 1 (Exact-realization invariant). Let Backend lifting is deliberately typed: StructOKρ (Γ, E, K) := EntryCompleteρ (R, M ) ∧ Verifydirect/KZG (µ(g)) = 1 =⇒ ∀o ∈ Og : τbρ,Γ,E,Aout |= o, ρ MaterializationCompleteρ (R, M, G) ∧ ObjectBindρ (G, E, K). CL-BLS Verifyρ (µ(g)) = 1 =⇒ QuorumSignedρ (Stmt(g)). Relative to an authenticated authority and faithful execution (22) of the registered requirement constructor, normalizer, quotient The second line authenticates an exact statement; it does not reconstruction, GroupOK logic, canonical encoder, and typed alone establish that statement’s semantic truth. For Certifiedobject resolver, Local groups, truth enters the composition argument only StructureAcceptρ (Γ, E, K) =⇒ StructOKρ (Γ, E, K). (19) through finalization together with DA, WatcherCompleteρ (ℓ), and fraud-judge assumptions. The registered semantic statement By definition, StructOKρ ⇐⇒ ¬RealizationGap on the well- for such a group is the conjunction of its exact obligations, typed normalization branch. Consequently, for the same opera- Stmt(g) ≡ V o∈Og o, encoded with the binding context in tional instance, Eq. (10). Proposition 1 (Finalized semantic composition). Let P OpRepρ,ℓ (q, K) = (Γ, E, Aout ) be a well-typed closed R ELATION IR-C ORE V 1 DAG with ∧ StructureAcceptρ (Γ, E, K) (20) registered inputs X, let χ = (Γ, E, K, Aout ), and suppose the =⇒ CompleteRealizationρ,ℓ (q), immutable AdmissionRecord for ℓ binds exactly χ. Assume so both AdmissionSOVEρ (η) and the abstract authentic and adequate task authority; canonical decoding and I SOVEAcceptρ,ℓ (q) event are false for H-CRSPV under registered file/vector co-reference; Theorem 1 and Lemma 3; backend soundness; a valid registered workflow; per-node the structural assumptions in Table II. adequacy; challenge data available through the deadline; Proof sketch. Lemma 1 establishes the obligation–entry WatcherCompleteρ (ℓ); a sound and complete fraud-proof bijection; Lemma 2 establishes registered-policy acceptance of judge; and the configured CometBFT threshold. If Reachρ (s), the proposal-induced partition and the concrete-object bijection Recordedρ (ℓ, χ, s), and Consumableρ (Aout , ℓ, s) hold, then over the same authority snapshot. Their conjunction is exactly Reachρ (s) ∧ Recordedρ (ℓ, χ, s) StructOKρ , equivalently the negation of Eq. (5); the Bridge Lemma then yields Eq. (20). □ ∧ Consumableρ (Aout , ℓ, s) (23) Lemma 3 (Reachable-state finalization safety). For every =⇒ AuditOKρ (Γ, E, Aout ) release ℓ, state s, and registered output Aout , ∧ Aout = Eval(P, X). Reachρ (s) Proof sketch. The record premise fixes the same χ throughout ∧ Consumableρ (Aout , ℓ, s) the argument, and Lemma 3 supplies exact admission for =⇒ Finalizedρ (ℓ, s) (21) that record. Lemma 1 supplies every exact obligation in its manifest; Lemma 2 validates the proposed groups and ∧ ExactAdmissionρ (ℓ, s) binds each admissible group to exactly one keeper-resolved ∧ NoDisputeρ (ℓ, s). object. Equation (22) lifts direct/KZG object verification to The witnessing finalizer ran after dℓ , found every group eligible, obligation truth and BLS verification only to an authenticated and atomically finalized certificates and settled each bond quorum statement. Per-node adequacy and topological induction establish every intermediate and output block. Output binding exactly once. Proof sketch. Induct on the path witnessing Reachρ (s). The identifies the result with Aout . For an optimistic group, suppose initial state is non-consumable. Admission, rejection, challenge, its conjunction were false. Watcher completeness supplies a expiry, and replay transitions cannot establish active-plus- timely included typed challenge, judge completeness upholds it, accepted. The only inductive case that can establish it is an and ∆ρ moves the release to terminal I NVALID, contradicting enabled atomic finalizer; its guard supplies every conjunct, Lemma 3 and consumability. This supplies the remaining and terminal immutability preserves them. The full transition semantic step. The result is a conditional pen-and-paper argument appears in Appendix F. □ composition argument, not mechanized verification of its TCB. □ B. Conditional Composition Guarantee Define FrontendRelρ (S, P, πlower ) as the trusted correspondence invariant that the supported source parser, tensor and The structural and lifecycle lemmas do not independently parameter mapping, consumer port, and output map are prove external source semantics or backend soundness. For field-complete and that the supported source evaluator is each registered primitive, we assume the per-node adequacy observationally equivalent to Eval(P, ·) at the bound output. ∗ condition. Let Vj be the admitted value at node nj and Vj its CheckLower checks the registered hashes and fields; it does reference value in topological order. Writing Pred(j) for its not prove this invariant for arbitrary executable code. registered predecessors, adequacy is the typed implication Claim 1 (Scoped frontend-TCB transfer). Let S belong to

the supported declarative PEFT/Safetensors subset. If Check∀i ∈ Pred(j) : Vi = Vi∗ ∧ ∀o ∈ NodeReq(nj , ρ) : τb |= o Lower accepts (H(S), P, πlower ), FrontendRelρ holds, and the =⇒ Vj = Semρ (nj , (Vi∗ )i∈Pred(j) ).

9

premises of Proposition 1 hold, then the accepted output equals the registered source semantics. This is a transfer through an explicit frontend TCB premise, not an independently proved source-level theorem, and it does not extend to arbitrary Python execution.

10

TABLE III N ORMATIVE RELEASE TRANSITIONS . G UARDS ARE EVALUATED FROM REPLICATED STATE ; THE LISTED RELEASE , CERTIFICATE , AND BOND EFFECTS COMMIT ATOMICALLY. Transition

Guard or rejected action

Atomic release/certificate/bond effect

P ENDING→P ROVISIONAL

ExactAdmissionρ (ℓ, s) ∧ h ≤ dℓ

No

P ENDING→R EJECTED

Complete deterministic evidence establishes a registered invalid state

Store immutable exact-admission record; certificates remain provisional and bonds locked Write rejected record; release and configured settlement become terminal

Revoke affected certificates and slash configured bonds exactly once Malformed/invalid typed challenge or unauthorized generic Reject transaction; no release, certificate, or bond dispute mutation

No

P ENDING/P ROVISIONAL →I NVALID s→s

Valid typed fraud proof and h ≤ dℓ

Cert.-bearing P ENDING →E XPIRED

h > dℓ with no complete admission or open dispute

P ROVISIONAL→ACTIVE

FinalizeGuardρ (ℓ, s)

Terminal → same terminal

Replay or illegal terminal mutation

C. SOVE Rejection Corollary 1 (No admitted structural omission). Under the structural premises of Theorem 1 and the OpRep relation for the same admission instance, StructureAccept implies CompleteRealization by Eq. (20). Any missing, duplicated, overlapping, cross-bound, non-admissibly grouped, reused, or orphaned obligation/object therefore prevents structural acceptance regardless of the validity of submitted objects. Separately, Lemma 3 prevents a provisional, disputed, or otherwise unfinalized release from satisfying Eq. (16). Neither conclusion requires the semantic premises of Proposition 1. D. Submitted-Object Interface Separation Observation 1 (Submitted-object non-implication). Component acceptance over only submitted objects does not imply manifest completeness unless the verifier also has a trusted complete requirement set, an equivalent reconstruction mechanism, or a proof of statement-set equality. Proof sketch. Remove a critical obligation o∗ and provide valid evidence for every remaining entry. The submitted-object view observes only valid objects; a verifier that reconstructs the complete requirement set rejects the missing o∗ . E. Residual Risk Acceptance remains conditional on distinct trust domains: task-authority adequacy and immutability, source lowering for the supported subset, canonicalization, file/vector co-reference, realization-to-evidence association, cryptographic soundness, the consensus threshold, data availability, watcher completeness, and the local-interpreter TCB. We do not assign a numerical union bound because deterministic implementation bugs and deployment-liveness failures lack a common probability experiment in the present model. VI. P ROTOTYPE AND E VALUATION The implementation has one versioned admission schema with several evidence realizations. The off-chain path consists

11

Mark certificate E XPIRED U NUSED; make bond available Atomically write accepted record, finalize all certificates, and release bonds once Reject or return the recorded result; never repeat settlement

Consumable

No

Unchanged

No Yes Unchanged

of the R ELATION IR-C ORE V 1 profile, a restricted PEFT 0.18.1/Safetensors 0.8.0 frontend [6], [7], an exact-binding manifest checker, a registrar-dependent co-reference gate, a Rust/Python heterogeneous dispatcher, commitment-bound local evidence, and consumer-output checks. The Cosmos SDK v0.50.5 keeper [8], replicated by CometBFT v0.38.6 [9], [10], loads an immutable task Verification Authority, verifies typed production-KZG and task-owned BLS evidence, checks an unsigned release envelope against a reusable task-registered static workflow authorization, and enforces the release lifecycle. A. Prototype and Experimental Setup The checker computes requirements before reading evidence verdicts. It rejects malformed or ambiguous identities, multiplicity mismatch, missing or unexpected entries, incorrect dependencies, stale policy versions, backend downgrades, incomplete output binding, policy-invalid proposer grouping, and concrete-object mismatch. The Go keeper loads authority from consensus state, derives and sorts obligations, reconstructs the quotient induced by the entries’ complete typed materialization keys, evaluates GroupOK, and reconstructs objects from mandatory/KZG/local payloads and CertifiedLocal state. A hash string alone can neither create a payload nor authorize batching. For certificate-bearing terminal paths, an active release has an accepted record, a finalized certificate, and an available bond. An invalid release has a revoked certificate and slashed bond; an expired release marks its unused certificate expired and returns the bond. A malformed fraud proof changes none of these states. Only an uncertified and unbonded pending reservation may be cancelled, replaced, or expired. The consumer API calls one predicate equivalent to Eq. (16); queries do not expose provisional artifacts as accepted. The legacy non-authority generic-dispute path permits at most one open dispute and only the frozen governance authority may resolve it; terminal state is immutable. Transaction handlers emit deterministic protocol

facts only. Host wall time, CPU time, and memory are recorded by the experiment harness rather than consensus events.

interpreter work:

size/capability → manifest binding The trusted path contains the parser, type checker, require→ registry/domain → decode/subgroup ment constructor, canonicalizer, object resolver and interpreters; → crypto → local judge → state write. lowering, authority, and the current co-reference registrar are also trusted. Any mechanism deciding what the constructor This ordering matters because the checker itself becomes must require therefore remains in the TCB. H-CRSPV bounds an attack surface once adversaries can submit manifests and it with a closed versioned language, hash-pinned authority, fail- challenges. The frozen campaign reports observable lifecycle closed operators, replicated execution, and differential oracles; and query results; rejection-path backend-call and state-write it does not choose late realizations or require an online semantic counters remain null and unobservable. Sustained throughput, planner. All planning and evidence-production roles remain external-network finality, and external-DA retention remain untrusted. Cryptography, BFT, DA, and watcher liveness are outside this paper’s claim. separate assumptions; testing reduces but cannot remove the We evaluate six questions. RQ1 tests the obligation–entry– TCB. After this interface is fixed, late actors cannot change group–object contract. RQ2 tests lifecycle safety. RQ3 asks obligations, objects, or consumability. whether one authority can support post-registration evidence 1) KZG and registered setup: The bundled Rust KZG changes without a trusted online planner. RQ4 tests source worker [11] implements chunked vector commitments, open- binding and compares fair completeness baselines. RQ5 follows ings, batch verification, and global affine checks. The keeper one artifact through replicated admission. RQ6 reports cost and permits only the registered production backend and SRS profile, deployment boundaries. Appendix H contains the supporting both loaded from consensus state. Transaction execution does mutation, cross-language, trace, and local-judge campaigns. not read node-local files or environment variables. The affine B. RQ1: Entry–Group–Object Exactness statement is reconstructed from authority-owned RelationIR; a The fixed PEFT instance contains 345 required obligation valid proof for another relation therefore fails the canonicalstatement gate. The co-reference registrar remains a TCB and occurrences, and its honest proposal contains the same number of realization entry occurrences. Those entries induce 26 is not presented as a KZG–Merkle equality proof. groups—one 320-entry group and 25 singleton groups—each 2) Certified local relations: The BLS quorum [12] of which satisfies GroupOK; ObjectBind then maps the signs a canonical digest over domain/schema, admissible groups one-to-one to 26 concrete objects. The large chain/task/release/candidate, publisher/submitter, artifact group shares one CertifiedLocal 3-of-4 aggregate certificate, and output digests and references, materialization-group so its entries are neither independent proofs nor independent relation set, DA tuple, certifier set/epoch/bitmap, deadline, objects. This is the frozen chain required occurrences → minimum remaining window W , and bond records. The keeper proposal entries → proposal-induced groups → GroupOKchecks three distinct members of four, bitmap consistency, admissible groups → keeper-resolved objects. Directed controls epoch, PoP state, and aggregate pairing. This authenticates distinguish three failure owners: incompatible sharing fails responsibility for the exact local statement; semantic truth GroupOK; missing, reused, orphan, stale, or cross-bound remains optimistic. The frozen certificate’s statement covers objects fail ObjectBind; and invalid proofs or certificates fail exactly 320 local obligations and remains bond-locked through native verification. Entry omissions, duplicates, and unmatched provisional/disputed state. A valid fraud proof rejects and identities fail the earlier exact-entry gate. Every legal and slashes; an unchallenged exact certificate may be finalized after adversarial row produces the expected decision; Appendix G the deadline. The final negative report separates malformed preserves the campaign counts and command-level evidence. encoding, bad PoP, stale epoch, wrong bitmap, and a valid We additionally construct six incorrect endpoints with fresh, aggregate over an alternate legal digest (5/5 alternate digests valid evidence for every relation that remains declared. The self-verify and fail the keeper digest). submitted-object stack and H-CRSPV receive identical artifacts and native evidence. The former accepts 6/6; H-CRSPV 3) Registered data availability: The authority freezes reconstructs the requirement set and rejects 6/6 before backend a versioned DA profile. The current loopback profile is dispatch (Table IV). Every row changes the deterministic output an implementation control, not external DA: it requires at the attacked coordinates. DACommitment = ArtifactDigest and DALocation = CanonicalCIDOrArtifactRef. Candidate, certificate, static work- C. RQ2: Lifecycle and Finalization Safety flow authorization, release envelope, provisional record, final The lifecycle matrix checks admission to P ROVISIONAL, record, and BLS digest bind the same tuple. Unknown versions, consumer rejection before finalization, deadline ordering, valid short retention, commitment or location swaps, and crossand malformed fraud proofs, replay, bond timing, terminal release tuple reuse fail closed. immutability, and idempotence. Each row compares release, 4) Cheap-check ordering: Both handlers are structured to certificate, bond, AdmissionRecord, consumability, and applireject inexpensive malformed cases before cryptographic or cation state across four validators. Every control reaches its

12

TABLE IV O MISSION ATTACKS WITH OTHERWISE VALID SUBMITTED EVIDENCE . A LL H-CRSPV ROWS REJECT DURING EXACT- REALIZATION ADMISSION .

Omitted or stale relation RangeOK RoundDiv Reindex Stale predecessor DARE LocalMap Output artifact bind

TABLE VI FAIR - BASELINE DECISIONS AND LOCAL ADMISSION - ONLY LATENCY.

Submitted Coordinates objects H-CRSPV 1 2 8 1 1 1

Accept Accept Accept Accept Accept Accept

Reject Reject Reject Reject Reject Reject

Attacks Honest Latency (ms) rejected accepted mean/P95

Acceptor

Completeness owner

Submitted-object stack H-CRSPV Trusted canonical Full replay Fixed semantic inspector

Submitted objects

0/36

6/6

0.30/0.43

Replicated exact set Online planner Deterministic executor Fixed policy

36/36 36/36 36/36 36/36

6/6 6/6 6/6 6/6

6.32/7.29 5.00/5.69 8.87/9.27 0.79/1.14

E. RQ4: Source Binding and Fair Baselines

TABLE V L IFECYCLE CONTROLS AND FOUR - VALIDATOR OUTCOMES .

The restricted frontend processes two independently generated adapter pairs under three fusion seeds. It binds all six Control Release result Safety check source instances to their consumer outputs and rejects 60/60 Exact evidence Provisional No accepted record; not mutations of rank, alpha, orientation, target module, tensor key, consumable dtype, consumer, output mapping, or base identity. Valid timely Invalid Certificate revoked; bond settled challenge once The attack harness creates six omission families for each Malformed challenge Unchanged Rejected transaction; no honest run, yielding 36 loadable Safetensors artifacts. PEFT advancement loads all artifacts, and the submitted-object stack accepts Bad evidence Rejected One terminal settlement 36/36 because every supplied object is valid. H-CRSPV rejects Incomplete at Expired Audit retained; bond available deadline 36/36 by reconstructing the omitted obligation. The trusted No dispute at Active W preserved; atomic final record canonical planner, deterministic replay, and fixed semantic deadline inspector also reject 36/36 while all four complete paths Replay or mutation Unchanged No rollback or duplicate settlement accept 6/6 honest releases. Thus requirement completeness is achievable by several fair baselines. H-CRSPV’s additional specified lifecycle outcome, and no exact admission is counted responsibility is late-bound actual-object resolution and the as final acceptance. The frozen counts remain in Appendix G. replicated provisional-to-consumable lifecycle. For comparability, Table VI reports only local admission work under single-process Python 3.10.9 with resident inputs: D. RQ3: Dynamic Late Binding 30 repetitions for each of six honest runs (n = 180). The With one unchanged protocol authority, 3/3 legal partitions trusted-planner row includes canonical plan construction and accept, 10/10 malformed partitions reject, and all 13 outcomes replay includes deterministic execution. Evidence materialization and verification, retrieval/cache state, network transfer, and converge across four validators. four-validator consensus are excluded from every row. One continuous run uses a provenance-bound Qwen2.5-1.5B On this small one-shot workload, full replay is faster end to artifact [13], four validators, and 6 loopback HTTP provider end; evidence materialization costs and model-output effects are processes on one host. At t0 the authority fixes the program, reported separately in Appendix B. H-CRSPV targets settings 240 local obligations, backend policy, and W = 10; only r1 where validators cannot all retrieve replay inputs, evidence is exists. The r2 bundle appears after its candidate commits and reused, or specialized evidence backends and a shared release is withdrawn after finalization (HTTP 404 without changing lifecycle are already required. terminal state); r3 appears only afterward. No future member list, object ID, root, or nonce exists at t0 . All 3 releases F. RQ5: Replicated Artifact Admission become consumable; omission, overlap, stale, and cross-binding One continuous chain binds a prerelease layout, static controls reject; and all 7 outcomes agree across replicas. authorization, and one immutable Safetensors digest through A fixed concrete plan finds complete requirements only for lowering, PEFT consumption, admission, and the final record. r1 . The trusted online planner and fixed semantic inspector The chain reproduces the same entry–group–object mapping as find complete requirements for r1 /r2 /r3 , while H-CRSPV RQ1 and uses a real 3-of-4 BLS aggregate generated by four additionally binds actual objects and finalizes all three releases centrally held test keys. Across the fixed and dynamic controls, (Table VII). The inspector establishes that requirement com- every committed decision and application-state hash agrees pleteness need not depend on an online trusted planner. Only the on four validators. Detailed case inventories, signer-isolation H-CRSPV row owns the replicated transition to consumability. receipts, and state-transition counts are retained in Appendix G. Across those releases, H-CRSPV commits 11 aggregate 3-of-4 BLS certificates, accounting for 33 signer participations; the G. RQ6: Cost and Deployment Boundary artifact does not claim 33 separately retained partial-signature Replay is simpler and faster for small available inputs. At the receipts. single fresh-cache r2 operating point, four validators retrieve

13

12,396,243,912 replay bytes versus 10,146,896 H-CRSPV bytes (1,221.68×), or 1,172.88× after provider-plane traffic. A warm observation records 0/506,996 incremental bytes. These are byte measurements, not latency or same-assurance comparisons; the size-matched CPU study in Appendix A is a separate negative result. The anonymous artifact binds every headline value to machine-readable results and includes sources, localnet scripts, public projections, and a detached clean-room verifier. Supporting test totals and claim-to-evidence mappings appear in Appendices H and G. VII. D ISCUSSION AND L IMITATIONS H-CRSPV targets late-bound releases whose evidence objects are resolved in replicated state and whose consumers need ordered activation; replay remains preferable when complete inputs are cheap. A fixed inspector closes identifier-set omission but does not own grouping, object binding, or activation. Claims remain conditional on Table II; Appendix D states the full TCB and deployment limits. VIII. R ELATED W ORK Complete mediation and plan-to-execution systems motivate full event and plan checking [14]–[18]; provenance, transparency, verifiable-computation, and translation systems authenticate workflows or supplied realizations [4], [19]–[26]; model-composition and supply-chain work defines the artifact substrate [3], [27]–[30]. H-CRSPV instead owns requiredset construction, proposer-grouping policy, object resolution, and replicated activation (Table I); Appendix E gives the full comparison. IX. C ONCLUSION H-CRSPV makes evidence completeness a replicated invariant: obligations map to entries, proposer-induced groups pass policy and bind resolved objects, and only guarded finalization activates a release. Explicit ownership preserves late binding without redefining what must be proved. E THICS C ONSIDERATIONS The experiments use controlled model artifacts, local harnesses, and an isolated four-validator localnet; they do not attack production services or use human-subject data. The attack describes a class of verification-interface failures rather than a secret vulnerability in a named deployed system. We avoid presenting component proof systems, PEFT, provenance tools, Cosmos, or CometBFT as broken in their native threat models and will disclose any concrete implementation vulnerability discovered during integration to the affected maintainers before publication. R EFERENCES [1] B. Cottier, R. Rahman, L. Fattorini, N. Maslej, and D. Owen, “The rising costs of training frontier AI models,” arXiv preprint arXiv:2405.21015, 2024. [2] M. Demirer, Özlem Bedre-Defolie, L. Einav, and J. Levin, “The emerging market for intelligence: Pricing, supply, and demand for LLMs,” Working Paper 34608, National Bureau of Economic Research, Dec. 2025.

14

[3] E. J. Hu, Y. Shen, P. Wallis, Z. Allen-Zhu, Y. Li, S. Wang, L. Wang, and W. Chen, “LoRA: Low-rank adaptation of large language models,” in International Conference on Learning Representations, 2022. [4] H. Lycklama, A. Viand, N. Avramov, N. Kuechler, and A. Hithnawi, “Artemis: Efficient commit-and-prove SNARKs for zkML,” arXiv preprint arXiv:2409.12055, 2024. [5] H. Sun, T. Bai, J. Li, and H. Zhang, “zkDL: Efficient zero-knowledge proofs of deep learning training,” IEEE Transactions on Information Forensics and Security, vol. 20, pp. 914–927, 2025. [6] S. Mangrulkar, S. Gugger, L. Debut, Y. Belkada, S. Paul, B. Bossan, and M. Tietz, “PEFT, version 0.18.1.” Software release, https://github.c om/huggingface/peft/releases/tag/v0.18.1, 2026. [7] Hugging Face, “Safetensors, version 0.8.0.” Software release, https: //github.com/huggingface/safetensors/releases/tag/v0.8.0, 2026. [8] Cosmos SDK, “Cosmos SDK, version 0.50.5.” Software release, https: //github.com/cosmos/cosmos-sdk/releases/tag/v0.50.5, 2024. [9] E. Buchman, J. Kwon, and Z. Milosevic, “The latest gossip on BFT consensus,” arXiv preprint arXiv:1807.04938, 2018. [10] CometBFT, “CometBFT, version 0.38.6.” Software release, https://gith ub.com/cometbft/cometbft/releases/tag/v0.38.6, 2024. [11] A. Kate, G. M. Zaverucha, and I. Goldberg, “Constant-size commitments to polynomials and their applications,” in Advances in Cryptology – ASIACRYPT 2010, pp. 177–194, 2010. [12] D. Boneh, B. Lynn, and H. Shacham, “Short signatures from the weil pairing,” in Advances in Cryptology – ASIACRYPT 2001, pp. 514–532, 2001. [13] Qwen Team, “Qwen2.5 technical report,” arXiv preprint arXiv:2412.15115, 2024. [14] J. H. Saltzer and M. D. Schroeder, “The protection of information in computer systems,” Proceedings of the IEEE, vol. 63, no. 9, pp. 1278– 1308, 1975. [15] F. B. Schneider, “Enforceable security policies,” ACM Transactions on Information and System Security, vol. 3, no. 1, pp. 30–50, 2000. [16] Y. Liu, Y. Xue, D. Wu, Y. Sun, Y. Li, M. Shi, and Y. Liu, “PropertyGPT: LLM-driven formal verification of smart contracts through retrievalaugmented property generation,” in Network and Distributed System Security Symposium, 2025. [17] B. Kim, J. Hur, A. Ahmad, and B. Lee, “Secure data analytics in apache spark with fine-grained policy enforcement and isolated execution,” in Network and Distributed System Security Symposium, 2025. [18] E. Li, T. Mallick, E. Rose, W. Robertson, A. Oprea, and C. Nita-Rotaru, “ACE: A security architecture for LLM-integrated app systems,” in Network and Distributed System Security Symposium, 2026. [19] S. Torres-Arias, H. Afzali, T. K. Kuppusamy, R. Curtmola, and J. Cappos, “in-toto: Providing farm-to-table guarantees for bits and bytes,” in 28th USENIX Security Symposium, pp. 1393–1410, 2019. [20] OpenSSF, “Supply-chain levels for software artifacts (SLSA), version 1.0.” Technical specification, 2023. [21] Z. Newman, J. S. Meyers, and S. Torres-Arias, “Sigstore: Software signing for everybody,” in Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, pp. 2353–2367, 2022. [22] H. Birkholz, A. Delignat-Lavaud, C. Fournet, Y. Deshpande, and S. Lasker, “An architecture for trustworthy and transparent digital supply chains,” RFC 9943, Internet Engineering Task Force, June 2026. [23] G. C. Necula, “Proof-carrying code,” in 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 106–119, 1997. [24] B. Parno, J. Howell, C. Gentry, and M. Raykova, “Pinocchio: Nearly practical verifiable computation,” in 2013 IEEE Symposium on Security and Privacy, pp. 238–252, 2013. [25] A. Pnueli, M. Siegel, and E. Singerman, “Translation validation,” in Tools and Algorithms for the Construction and Analysis of Systems, pp. 151–166, 1998. [26] X. Leroy, “Formal verification of a realistic compiler,” Communications of the ACM, vol. 52, no. 7, pp. 107–115, 2009. [27] G. Ilharco, M. T. Ribeiro, M. Wortsman, S. Gururangan, L. Schmidt, H. Hajishirzi, and A. Farhadi, “Editing models with task arithmetic,” in International Conference on Learning Representations, 2023. [28] P. Yadav, D. Tam, L. Choshen, C. Raffel, and M. Bansal, “TIES-merging: Resolving interference when merging models,” in Advances in Neural Information Processing Systems, 2023. [29] W. Jiang, N. Synovic, R. Sethi, A. Indarapu, M. Hyatt, T. R. Schorlemmer, G. K. Thiruvathukal, and J. C. Davis, “An empirical study of artifacts and security risks in the pre-trained model supply chain,” in Proceedings of

the 2022 ACM Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses, pp. 105–114, 2022. [30] L. Wang, J. Wang, T. Cong, X. He, Z. Qin, and X. Huang, “From purity to peril: Backdooring merged models from “harmless” benign components,” in 34th USENIX Security Symposium, pp. 6339–6358, 2025. [31] B. Hassanshahi, T. N. Mai, A. Michael, B. Selwyn-Smith, S. Bates, and P. Krishnan, “Macaron: A logic-based framework for software supply chain security assurance,” in Proceedings of the 2023 Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses, pp. 29–37, 2023. [32] J. Samuel, N. Mathewson, J. Cappos, and R. Dingledine, “Survivable key compromise in software update systems,” in Proceedings of the 17th ACM Conference on Computer and Communications Security, pp. 61–72, 2010. [33] T. K. Kuppusamy, L. A. DeLong, and J. Cappos, “Uptane: Security and customizability of software updates for vehicles,” IEEE Vehicular Technology Magazine, vol. 13, no. 1, pp. 66–73, 2018. [34] A. Ferraiuolo, R. Behjati, T. Santoro, and B. Laurie, “Policy transparency: Authorization logic meets general transparency to prove software supply chain integrity,” in Proceedings of the 2022 ACM Workshop on Software Supply Chain Offensive Research and Ecosystem Defenses, pp. 3–13, 2022. [35] M. Moore, A. S. A. Yelgundhalli, and J. Cappos, “Securing automotive software supply chains,” in Symposium on Vehicles Security and Privacy, 2024. [36] A. Chiesa and E. Tromer, “Proof-carrying data and hearsay arguments from signature cards,” in Innovations in Computer Science, pp. 310–331, 2010. [37] C. Weng, K. Yang, X. Xie, J. Katz, and X. Wang, “Mystique: Efficient conversions for zero-knowledge proofs with applications to machine learning,” in 30th USENIX Security Symposium, pp. 501–518, 2021. [38] T. Liu, X. Xie, and Y. Zhang, “zkCNN: Zero knowledge proofs for convolutional neural network predictions and accuracy,” in Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, pp. 2968–2985, 2021. [39] H. Sun, J. Li, and H. Zhang, “zkLLM: Zero knowledge proofs for large language models,” in Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security, pp. 4405–4419, 2024. [40] Z. Wang, N. Dong, J. Sun, W. Knottenbelt, and Y. Guo, “zkFL: Zeroknowledge proof-based gradient aggregation for federated learning,” IEEE Transactions on Big Data, vol. 11, no. 2, pp. 447–460, 2025. [41] G. Liao, T. Wang, S. Zhang, J. Zhang, L. Shi, and D. Tao, “VeriLoRA: Fine-tuning large language models with verifiable security via zeroknowledge proofs,” in Network and Distributed System Security Symposium, 2026. [42] S. Pailoor, Y. Chen, F. Wang, C. Rodrı́guez, J. V. Geffen, J. Morton, M. Chu, B. Gu, Y. Feng, and I. Dillig, “Automated detection of underconstrained circuits in zero-knowledge proofs,” Proceedings of the ACM on Programming Languages, vol. 7, no. PLDI, pp. 1510–1532, 2023.

[43] S. Chaliasos, J. Ernstberger, D. Theodore, D. Wong, M. Jahanara, and B. Livshits, “SoK: What don’t we know? understanding security vulnerabilities in SNARKs,” in 33rd USENIX Security Symposium, pp. 3855–3872, 2024. [44] J. Qiu, C. Cai, S. Bhatia, N. Hasabnis, S. A. Seshia, and A. Cheung, “Tenspiler: A verified-lifting-based compiler for tensor operations,” in 38th European Conference on Object-Oriented Programming (ECOOP), pp. 32:1–32:28, 2024. [45] H. Kalodner, S. Goldfeder, X. Chen, S. M. Weinberg, and E. W. Felten, “Arbitrum: Scalable, private smart contracts,” in 27th USENIX Security Symposium, pp. 1353–1370, 2018. [46] M. Al-Bassam, A. Sonnino, and V. Buterin, “Fraud and data availability proofs: Maximising light client security and scaling blockchains with dishonest majorities,” arXiv preprint arXiv:1809.09044, 2018. [47] Z. Zheng, P. Xie, X. Zhang, S. Chen, Y. Chen, X. Guo, G. Sun, G. Sun, and L. Zhou, “Agatha: Smart contract for DNN computation,” arXiv preprint arXiv:2105.04919, 2021. [48] S. Das, V. J. Ribeiro, and A. Anand, “YODA: Enabling computationally intensive contracts on blockchains with byzantine and selfish nodes,” in Network and Distributed System Security Symposium, 2019. [49] L. Yu, B. Yu, H. Yu, F. Huang, and Y. Li, “Language models are super mario: Absorbing abilities from homologous models as a free lunch,” in Proceedings of the 41st International Conference on Machine Learning, vol. 235 of Proceedings of Machine Learning Research, pp. 57755–57775, PMLR, 2024. [50] S. Meiklejohn, H. Blauzvern, M. Maruseac, S. Schrock, L. Simon, and I. Shumailov, “Position: Machine learning models have a supply chain problem,” in Proceedings of the 42nd International Conference on Machine Learning, vol. 267 of Proceedings of Machine Learning Research, pp. 81774–81785, PMLR, 2025. [51] X. Mu, Y. Wang, Y. Zhang, J. Zhang, H. Wang, Y. Xiang, and Y. Yu, “Model provenance via model DNA,” in ECAI 2024, IOS Press, 2024. [52] M. Spoczynski, M. S. Melara, and S. Szyller, “Atlas: A framework for ML lifecycle provenance & transparency,” in 2025 IEEE European Symposium on Security and Privacy Workshops, pp. 448–461, 2025.

G ENERATIVE -AI U SE D ISCLOSURE OpenAI Codex desktop was used interactively in July 2026; the client did not expose a stable model or build identifier. It assisted with prose drafting, restructuring, and compression in the Abstract, Introduction, design and security-model sections, evaluation framing, Discussion, Related Work, Conclusion, tables, figure captions, and this disclosure. It also assisted with code scaffolding, test generation, experiment orchestration, result-packaging scripts, and diagnostic review. No model was permitted to manufacture measurements or silently replace missing results: the release source imports frozen machinereadable results and fails if its generated result macros are absent. The authors defined the research question and protocol, supplied and reviewed the implementation and source materials, executed or supervised the experiments, inspected raw logs, verified result-to-claim mappings and citations, and edited every generated passage and code change. The authors accept responsibility for the complete submission; no generative system is listed as an author. A PPENDIX A S IZE -M ATCHED A SSURANCE –C OST B OUNDARY The small PEFT workload favors replay. We retain a separate Qwen2.5-3B-sized adapter-space workload only as an operating-region study. Its package does not establish an originating repository revision, source Safetensors hashes, or lowering certificate and therefore is not a provenanceverified Qwen artifact. Its legal policy requires mandatory typed bindings, one deterministic KZG global relation, and

15

a) Deferred audit details: The production profile identifier is relationir-core-v1; its full SHA-256 value (abbreviated b0af034e. . . 893f70e4) is bound into program, obligation, and transcript identities. The authenticated coreference gate accepts the honest registrar transcript and rejects 18/18 context, descriptor, root, domain, length, and canonicalstream substitutions. One prerelease in-toto layout and static workflow authorization bind a single Safetensors digest before any release; unsigned proposer envelopes later select release realizations, while release-bound aggregate certificates remain required.

TABLE VII L ATE - BINDING COMPARISON . “Y ES ” UNDER ri MEANS THAT THE MECHANISM IDENTIFIES A COMPLETE REQUIREMENT SET FOR THAT RELEASE .

Replicated finality Added online actor

Complete requirements

Actual object

Mechanism

r1

r2

r3

bound

owned

Frozen plan Trusted planner Fixed inspector H-CRSPV

Yes Yes Yes Yes

No Yes Yes Yes

No Yes Yes Yes

No No No Yes

No No No Yes

None Planner call None Certifier quorum

The isolation launcher records 3 receipts, 0 successful privatekey canary reads, 0 private-key mounts, and 0 signer sockets after signer exit. A separate offline Qwen control retains 24 samples and the corresponding native and omission receipts. Supporting campaigns accept 128/128 generated legal manifests and 90/90 honest plans; reject 466/466 requirement mutations and 90/90 concrete attacks; report no Python/Rust/Go mismatch over 10,000 legal programs; expose all 12 targeted guard ablations; and detect all 15 injected failures in 2,729 localjudge cases. These records support implementation auditability and do not alter the main RQ outcomes.

exhaustive CertifiedLocal coverage; a k = 8 opening diagnostic cannot discharge local obligations. For validator count V , reuse R, bandwidth B, online evidence bytes SE , and replay-input bytes SX , the modeled accounting is CH = Treg /R + V (Tverify + SE /B), CR = V (Treplay + SX /B).

The retained size-matched study derives 5,420 obligations (5,400 C ERTIFIED L OCAL, 19 M ANDATORY, and one G LOB AL A LGEBRAIC ) and measures an 18-realization historical operating point. It is not used as evidence for the current A–D group/object or lifecycle claims. Thirty Rust rows give 167.943/178.765 ms mean/P95 for the production-SRS global relation and 2,663.263/2,729.535 ms for deterministic replay. A. Retrieval and Lifecycle Accounting Requirement reconstruction and admission are single observed stages of 3,042.165 and 3,349.522 ms. Separately measured components model a policy-complete validator at 7.870 s versus Table VIII counts validator-side HTTP response bodies. In 5.582 s for replay. This is a negative CPU result, not a crossover the fresh r row, 9,639,900 reusable-component bytes are 2 or observed end-to-end Qwen claim. Replay also removes the not cache hits: the measured cache-hit count is 0. ReleaseCertifiedLocal quorum assumption, so the comparison is not bound traffic is 506,996 bytes across four validators, i.e., same-assurance. 126,749 unique source bytes fetched once per validator. The Separate planner tests accept canonical and cost-optimized table excludes 422,127 bytes of provider-plane traffic; RQ6’s realizations for 160 randomized legal configurations and inclusive ratio adds that traffic explicitly. reject 960 resealed omission, incompatible-batch, wrongpredecessor, downgrade, DA-expiry, and challenge-window attacks. The objective is synthetic and makes no optimalTABLE VIII ity claim. A fresh-process scaling run accepts all 40 rows E3 VALIDATOR - RETRIEVAL BYTE LEDGER ( AGGREGATE HTTP RESPONSE BODIES ). from 102 to 105 obligations; at 100,000 obligations, checker mean/P95 is 493.3/663.5 ms, total plan-plus-check mean/P95 Fresh Continuous Warm r2 r1 → r2 → r3 r1 → r2 is 588.0/805.8 ms, and maximum peak RSS is 142.0 MiB on Metric (bytes) the stated 8-CPU macOS host. Replay input 12,396,243,912 – 0 H-CRSPV retrieval Reusable component Cache hit Release-bound Stale response

A PPENDIX B S UPPLEMENTARY E VALUATION E VIDENCE

10,146,896 9,639,900 0 506,996 0

11,140,644 506,996 – 9,639,900 19,279,800 9,639,900 1,500,744 506,996 953,252 446,256

The detailed dynamic late-binding comparison follows. The following tables retain the measurements needed to interpret the main-text claims. Full identities, raw receipts, Each release is one wall-clock observation (n = 1). In rejection logs, and the claim lock remain in the frozen artifact. Table IX, Gap is measured wall time between instrumented For E3, each lifecycle is one observation (n = 1); timing stages, and Residual is end-to-end time minus the sum of stages are disjoint, and the byte ledger separates cache hits all named stages and Gap. A zero residual is an accounting from reusable and release-bound bytes. identity, not a variance or accuracy estimate.

16

TABLE IX E3 WALL - CLOCK LIFECYCLE DECOMPOSITION ( MS ); ADMISSION AND FINALIZATION STAGES ARE DISJOINT. r1

Stage

r2

r3

Candidate Publish Catalog Plan Materialize+BLS Admit Policy wait Finalizer Gap

5,411.49 3,109.96 1,993.44 5,805.65 7,730.45 9,669.22 23.57 16.75 20.97 42.21 31.51 35.31 21,962.55 86,873.13 135,517.20 8,047.30 8,130.41 7,781.96 239,540.68 169,596.33 124,102.82 615.89 1,612.12 635.73 360.43 350.42 455.19

End-to-end Residual

281,809.77 277,451.08 280,211.84 0.00 0.00 0.00

B. Attack Controls and Secondary Evidence For every attack in Table X, a nonzero evidence-transaction ABCI code means deterministic rejection with no admitted release mutation; the subsequent cancel transaction returns code zero, meaning that cleanup commits successfully. The packaged verifier recomputes the owning gate from the raw log rather than trusting the normalized label. TABLE X C OMMITTED E3 ATTACK CONTROLS AND INDEPENDENTLY RECOMPUTED REJECTION GATES .

Attack

Mutation; owning gate

Omission

Remove one required entry; entry/group exactness Cover one member twice; typed disjointness Reuse a prior-release payload; release/object binding Bind another program or artifact; artifact/program binding

Overlap Stale Crossbinding

Evidence / cancel ABCI

Replicas

>0/0

Reject; 4/4

>0/0

Reject; 4/4

>0/0

Reject; 4/4

>0/0

Reject; 4/4

Table XII separates output-level consequences from localjudge conformance. The 36 artifacts are the RQ4 omission artifacts; the 2,729 judge cases and 15 injected failures are a distinct implementation campaign and are not added to the attack denominator. A PPENDIX C R ELATION IR-C ORE V 1 R EQUIREMENT RULES Table XI summarizes the rule families used by the current checker. A future extension is covered only after it adds a type rule, base obligations, propagation conditions, normalized keys, admissible backends, and a witness or interpreter interface.

17

TABLE XI R EQUIREMENT RULES IMPLEMENTED BY THE CLOSED R ELATION IR-C ORE V 1 PROFILE . Primitive

Base requirements

Propagated requirements

Input/output descriptors AffineCombine

Artifact, type, domain, commitment, Output binding and lineage reachability Coefficients, predecessors, affine Dependency and commitment domains relation Transform, seed/mask or scale, RangeOK and exact source block witness Divisor, signed lift, tie rule RangeOK and overflow

LocalMap: drop/scale LocalMap: round-div LocalMap: quantize Scale, clipping, cast, rounding Reindex Total block map; unique outputs Provisional local Relation digest and signer set backend

Signed input/output ranges Layout and dependency mapping DA, challenge, fraud, finalization

A. Normative Integer and Tensor Semantics The current R ELATION IR-C ORE V 1 language evaluates canonical integer tensors, not host floating point. A tensor type T = (shape, layout, w, s, B, q, d) binds shape and coordinate order, signed width w, fixed-point scale s, declared absolute bound B, field modulus q, and commitment domain d. A decoded coordinate x is valid only when −2w−1 ≤ x < 2w−1 ,

Evidence path

|x| ≤ B < q/2,

Mandatory typed checks Production KZG Direct or CertifiedLocal judge Direct or CertifiedLocal judge Direct or CertifiedLocal judge Deterministic judge BLS certificate and lifecycle

B. Normative Canonicalization Protocol identities hash a versioned, domain-separated canonical encoding. Accepted structured values use sorted object keys, order-preserving arrays, base-10 integers only, UTF-8 text with deterministic escaping, and no insignificant whitespace; mathematical sets are sorted by their canonical byte encoding before hashing. Tensor bytes use registered signed width, endianness, coordinate order, length, and block partition. The registration, obligation, witness, transcript, and output domains use distinct tags. A production decoder must reject duplicate identifiers, noncanonical numeric forms, unknown primitive versions, and any descriptor/byte-length mismatch before computing an identity. The independent Rust oracle tests the current Python encoding, but neither implementation is mechanized; this bridge remains in the TCB.

(24)

and its field encoding is x mod q. The B < q/2 premise makes the registered signed lift unique; an affine field equality without the corresponding range obligations is insufficient. For d > 0, the only registered division rule is nearest-integer rounding with halves away from zero:   |x| + ⌊d/2⌋ rndd (x) = sgn(x) , (25) d

A PPENDIX D E XTENDED S COPE AND D EPLOYMENT B OUNDARIES

with rndd (0) = 0. The implemented primitives have the following coordinate semantics, with every displayed parameter loaded from the registered node rather than from a witness: Scalea (x)j = axj , ( axj Keep(σ, j) = 1, DropRescaleσ,a (x)j = 0 otherwise, m X Affinea (x1 , . . . , xm )j = ai xi,j , i=1

RoundDivd (x)j = rndd (xj ), Quantized,ℓ,u (x)j = min(u, max(ℓ, rndd (xj ))), Reindexπ (x)j = xπ(j) . Keep is a versioned deterministic bit generator bound to seed σ and global coordinate j. The P affine range rule requires a declared output bound at least i |ai |Bi and below q/2; scaling, rounding, and quantization propagate the corresponding arithmetic bounds. π must be a bijection over [0, n); the implemented packing profile additionally requires each output block, including a final partial block, to select one contiguous, aligned source block. These predicates define the current claim; alternative stochastic masks, zero-point quantization, arbitrary reshapes, and host-language casts are rejected as unsupported.

18

The main result treats RelationIR as authoritative. For the supported declarative PEFT/Safetensors subset, CheckLower binds source configuration, tensor bytes, consumer mapping, and output identity to R ELATION IR-C ORE V 1; 60 source/IR mutations exercise this bridge. A separate checker validates a 71-event executor trace and rejects 9/9 mutations, including four that recompute the program hash after changing sourcerelevant fields. The executor parses PEFT-format artifacts but does not instrument arbitrary PEFT, Python, Torch, or custom kernels; unsupported execution is rejected. Exact binding moves security weight onto decoding and canonicalization. Ambiguity in signed encodings, endianness, layout, shard order, or duplicate identifiers remains a fileto-vector TCB failure rather than a backend-proof failure. CertifiedLocal soundness and finalization remain conditional on the configured committee, data availability, watcher, challenge inclusion, and deadline assumptions; deployments that reject these assumptions require a liveness-independent proof or replay for critical relations. Finally, the four-validator localnet demonstrates current-schema admission and deterministic replicated rejection, not sustained throughput, external-DA retention, or production-chain finality. A centralized auditor can run the

same checker; consensus is useful only when multiple parties require shared ordering and consequences.

f) Model-artifact composition: LoRA, task arithmetic, sparse merging, and adapter composition define the composition substrate [3], [27], [28], [49]. Model-supply-chain studies, merge-time backdoors, Model DNA, and Atlas motivate pipeline-wide integrity and lineage [29], [30], [50]–[52]. These works expose or track unsafe components and compositions; H-CRSPV instead enforces release-time completeness for one closed, authority-declared profile.

A PPENDIX E E XTENDED R ELATED W ORK

H-CRSPV composes established primitives around a distinct enforcement boundary. The relevant comparison is whether a system owns required-set construction, policy validation of proposer grouping, concrete-object resolution, and activation A PPENDIX F when a later actor controls realization (Table I). P ROOF D ETAILS a) Reference monitors and complete mediation: Complete mediation checks every security-relevant access, whereas A. Finite Requirement Construction execution monitors enforce policies recognizable from observed For a fixed well-typed program and block partition, registered events [14], [15]. H-CRSPV specializes this principle to nodes, edges, blocks, outputs, and policy clauses are finite. plan-to-evidence admission: it derives the reference set before Equation (12) therefore yields a finite list, and canonical sorting realization and mediates entries, proposed groups, resolved terminates. The implementation uses topological enumeration objects, and final activation. plus validation, not a fixed-point or worklist algorithm. b) Specification and plan-to-execution enforcement: PropertyGPT generates and checks candidate smart-contract B. Replica Determinism properties [16]; LAPUTA checks Spark physical plans and Fix canonical bytes for ρ, Γ, E, and the authenticated keeper protects their execution [17]; ACE separates trusted abstract snapshot K. Canonical decoding either fails at every correct plans from untrusted concrete mappings [18]. H-CRSPV starts replica or yields the same typed values. On the accepting from an authenticated finite requirement set and extends planbranch, Req(ρ) is a pure topological traversal of the same to-execution enforcement through registered-policy validation finite DAG; Norm(Γ) is a pure typed normalization; canonical of proposed evidence sharing, keeper-object binding, and the sorting followed by a duplicate ordinal fixes every occurrence provisional-to-active transition. tag; and equality of κρ fixes the same proposer-induced quotient c) Supply-chain provenance and transparency: in-toto classes. Each class and object key is then traversed in canonical and SLSA bind declared steps and provenance, while Macaron byte order. Finally, the resolver is a function of the same releaseevaluates logic-based supply-chain policies [19], [20], [31]. scoped payload and keeper snapshot. Functional composition Sigstore/Rekor, TUF, Uptane, Policy Transparency/PolyLog, therefore gives identical R, M , G, Oρ , and acceptance bits. SCITT, and Scudo add signing, update, transparency, receipt, This argument requires the canonical decoder and resolver and root-composition layers [21], [22], [32]–[35]. These assumptions in Table II; it is not a claim about faulty replicas. systems authenticate workflow assertions and their history. They do not automatically derive the complete semantic- C. Lemma 1 relation multiset of a late-bound model release or bind it to Let R = Req(ρ) and M = Norm(Γ). Registration freezes one replicated consumer state; they can enforce H-CRSPV’s boundary when policy also supplies the constructor, object ρ. For each o ∈ Uρ , the checker counts the occurrence-tagged entries whose typed projection is o. Acceptance establishes resolver, and final-state rule. ρ )# Occ(M ) (o) = multR (o), including zero on both sides d) Proof-carrying and verifiable computation: Proof- mult(πobl for identities absent from R. Hence no occurrence can project carrying and verifiable-computation systems check supplied to an unexpected identity, and every required occurrence has exexecutions or claims [4], [5], [23], [24], [36]–[41]; underactly one matching entry occurrence. The remaining accepting constrained-circuit analyses find unintended witnesses [42], branches compare each entry’s authority hash, node, relation, [43]. SOVE instead omits an externally required statement: every received proof may be sound while one required proof primitive, endpoints, coordinates, parameters, dependencies, to is absent. A proof system closes that gap only when its public assurance policy, and interpreter version with the obligation ρ statement, circuit, or admission layer also commits to required- which it projects. They establish ExactEntryBindρ (m, πobl (m)) for every m ∈ Occ(M ). These two facts are exactly Eq. (8); set equality. e) Compilation and optimistic verification: Transla- equivalently, they induce a multiplicity-preserving bijection tion validation, CompCert, and Tenspiler connect programs between required and admitted occurrences. to checked realizations [25], [26], [44]; fraud-proof and D. Lemma 2 outsourced-computation systems challenge available invalid transitions or replicated results [45]–[48]. H-CRSPV’s frontend Equality of the complete typed key κρ induces the equivais narrower: it binds one declarative PEFT/Safetensors subset lence relation ∼mat , so the grouping proposed by those entry to a closed RelationIR profile, then keeps every bound relation keys has a unique quotient whose classes partition Occ(M ). provisional while its watcher-completeness premise applies. These are proposed groups, including any singleton classes.

19

ρ Since Og = (πobl )# g and pushforward commutes with disjoint multiset union,   ] ] ρ ρ Og = (πobl )#  g  = (πobl )# Occ(M ) = R, g∈G

expose at least one operational realization-gap branch; no reverse equivalence is needed because the operational checker may reject additional malformed or unsupported realizations. G. Lemma 3

g∈G

Let s0 , . . . , sk = s witness Reachρ (s). We prove Eq. (21) where the last equality is Lemma 1. The registered batching by induction on k. At k = 0, the initial state contains neither checks then establish GroupOK for every proposed group; ACTIVE nor an accepted record, so the antecedent is false. only those passing classes are admissible, and non-shareable or For the inductive step, consider (sk−1 , ak−1 , sk ) ∈ ∆ρ . If incompatible classes reject. This check does not prove that an the release was already consumable in sk−1 , the induction object covers Og . After all groups are admissible, the resolver hypothesis supplies a witnessing finalizer; terminal immutability reads typed payloads and registered state, not a proposer- preserves exact admission, zero disputes, certificate state, and supplied digest, and accepts exactly one object per class only settlement in sk . Otherwise, consumability is newly true in sk . if both its canonical statement and full materialization key By the writer restriction on ∆ρ , ak−1 must be finalize(ℓ). agree. Totality of µ excludes a group with no object, injectivity Its guard supplies the immutable exact-admission record, excludes cross-group object reuse, and surjectivity excludes any h(sk−1 ) > dℓ , the preserved window, all-group eligibility, and resolved orphan object outside the image of a group. The two zero disputes, while its atomic write supplies active, accepted, equality checks reject cross-context or unrelated statements. finalized certificates, and one-time bond settlement. Taking This proves Eqs. (9) and (11); constructor or resolver bugs u = sk−1 and v = sk witnesses Finalizedρ (ℓ, sk ). remain explicit TCB failures. No ordering corner case adds another branch: a challenge is enabled through h = dℓ , whereas finalization requires h > dℓ ; E. Proof of Theorem 1 accepted transactions are linearized within each block. Thus an The structural accepting path is the sequential composition included deadline challenge reaches terminal I NVALID before of the entry phase and materialization/object phase over any later finalizer can be enabled. Rejection, expiry, and upheldone authenticated authority snapshot. Lemma 1 supplies the challenge states are terminal and non-consumable, and replay exact obligation–entry multiset equality. Lemma 2 reconstructs cannot repeat the atomic settlement. the quotient proposed by complete entry keys, checks its disjoint complete union, admits every group under GroupOK, H. Proof of Proposition 1 resolves the actual typed objects from payloads and keeper Proposition 1 is conditional on primitive adequacy, backend state, and establishes the canonical-statement bijection. Their lifting, canonicalization, co-reference, and watcher completeconjunction is StructOKρ , equivalently the negation of Eq. (5), ness over the registered R ELATION IR-C ORE V 1 program. Lemand establishes Eq. (19). No step invokes a backend truth-lifting mas 1–2 supply exactly the obligations and actual objects used rule, source-lowering claim, external co-reference adequacy by Eq. (22). Direct and KZG acceptance supplies their typed premise, watcher, or finalizer; those premises enter only the semantic predicates by backend soundness. For a CertifiedLocal semantic and lifecycle results. class, assume for contradiction that its registered conjunction is false. WatcherCompleteρ (ℓ) supplies detection, valid typedchallenge construction, timely submission, and inclusion; judge Fix one operational instance OpRepρ,ℓ (q, K) = (Γ, E, Aout ). completeness upholds the challenge and transitions the release On the accepting branch, Lemma 2 yields the unique bijection to terminal I NVALID. This contradicts reachable consumability ∼ µ:G− → Oρ (E, K). We therefore instantiate SubObj(q) by its by Lemma 3, so every class conjunction used by a consumable codomain and define Covρ,ℓ (q, µ(g)) = Og . release is true. This definition is total on SubObj(q) because µ is surjective. Now induct over the registered topological order. Registered It is single-valued because µ is injective and the resolver input nodes form the base case by the authority and co-reference rejects duplicate complete object keys. It is authority-scoped premises. For node n , the induction hypothesis equates every j because GroupOK checks the exact obligation multiset and both predecessor value with its reference value; the exact NodeReq equalities in Eq. (11) bind the canonical statement, complete predicates and the stated per-node adequacy implication then context, and materialization key. Finally, yield Vj = Vj∗ . The output-map obligation and object binding ] ] identify the final reference value with the consumer artifact. Covρ,ℓ (q, e) = Covρ,ℓ (q, µ(g)) The present mixed KZG/Merkle path still trusts registration to g∈G e∈SubObj(q) ] resolve both roots to one canonical stream. = Og = Rρ , g∈G I. Scope of Claim 1 F. Operational–Abstract Correspondence

where the first equality reindexes by the bijection and the last is Eq. (9). Thus both clauses of Eq. (3) hold. Conversely, contraposition shows that an abstract SOVE accepted by a submitted-object interface on this operational instance must

20

For the supported frontend, CheckLower reparses source configuration and Safetensors metadata, recomputes content hashes, and compares every registered source tensor, LoRA parameter, consumer port, and output mapping with the

fields used to construct P . Those checks establish recorded field equality, not a general semantic theorem for Python. Observational equality of the supported source evaluator and R ELATION IR-C ORE V 1 evaluator is therefore named explicitly as FrontendRelρ and kept in the frontend TCB. Conditional on that invariant, Proposition 1 transfers immediately to the bound source output. Parser or correspondence bugs remain lowering-TCB failures. J. Corollary 1 Any omitted or duplicated entry contradicts Lemma 1. Any overlapping, incomplete, incompatible, reused, cross-bound, or orphan materialization contradicts Lemma 2 and therefore Theorem 1. In every reachable state, a release that remains provisional, has an open dispute, lacks exact admission, or is marked settled without a witnessing finalizer cannot satisfy Eq. (16). A provisional release may satisfy Eq. (15) only after the deadline with exact admission, all groups eligible, and no open dispute; the enabled finalizer then atomically changes it to ACTIVE with an accepted record. Hence no structurally defective or unfinalized release is consumable, regardless of the validity of the objects that were submitted. TABLE XII S ECONDARY EVALUATION EVIDENCE : OUTPUT EFFECTS AND LOCAL - JUDGE CONFORMANCE . (a) Effect distribution across 36 PEFT attack artifacts Metric

Median

P95

Max

Logit L∞ 0.0478 1.2254 2.2688 Changed coordinates (%) 0.0244 1.4771 1.5381 Weight-delta L2 0.0560 1.4277 1.4940 Top-1 position change (%) 0 6.25 16.67 (b) Local-judge conformance Primitive Drop-rescale RoundDiv Quantize RangeOK Reindex/sharding Total

Injected Cases failures caught 545 551 551 543 539

3/3 3/3 3/3 3/3 3/3

2,729

15/15

A PPENDIX G E VIDENCE S UMMARY Table XIII maps RQ1–RQ6 to frozen evidence and claim boundaries; the full inventory, commands, hashes, and claim lock remain in the artifact. The 39 structured lifecycle records decompose as 1 legal +35 committed attacks +1 replay +2 prepublication controls. Accordingly, the 37 committed Cosmos decisions are the legal release, 35 attacks, and replay; “37 attack controls” elsewhere means the 35 committed attacks plus the two prepublication controls.

21

TABLE XIII F ROZEN EVIDENCE - TO - CLAIM SUMMARY. C OUNTS WITH DIFFERENT DENOMINATORS ARE NOT COMBINED . RQ

Frozen observation

1

Exact entries/groups/objects. 345 entries → 26 admissible shared-evidence groups → 26 Trusted registrar; no KZG–Merkle equality proof; entries are not independent proofs. objects; six omissions and 18 co-reference substitutions reject. Reachable lifecycle safety. 37/37 committed Cosmos decisions converge: one legal release, Four-validator localnet, loopback DA, local finality. 35 attacks, and one replay; two prepublication controls remain separate. Dynamic late binding. E1 has 3 legal and 10 invalid partitions with 13/13 convergence. In Six same-host HTTP processes; each E3 lifecycle has E3, the frozen plan is complete only for r1 ; the trusted planner, fixed inspector, and n = 1. H-CRSPV are complete for r1 , r2 , r3 . Source binding/fair completeness. Six source instances bind; 60/60 source mutations and Declarative PEFT/Safetensors subset; frontend relation 36/36 loadable omissions reject; complete baselines accept 6/6 honest cases. and interpreter remain in the TCB. Replicated admission. One artifact identity, prerelease authorization, 11 aggregate 3-of-4 Centralized test keys; unsigned release envelopes. certificates, and 33 signer participations retain one lineage. Cost/deployment boundary. Fresh: 1,221.68× replay/evidence; warm: 0/506,996 bytes; One fresh and one warm point; not latency, optimized size-matched CPU result is negative. replay, throughput, or same assurance.

2 3

4 5 6

Claim boundary

A PPENDIX H S UPPLEMENTARY VALIDATION C AMPAIGNS A. Requirement Construction Generated R ELATION IR-C ORE V 1 tests accept 128/128 legal manifests and reject 466/466 mutations across 21 rule families; a multi-seed campaign accepts 90/90 honest plans and rejects 90/90 endpoint-changing attacks. Python, Rust, and Go agree on 10,000 legal obligation roots, reject nine malformed cases and 30/30 profile mutations, and agree on 1,882 bounded semantic cases. An independent Rust oracle matches 10,000 valid programs, rejects 2,000 invalid programs, and direct mutation rejects 50/50 non-equivalent changes across 18 families. These finite campaigns reduce correlated implementation risk but do not prove profile or rule-table adequacy. B. Guards and Local Semantics Thirty-two context, root, endpoint, coordinate, parameter, and reindex controls match expectations. Twelve guard ablations cover anti-downgrade, batch compatibility, DA expiry, and challenge timing: every attack rejects under the full verifier and passes only its matching ablation; honest input passes both. This shows necessity in the evaluated cases, not minimality. A separate 2,729-case judge harness detects all 15 injected failures. Because fixtures are shared, this is conformance evidence, not formal validation.

22

Related documents

• H-CRSPV: Preventing Semantic Omission in Late-Bound Large Language Model Releases#1202408
• PrefixPlace: Provable Prefix Key-Value Placement for Large Language Model Serving under Heterogeneous Compute and Transfer Costs#423930
• Software Testing With Large Language Models: Survey, Landscape, and Vision#16631
• Robustness of LLM-Generated SystemVerilog Assertions to Semantics-Preserving RTL Transformations#972709
• NebulaSD: Many-for-Many Speculative Decoding#1108689