Status: NORMATIVE. Depends on TRVM-PROOF-WIRE-v1.md, which defines the wire, the content address, resolution, input ownership and resource policy. This document defines one proof protocol carried on it.
Conformance vectors: vectors/manifest.json.
A nested composition asserts the conjunction of the claims named by its operands, and nothing else. It carries none of them: each is named by a content address and resolved from an untrusted store.
The theorem is deliberately trivial. What the protocol is for is the shape — a proof DAG whose shared nodes are stored once and whose every node is judged by the checker of its own protocol.
An artifact of this protocol has exactly these members. Every one is required except the three marked non-semantic.
| member | plane | answers |
|---|---|---|
protocol | CHECKED | which protocol this is |
claim | semantic | WHAT is asserted |
chain_ids | derived | UNDER WHICH COMPILERS |
references | transport | WHERE THE OCTETS ARE |
aggregate | evidence | WHAT EVIDENCE HOLDS |
structure | shape | WHAT SHAPE THE DAG IS |
type, version, annotations | NON-SEMANTIC | nothing |
A sixth plane — verifier execution, how many times a checker ran and whether it reused a derivation — is not in the artifact at all. It is a property of a verification run, no artifact can be right about it, and placing it in the claim or the aggregate means a sound verifier changing strategy renames the theorem.
2.1. `claim.operands` MUST NOT contain an address. A locator may rename the artifact carrying a proof; it MUST NOT rename the proof. An implementation that binds artifact_root into the claim identity will find that rewording a non-semantic annotation on a leaf renames the theorem at every level above it.
2.2. What an artifact may state about its own shape MUST be strategy-independent. edges and films_below_by_edge_multiplicity are properties of the DAG. checker_evaluations is not.
2.3. `annotations` establishes nothing. It is bounded to strings, arrays of strings, and flat records of those. It is inside the artifact root — so editing it changes the artifact's address — and it is outside every semantic identity, so editing it changes no claim, aggregate or certificate.
protocol is the string TRVM-NESTED-COMPOSITION-v2.
bundle = { protocol, claim, chain_ids, references, aggregate, structure,
type?, version?, annotations? }
claim = { connective, scope, operands, nested_claim_sem_id }
scope = { kind, quantifier, generalizes_beyond_children,
children_rechecked_by_their_own_checkers, parent_rederives_leaf_evidence }
operand = { protocol, claim_sem_id, aggregate_id, verified_claim_sem_id }
references = { contract, operands }
contract = { resolution, wire, address_is_a_warrant }
reference = { verified_claim_sem_id, artifact_root }
chain_ids = { leaf_chains }
aggregate = { operands, child_verdicts, leaf_receipts_rederived_by_parent,
films_replayed_by_parent, nested_verdict, aggregate_id }
structure = { edges, unique_artifacts, max_depth_below, bytes_if_inlined, unique_bytes,
films_below_by_edge_multiplicity, films_below_distinct,
cases_below_by_edge_multiplicity, cases_below_distinct, structure_sem_id }3.1. The key sets are EXACT. A member not listed for a record is a refusal. This is not a convenience: a producer that can add a member can state things the checker never agreed to without altering any value the checker reads. Extending the vocabulary is a protocol revision.
3.2. The checker owns the vocabulary. An implementation MUST declare these key sets itself and MUST NOT read them from the artifact.
3.3. Values the checker declares (CHECKED — compared against the implementation's own copy, never read from the artifact):
scope.kind "NESTED_COMPOSED_VERIFIED_CLAIM_CONJUNCTION"
scope.quantifier "OVER_CITED_CHILD_CERTIFICATES"
scope.generalizes_beyond_children false
scope.children_rechecked_by_their_own_checkers true
scope.parent_rederives_leaf_evidence false
references.contract.resolution "CONTENT_ADDRESSED"
references.contract.wire "CANONICAL"
references.contract.address_is_a_warrant false
claim.connective one of ["CONJUNCTION"]A scope value that is a string containing whitespace is a refusal: explanatory prose does not belong in a machine-readable value.
All three use the canonical encoding of TRVM-PROOF-WIRE-v1.md §1 and a domain-separation prefix that is part of the preimage.
nested_claim_sem_id = "nclaim-" ++ hex(SHA-256(
"TRVM-NESTED-COMPOSITION-v2|" ++ canonical_bytes({
protocol: "TRVM-NESTED-COMPOSITION-v2", connective, scope, operands })))
aggregate_id = "nagg-" ++ hex(SHA-256(
"TRVM-NESTED-COMPOSITION-v2|" ++ canonical_bytes(aggregate WITHOUT aggregate_id)))
structure_sem_id = "nstruct-" ++ hex(SHA-256(
"TRVM-NESTED-COMPOSITION-v2|" ++ canonical_bytes(structure WITHOUT structure_sem_id)))4.1. nested_claim_sem_id binds the operand sequence. Two artifacts differing only in operand order are different claims.
4.2. The certificate identity of a child, verified_claim_sem_id, is defined by the certificate protocol and binds (protocol, claim_sem_id, aggregate_id, chain_ids) together. An artifact that does not carry all four cannot be cited at all — this is citability, and it comes before identity, availability and warrant.
4.3. The verifier's own coordinates. Two further identities are about the VERIFIER rather than the artifact, and are reported with the verdict rather than sealed into it:
verifier_policy_id = "nestpol-" ++ hex(SHA-256(
"TRVM-NESTED-COMPOSITION-v2|" ++ <the effective policy, key-sorted k=v joined by "|">))
child_protocol_set_id = "nestcps-" ++ hex(SHA-256(
"TRVM-NESTED-COMPOSITION-v2|" ++ canonical_bytes(
the SORTED supplied list of {protocol, checker_id, claim_field})))When a table was supplied, child_protocol_set_id is folded into the preimage of verifier_policy_id, so one coordinate names both what was bounded and who was allowed to check. Two verifiers holding the same supplied set report the same set id; a verifier holding none reports verifier_policy_id byte-identically to every id issued before the table existed.
chain_ids(leaf) = the leaf's own chain record
chain_ids(composed) = { leaf_chains: the flat, deduplicated set of its DIRECT
children's chain records, canonically ordered }5.1. A composed child's set is already flat, so it never grows with depth and a parent reads only its direct children. It is O(distinct compilers), not O(evidence); this is not flattening.
5.2. leaf_chains is compared as a SET. Order is not part of the protocol.
5.3. A producer MUST NOT write its own chain. A producer that could would be naming the compiler its own proof was checked under.
Three phases, in this order.
6.1. RESOLVE. Walk references.operands from the root, resolving each cited root per TRVM-PROOF-WIRE-v1.md §3 into a snapshot the verifier owns. Every resource bound is decided here. When resolution completes, the store MUST NOT be consulted again.
each unique root is resolved once;
a root already on the current path is a cycle refusal;
for each edge, depth + 1 + height(child) MUST NOT exceed the depth bound (§6 of the wire spec);
resolution count, total resolved octets and per-node operand counts are all bounded, and both
claim.operands and references.operands are bounded before either is iterated.
6.2. JUDGE. Each distinct artifact in the snapshot is handed to the checker of its own protocol. A verifier MAY reuse a judgment it derived itself in this run; the verdict and the refusal set MUST be identical to recomputation.
6.2.1. The protocol→checker table belongs to the VERIFIER, never to the artifact. A verifier MAY extend the table in §3's child_protocols with protocols it does not implement natively, and MUST refuse a supplied entry that would REPLACE one it ships (nest-child-protocol-override-refused) or that is not the shape it holds (nest-child-protocol-registration-malformed). An artifact MUST NOT be able to name, carry or inject checker code: what the caller supplies is verifier configuration, read once and copied field by field, and a later mutation of the caller's object MUST reach nothing. When a table was supplied, the verdict MUST name the effective set — the built-in keys, the supplied (protocol, checker_id) pairs and a child_protocol_set_id over them — and the reported verifier_policy_id MUST fold that set id in. With no supplied table nothing is added and no identity moves.
6.3. WALK. For every operand:
exactly one reference names the same verified_claim_sem_id — the two planes are matched as SETS,
not by position;
the resolved artifact's certificate is recomputed and compared to the citation field by field,
because agreeing on a hash is not agreeing about what the hash names;
the child's verdict is VERIFIED.
Then: operands are pairwise distinct by certificate at this node (the same artifact reached by two different paths is the diamond and is what the protocol is for); nested_claim_sem_id, aggregate_id and structure_sem_id are recomputed; and every member of aggregate and structure is derived and compared.
6.4. There is no fourth category. Every member of every record is DERIVED (the checker computes the value itself), CHECKED (compared against a value the checker declares), or NON-SEMANTIC (nothing depends on it). A member that is hashed and read by nothing is not evidence — nested_verdict was exactly that, and an artifact stating of itself that it was REFUSED verified.
An implementation MUST use these codes. Conformance on negative vectors is compared as a SET; refusal precedence is not part of this protocol and MUST NOT be relied on.
nest-ingress-refused the artifact handed in has no canonical form
nest-protocol-mismatch not a nested composition
nest-vocabulary-unknown a member this checker's grammar does not have
nest-scope-mismatch scope is not the one this checker implements
nest-reference-contract-mismatch the transport contract is not this one
nest-connective-unsupported a connective this checker cannot evaluate
nest-operand-malformed an operand missing a field a citation needs
nest-operand-duplicated the same certificate cited twice at one node
nest-reference-mismatch references and operands do not name the same set
nest-artifact-root-malformed a citation that is not a well-formed root
nest-artifact-unresolvable the store has no octets under a cited root
nest-artifact-invalid-utf8 the octets are not valid UTF-8
nest-artifact-malformed the octets do not parse, or have no canonical form
nest-artifact-non-canonical the octets are not the canonical encoding of what they parse to
nest-artifact-root-mismatch the octets are not the artifact that was cited
nest-child-protocol-unsupported a child protocol with no checker here
nest-child-refused a child's OWN checker did not return VERIFIED
nest-certificate-stale the recomputed certificate id is not the one cited
nest-citation-cross-wired the id is right and the claim or aggregate it names is not
nest-chain-ids-mismatch the stored chain set is not the one the children give
nest-claim-id-mismatch nested_claim_sem_id is not over these operands
nest-count-inconsistent an aggregate member this checker derives otherwise
nest-structure-mismatch a structural member this checker derives otherwise
nest-depth-exceeded a citation chain past the policy ceiling
nest-budget-exceeded octets, resolutions or operands past the policy ceiling
nest-cycle a root cited by one of its own ancestors
nest-policy-weakened a caller asked for a policy looser than the shipped one
nest-child-protocol-override-refused
a supplied entry would REPLACE a checker the verifier ships
nest-child-protocol-registration-malformed
a supplied table, or one of its entries, is not the shape
the verifier holds
nest-checker-threw the checker raised instead of refusingnest-cycle is defence in depth and not load-bearing: sealing a cycle requires octets that hash to a root those octets already contain. That was not achieved in a bounded experiment of 512 attempted fixpoints; it is assumed computationally infeasible under the hash model and is not proved.
Not a new mathematical result. The conjunction is redundant by design.
Not that resolving an address establishes anything about the artifact.
Not a warrant cache. A verifier may reuse a judgment it derived itself, in this run, over a
snapshot it owns. Believing a verdict issued elsewhere, or one that outlived a run, is a different object and does not exist in this protocol.
Not unbounded. Every dimension an untrusted store controls is bounded by a policy the checker
owns and a caller may only tighten.
Not a claim about how many times anything was checked.
Not transitive in the sense of trust. A nested composition may cite another, and every artifact
in the graph is judged by its own protocol's checker regardless of depth.
Not a verdict independent of who checked it. A VERIFIED issued while a supplied child-protocol
table was in force is meaningful ONLY together with the verifier_policy_id and child_protocol_set_id reported beside it. A checker_id is a NAME, not a warrant: a supplied checker that answers VERIFIED to everything widens only what THAT verifier will hold, and says nothing about what any other verifier would. A consumer MUST NOT equate two verdicts because the token is the same string; verification without verifier identity is incomplete evidence.
These are named so an implementer does not assume they were forgotten:
Refusal precedence. Not decided. Compare sets.
Connectives other than CONJUNCTION. Not specified.
A persistent, verifier-issued warrant. Not specified, and §8 says why.
A generic checker-derived citation subject. verified_claim_sem_id is currently defined by the
certificate protocol and requires chain_ids; a composition's flattened leaf_chains is redundant for binding — a child certificate already propagates a compiler change into every ancestor's claim id — and load-bearing only for citability. The interface that would replace it is not specified here.
Full RFC 8785 conformance. The bundled corpus is not the reference suite.