Skip to content

Add Adversarial Execution Evidence predicate (v0.7) - #570

Open
astrogilda wants to merge 1 commit into
in-toto:mainfrom
astrogilda:predicate/adversarial-execution-evidence
Open

Add Adversarial Execution Evidence predicate (v0.7)#570
astrogilda wants to merge 1 commit into
in-toto:mainfrom
astrogilda:predicate/adversarial-execution-evidence

Conversation

@astrogilda

@astrogilda astrogilda commented Jul 15, 2026

Copy link
Copy Markdown

Adversarial Execution Evidence predicate

This adds a predicate for the evidence produced by deliberately executing an untrusted artifact against a known adversarial corpus inside a containment substrate: agent tools, MCP servers, plugins, build steps. The producer runs the artifact, injects the corpus, and signs what the substrate intercepted.

The predicate has been through fifteen rounds of review here, and @Rul1an has written a checker from the text alone and runs its conformance corpus, so the field shape is settled enough to read as written. They are the same reader in every reference below. I still want review of the fields before the vetting meeting. To answer the new-predicate guideline questions up front:

The use case is an admission controller gating a third-party MCP or agent image on evidence it was detonated against a named corpus under an enforcing catch policy, and an auditor re-verifying a specific interception offline without trusting the producer's infra. Existing predicates do not cover it: runtime-trace carries raw monitor activity with no corpus binding, no coverage denominator, and no per-event signature; SCAI carries attribute assertions, not an adversarial corpus with recomputable outcomes; VSA and SVR carry policy verdicts computed downstream of evidence like this. This is the evidence layer those consume, so verdict semantics stay out of scope here. The policy question it answers is which attacks this exact image faced, what the substrate did about each, and under what network posture. A consumer recomputes all of that from the attestation plus the producer's published taxonomy, with no call back to the producer.

The shape carries an explicit doesNotAssert negative scope, and five further design properties motivate it. I'm happy to defend or change any of them in review:

  • A recomputable result: a deterministic function of the carried evidence, which a consumer re-derives for itself instead of taking the producer's word for it.
  • An attack-granular coverage binding, where the coverage denominator is a digest-committed manifest mapping each class to its attack ids and carried in the attestation, so an edit to the assessed set changes corpus.digest.
  • Independently signed intercept records (DSSE-shaped, verify-then-read) under a single predicate-level batchRoot.
  • An I-JSON safe-integer profile on every rail, so canonicalization is byte-identical across languages.
  • A bounded producer extension surface. The aee member prefix is reserved for future versions of this predicate and everything else in an observation payload stays producer territory, but no member of that territory is read by a conforming verifier: a producer-defined member MUST NOT affect structural validity, MUST NOT affect result, and MUST NOT affect the evidence tier, whether or not its values can be ordered. A producer-defined ordered axis additionally MUST NOT be ranked by a verifier and MUST NOT be composed by weakest input across records or rows, because the two axes this predicate does order, basis and method, are ordered only because a normative reader consumes them, and a producer axis acquires no such reader by sharing the envelope. That constraint sits in the paragraph granting the territory, rather than beside each future member, so an implementer meets it before the member exists and not after the first one has shipped. The first version of this rule reached only ordered members. They applied it to their own tooling the day it published and reported two gaps: it missed their unordered producer members, and one of their checkers was gating validity on a producer member's value, which their own design document forbade. Both halves of the wording above come from that report.

One thing I'd specifically like the maintainers' read on: whether evidence that carries no verdict belongs as its own predicate or should be framed relative to SCAI.

We build monitors that would emit this downstream of runtime traces. For folks in #557 and #568 working on eBPF and CI monitors (@rung, @stupendoussuperpowers): this is designed to wrap and bound the outputs of a trace, and I'd value knowing whether your tools' trace-policy and scope outputs map cleanly onto observationEnvironment and the coverage sets.

Vetting status (v0.7, suiteRevision 25)

This pull request is at predicate version v0.7, and its head carries it. The conformance corpus is at suiteRevision 25, which is 250 vectors: 55 accept, 193 reject and 2 indeterminate. The indeterminate class is a third disposition rather than a rounding of the other two, and a statement lands there when the corpus declares that more than one conformant reading is available. aeeChainScope is an array a machine can compare, canonically sorted and free of duplicates, of registered dimension tokens with a two-sided equality gate that closes both scope-narrowing and coarse-side pooling. The whole statement is parsed as strict I-JSON; every string literal must be a well-formed sequence of Unicode scalar values checked on the raw bytes, which now excludes the Unicode noncharacters RFC 7493 §2.1 forbids; and JSON nesting is bounded normatively at 128 with its counting rule stated (the number of open containers, the outermost brace being depth 1). An arming payload may carry a read-first aeeBindingVersion; armedAt requires a zero UTC offset; an out-of-range observationRefs index is a fault on any row; duplicate attackId rows are malformed; the single-subject requirement holds on a statement of any basis; and the three coverage sets are a disjoint partition. Every interpretation decision is locked by a forcing vector under a CI-checked registry, and the spec says plainly that a reading no vector exercises is untested, not confirmed. Working in a different language from the published text, they have run this suite at six of its revisions, and not at the rest: there is no posted run for suiteRevisions 4, 7 through 21, or 23 through 25, so this pull request publishes no independent score at any of those. What they have posted is 125/125 blind at revision 1, 138/138 spec-diff-led at revision 2, 140/140 at revision 3 as a first run by an unchanged build whose reason-map rule predated the two new vectors, 149/149 at revision 5, 153/153 at suiteRevision 6 (2026-07-28, aee-checker#4), and at v0.7 and suiteRevision 22 a blind first run of 179/232 followed by a directed run of 232/232. The blind number is the informative one and it is not flattering. They partition the 53 first-run mismatches by the message their checker emitted: 42 on one run-binding derivation, 7 returning valid with no reason, and 4 answering pass_indirect where the corpus expects pass. That partition is by message and not by cause, and they state in their own report that attributing a recovery to a particular fix would need a bisection against the blind build, which is unrecoverable, so no causal residual follows from it. They also record that the blind build was never committed on its own, so the 179 is not independently reproducible and their index carries an explicit null digest saying so. Their run records and report for this revision are pinned at reports/v0.7-RUN.md, and our own implementation notes are in docs/IMPLEMENTATION-REPORT.md.

A protobuf definition ships with this revision, transport/codegen-only: its JSON output is never re-canonicalized for signing (proto3 ProtoJSON is not RFC 8785), since DSSE signs the body bytes verbatim.

Edited 2026-08-20 to correct the corpus counts: suiteRevision 25 is 250 vectors, 55 accept and 193 reject, and this description carried suiteRevision 24's 248, 54 and 192 against revision 25's name.

@Rul1an

Rul1an commented Jul 19, 2026

Copy link
Copy Markdown

Taking you up on the early-draft invitation. Mostly field-level, plus one gap I think this predicate is unusually exposed to.

observationEnvironment pins what the substrate was configured to do and coverage pins what was assessed. Neither pins where an observation came from. interceptRecords are signed by the substrate, but the signature binds emission rather than vantage: the record's content is producer-defined, so an egress_captured the substrate intercepted at the network boundary and one derived from the executed artifact's own stderr both verify identically.

That interacts badly with the property I like most in the draft. Because result is a deterministic function of the carried evidence, both of those recompute to the same fail, and the recompute is what gives a consumer confidence in the first place. It is also why the record signatures do not close this: interceptRecords is optional and the recompute reads containmentObserved, so a fail is reachable with no signed record at all. A self-reported observation that lands on fail through a correct recompute is worse than one that does not, because everything downstream now reads as checked.

This is not the coverage question from #557. catchPolicy and networkPosture do pin the substrate's configuration, but basis is per-observation rather than per-run: the same enforcing policy is compatible with a row the substrate saw and a row the artifact reported, and the recompute reads the row.

You have already drawn the distinction once. networkPosture is specified as the substrate-authoritative egress posture, which is a claim about vantage rather than about content. Generalizing that to the observations themselves would close the gap: a per-row basis on attackResults with a small closed vocabulary, along the lines of substrate_observed, artifact_reported, inferred, with unknown labels failing closed the way containmentObserved already does.

actualLayer is adjacent but answers a different question, and its clean-run behavior is not stated. It names which enforcement layer acted, so presumably nothing on a pass, which is the case where a consumer most wants to know whether anything was positioned to see. Worth pinning either way.

On your two questions, though you asked the maintainers and I would defer to them on the first. Verdict-free evidence reads as its own predicate rather than SCAI, since the recompute rule is normative here while SCAI leaves attribute and evidence formats to producer and consumer with no re-derivation requirement. On does_not_assert, I would just rename it. Your changelog says 0.1 to 0.2 were internal iterations, so the spec has no deployed readers to keep, and any old-name tolerance is your producer's migration concern rather than something the wire format has to carry. A permanent alias is the one option I would avoid, since two accepted spellings means two canonicalizations for the same content and you hold I-JSON discipline everywhere else.

I can send the three-value vocabulary as a suggested diff if you want it concrete.

@astrogilda

astrogilda commented Jul 19, 2026

Copy link
Copy Markdown
Author

You found the real hole. The recompute is the property I care most about, and you're right that it's exactly what makes the vantage gap dangerous. A fail derived from rows the artifact itself reported verifies and recomputes identically to one the substrate intercepted. And because the recompute is what buys confidence, everything downstream reads it as checked. interceptRecords being optional means the signatures never close it either; a fail is reachable with zero signed records, off containmentObserved alone. Self-reported observation that survives a correct recompute is worse than none, and I'm not going to argue with any part of that.

I've adopted your fix as proposed and pushed the revision, so what is below is the committed text itself. basis is now required on every attackResults row, with the closed three-value vocabulary: substrate_observed (the substrate saw the event at its own vantage, network boundary, syscall supervision, or VM introspection, independent of the artifact's cooperation), artifact_reported (derived from the artifact's own stdout/stderr, exit status, or self-emitted logs), and inferred (indirect derivation, say a post-hoc state diff). A missing basis, or any value outside those three, fails closed through the same mechanism as an out-of-vocabulary containmentObserved label. The row forces result to fail and can support nothing stronger, and the recompute rule now reads it directly. I did not let an unknown basis degrade to artifact_reported, since that would launder unknown vantage into a weaker but accepted claim, which is the same failure in a nicer suit. The spec also says the quiet part now. Consumers MUST be able to gate on basis, a fail supported only by artifact_reported rows SHOULD be treated as weaker than one carrying a substrate_observed row, and a consumer MAY reject it outright. That keeps the gating decision on the consumer side without the predicate ever carrying a policy verdict.

The actualLayer clean-run behavior is pinned too. On a clean row the producer MUST emit the literal none, explicit rather than omitted, so that "nothing needed to act" is distinguishable from an accidental omission. Your positioned-to-see question turned out to be the best argument for basis on clean rows as well: a clean row carrying substrate_observed states the substrate had vantage and observed nothing, which is the claim a pass actually rests on. That keeps actualLayer answering only which layer acted, and keeps vantage from being loaded onto it.

On the rename, agreed and done. Two accepted spellings means two canonicalizations for the same content, so no alias; the old spelling is rejected, and migrating old producer output is our producer's problem rather than the wire format's. The field is doesNotAssert, and since a rejected spelling is a breaking wire change I bumped the predicate to v0.4 (Type URI and Version both), with all three of these changes in the changelog entry.

On SCAI, same read for the same reason: the normative recompute rule is what makes this its own predicate, since SCAI deliberately leaves attribute and evidence formats to producer and consumer with no re-derivation requirement. The call stays with the maintainers, but a second reviewer landing on own-predicate off the recompute rule is the strongest version of the argument I could bring to vetting.

The suggested diff is the smaller half of your offer, and I'd take the stronger version. The vocabulary is committed text now, and what I want from you is the read you gave the recompute, aimed at the observation that fits none of the three cleanly. The seam I'd probe is between substrate_observed and inferred: a substrate-adjacent monitor with real vantage that isn't the enforcing substrate itself. If that deserves a fourth value, now is the time, while there are still no deployed readers to keep.

Edited 2026-08-31: prose only, for readability. No field name, vocabulary value, version or claim changed.

@Rul1an

Rul1an commented Jul 20, 2026

Copy link
Copy Markdown

Read it the way you asked, against the recompute rather than the prose, and the three values hold up better than the seam you flagged. Let me take that seam first, then hand you a sharper one.

The substrate-adjacent monitor does not want a fourth value, because what separates it from the enforcing substrate is enforcement role, not basis. A passive tap that saw an egress at the network boundary and the inline gate that intercepted the same egress make the identical claim on that row: each observed the event at its own vantage, independent of whether the artifact cooperated. What differs is that one was positioned to act and the other only to watch, which is an enforcement-role fact rather than a basis one, and whether anything acted is the separate question actualLayer answers. This works only if substrate_observed names a class of vantage, cooperation-independence, rather than the identity of the enforcing substrate. Under the identity reading your seam is real and wider than one monitor: the adversarial corpus endpoint that logs the inbound connection it received is neither the enforcing substrate nor the artifact, yet plainly not artifact_reported. But the fix for that is to sharpen substrate_observed to name the vantage class, since the corpus endpoint and the enforcing substrate sit at the same basis and differ only in who, if anyone, could act. Either way, no fourth value: adjacency is a fact about enforcement role, which basis does not and should not measure, not about the cooperation-independence that separates substrate_observed from artifact_reported.

The seam I would actually probe runs inside a single value rather than between two, and it passes through one of your own substrate_observed examples. Take VM introspection. A trap on a write catches the event as it happens, but a snapshot-to-snapshot memory diff has the same independent vantage, the guest cannot forge the hypervisor's read, and yet it is a reconstruction across the semantic gap rather than a caught event, so it can miss a transient raised and undone between the two snapshots. VM introspection therefore splits by directness while staying substrate_observed, and the same physical evidence can land elsewhere too: a state diff parsed from the artifact's own logs is inferred and not independent at all. inferred therefore says nothing about vantage, which is the one thing basis most needs to preserve.

That matters for the recompute for the same reason unknown basis did. You refused to let an unknown vantage launder down into artifact_reported, since it would buy a weaker but accepted claim. The symmetric leak is upward: unless the independence of an inference's inputs is itself stated, a reconstruction built on the artifact's own testimony reads as if it carried substrate vantage. The cheap version, while there are no deployed readers to keep, is one line: a fail supported only by inferred rows reads no stronger than one supported only by artifact_reported, and if you want a reconstruction from independent inputs to count for more, the independence of those inputs has to travel the way you made basis itself travel.

Everything else in the revision reads clean. basis required with the closed vocabulary and fail-closed on unknown, the gating language moved onto the consumer without the predicate holding a verdict, actualLayer pinned to literal none on clean rows, and basis kept on clean rows so a pass states the vantage it rests on, all land where I hoped. Rejecting the old spelling rather than aliasing it is the right I-JSON call, and the v0.4 bump is the right breaking-change signal for it. Glad to be second reviewer at vetting time, holding an author's own predicate to the recompute rather than the prose, if that helps carry it.

@astrogilda

astrogilda commented Jul 21, 2026

Copy link
Copy Markdown
Author

Both halves taken. Your vantage class reading is now the definition itself: in the new text substrate names cooperation independence, and your corpus endpoint sits next to the tap and the inline gate as the worked instance of same basis, different enforcement role. The seam inside substrate_observed was worse than you stated it, too, because my own examples already instantiated it. VM introspection sat under substrate_observed. Post-hoc state diff sat under inferred. A hypervisor snapshot diff is both at once, so two values claimed the same evidence, and the closing question from my last reply got the answer it deserved: the hunt for a value that fits none of the three fails because the three values were two axes fused into one vocabulary, vantage and how the observation was made.

I did not take your cheap fix, for a structural reason rather than taste. A flat "inferred reads no stronger than artifact_reported" binds only the producer who volunteered the weaker label, and with my examples ambiguous the same snapshot diff pipeline could defensibly label substrate_observed, so the line would have penalized the honest producer without constraining anyone else. Your strong version is the one that holds: the independence of an inference's inputs has to travel. The revision at def32f0 does that literally. basis collapses to two values, substrate and artifact, defined as the vantage of the claim's weakest input, with a stated criterion for what counts as artifact-sourced: a channel the artifact can populate arbitrarily without performing the claimed event. Testimony about an event, versus the event itself. That is why an egress capture does not inherit artifact even though the artifact authored the packet bytes, and why its stdout always does. inferred is deleted with no successor, and your two state diffs land at (substrate, reconstructed) and (artifact, reconstructed). The weakest-input rule is your half of this design, written down.

The directness axis is my extension. It has to live on the wire rather than in producer vocabulary for the same reason basis did: the recompute and the documented gating on the pass side read it, and transient tolerance cannot be gated fail-closed across producers on open per-producer labels. method is intercepted or reconstructed, required, closed, fail-closed, and it composes the same way basis does. A claim inherits reconstructed from any input derived from state after the fact, while decoding a channel that was armed before the event does not demote a row. Attribution strength stays in the producer's containmentObserved vocabulary on purpose, since nothing normative reads it; that boundary is unchanged from 0.4.

Your transient example also bites hardest where you did not press: on pass. The ordering is two-sided now. While basis bounds a fail over a defined supporting set, method bounds a pass, with (substrate, intercepted) clean rows as the strongest absence claim the predicate can carry and any reconstructed clean row read as tolerating transients between the observed states. Rows fail-closed on either field sit at the bottom of both orderings, which is where a row with unknown vantage belongs.

One more change completes your own no-fourth-value argument. You delegated enforcement role to actualLayer, but 0.4 gave your passive tap nowhere to land, since a caught row where nothing acted was undefined. actualLayer is now required on every row, and none is valid on a caught row, where it states the event was observed and no layer acted, which is the enforcement role fact your argument needed a home for.

Mechanics: the three 0.4 spellings are rejected with no alias, same protocol as the does_not_assert rename, licensed by zero deployed readers. I resisted a third axis (confidence, attribution) as territory for producer vocabulary. Naming is open. If the maintainers prefer observationMethod or directness over method, that is a cheap rename before vetting and their call. The proto lands once the field shape settles, as the PR body says.

The main thing I want your read on is whether the weakest-input rule and the artifact-sourcing criterion close the upward leak you named. Beyond that, check me on where the method/attribution line sits, and on whether a caught-row none covers your passive tap the way you meant it. Yes to second reviewer at vetting.

Edited 2026-08-31: formatting only. A few repeated field names lost their backticks after their first mention; no name, value, commit or claim changed.

@astrogilda
astrogilda force-pushed the predicate/adversarial-execution-evidence branch from 92424ac to 4133b14 Compare July 21, 2026 05:36
@Rul1an

Rul1an commented Jul 21, 2026

Copy link
Copy Markdown

That is the right cut, and the reason the hunt failed is as you put it: three values were carrying two questions, so no single value could fit an observation that varied on both. Weakest-input over vantage and directness is the composition that makes the two axes independent again, and the artifact-sourcing criterion, a channel the artifact can populate without performing the claimed event, is the sharp version of what I was reaching for with testimony. Egress-capture-is-substrate-because-the-packet-had-to-be-sent is the case that proves the criterion carries its weight.

On your main question, the weakest-input rule closes the leak I named, but only for a producer telling the truth about its inputs, and that deserves being exact about because it is the same shape as the gap I opened first. basis and method are still labels the producer writes and the recompute reads, not facts the recompute derives from carried evidence. A pipeline reporting everything off the artifact's own testimony can still stamp substrate on every fail row and mint the strongest fail you can carry, with no substrate anywhere in the loop. Weakest-input disciplines the honest producer, whose weakest input drags the row down. It does not bind the one who simply labels the row substrate, and the strongest claim staying self-certifiable is exactly the hole from my first comment: interceptRecords optional, the recompute reading a producer field, a fail reachable with zero signed records.

The close is to make the strong label cost the one thing a self-reporter does not have. A row may carry basis substrate only if a substrate-signed interceptRecord covers that observation; absent it the row cannot claim substrate and fails closed toward artifact. interceptRecords stays optional in general, artifact rows never needed a signature, but substrate becomes the value you cannot assert without the substrate's own signature over the row. That makes basis substrate a claim the substrate signed over the row rather than one the producer asserts, so asserting it now requires the substrate's own key, which a pure self-reporter does not hold. It relocates the trust root from the producer to the substrate rather than dissolving it, which is where substrate vantage should cost, and it composes with weakest-input unchanged: an input lacking substrate backing is just another weakest input that caps the row. If the signed record also states how it observed, intercepted or reconstructed, then method for substrate rows rides that signature too, so the strongest value on each axis rests on the substrate rather than the producer, substrate on the fail side and intercepted on the pass side. method on artifact rows can stay a declared label, since artifact has already capped what that row supports.

On the passive tap, yes, and making actualLayer required on every row is what closes it. A tap that saw an egress it could not block lands at substrate, intercepted, actualLayer none, contained false, and that reads correctly as a strong fail: an independent vantage watched the thing happen and nothing stopped it. none on a caught row was the missing home for the enforcement-role fact I split off, so requiring it everywhere rather than leaving it undefined is the right completion of the argument against adding another value, not a new question.

On where the method and attribution line sits, I think you have it right: method is a fact about the observation, how directly it was made, while attribution is a fact about the mapping from an observation to a named attack class, and those vary independently. The one thing I would check is that containmentObserved is not now carrying both. It holds the containment bit the recompute reads, which is normative, and, as I read the revision, attribution strength now also lives in its vocabulary as non-normative nuance. A single field with a gated meaning and an ungated one beside it is the overload we just spent two rounds pulling out of basis and actualLayer, so it is worth confirming the recompute reads only the containment bit and nothing downstream leans on the attribution nuance to move a result.

Yes to second reviewer at vetting. On naming, method or observationMethod or directness all read fine and it is the maintainers' call; the shape underneath, two required closed axes with weakest-input composition and a two-sided ordering, is the thing I would freeze.

@astrogilda
astrogilda force-pushed the predicate/adversarial-execution-evidence branch from 4133b14 to def32f0 Compare July 21, 2026 13:09
@astrogilda

astrogilda commented Jul 21, 2026

Copy link
Copy Markdown
Author

Both halves of the gate taken. I want to lead with the two places my first pass would have overclaimed, because you would have caught them on the first read and I would rather retire them myself. The revision at b5acaa5 is v0.6; as before, this reply lands after the push so you are reading committed text.

The first place is the one you care most about, the recompute. My instinct was to add the coverage gate as a second object every consumer derives beside result, and leave that member itself reading basis as a raw label. That is your round-three hole wearing a MUST-derive obligation. A consumer that reads result and skips the object is exactly as deceived as under v0.5. So I split the gate by what it actually depends on. Four of its steps are pure functions of the carried bytes, with no key and no policy in them: the references resolve and are in range and class-match the row's method; every covering payload is canonical and carries the reserved members with a run binding equal to the one the verifier derives; the row's method does not exceed the weakest signed method across its covering records; and the batchRoot recomputes. Those four are now VALIDITY requirements, at the same altitude as a missing actualLayer. I made them consumption preconditions in so many words: a consumer that consumes result or credits any row must evaluate them first, and on failure the attestation is invalid and the result must not be consumed. I am being pedantic about that sentence because a gate nobody is required to run is not a gate, and the result-only consumer you constructed is bound only if reaching it is defined to go through the gate. Only the fifth step is genuinely trust relative, whether the covering signatures verify against a key you name as a substrate key. That one stays a per-row derived tier, because a validity rule that varied with your trust anchors would break the recompute we have argued everything against. So the recompute is still pure, but a valid attestation can no longer carry a strong substrate row whose coverage is dangling, class-mismatched, cross-run spliced, or unrooted. While making that claim honest I had to fix one more purity leak you had not called yet. Caught versus clean used to be decided by my published vocabulary, a document that does not travel, which would have made validity a function of something I could edit after signing. The vocabulary and its caught subset now ride in the attestation, digest-pinned the same way the corpus manifest already was, so the classification is carried bytes too and an archived attestation stays verifiable if my documentation moves or I disappear.

The second place is the single-key topology, and here I have to concede the frame before I describe the mechanism, because your read falsifies the confident version in two lines. In the deployment we actually ship, the substrate signer and the assembly signer are the same key held by the same operator. Under that key the tier does not defeat a pipeline with no substrate in the loop. An operator holding the key can hand-author an arming record with the right derived run binding and a valid signature without any substrate ever running, and every clean row it points at derives attested. A signature proves key possession, and nothing about it proves a substrate executed. So the named attacker, the self-certified strongest pass and strongest fail, is closed only where the substrate observation key is held apart from the assembly plane, which is a SHOULD we do not yet ship. What the tier buys under one key is smaller and real. Against a party that does not hold a substrate key, a downstream tamperer, it still binds every record to this run so a foreign-run record cannot be spliced in, still commits the whole record set under batchRoot so nothing can be dropped, and still pins method to what the substrate signed. I have graded the threat-model list accordingly, and the trust-boundary section now reads as a field partition with a key floor, where it used to read as a triumphant walkthrough. Walk your artifact-testimony pipeline through the gate and the defeat holds only where the pipeline does not hold a key you name as a substrate key, a precondition that now lives in the sentence itself and no longer 20 lines below it.

Now the mechanism, with those two retractions in view. Your rule keys on a substrate-signed record covering the observation, and your pass-side sentence wants intercepted on the pass side resting on the substrate too. Each collides with a line I had already committed, that a clean row's interception has nothing to sign. So the pass side needed the instrument your sentence presupposes without naming. It also needed a second record, because a single arming record proves the vantage was armed at t0 and nothing more, and a vantage dropped one tick after arming would satisfy the strongest pass claim. That is your own "a missing signal is not a clean one" reintroduced on the pass side. So in v0.6 interceptRecords becomes observationRecords and admits, beside per-event interception records, a run-level arming record and a run-level sealed record. The arming record says a live vantage was armed before injection and pins the posture digest it was armed under. The sealed record says the vantage stayed armed to run-end, and its signed payload carries a still-armed flag, a run-wide count of dropped observations, and the posture digest in effect at run-end. The covering rule is normative and byte-checkable: a sealed record covers no clean row unless the flag is true, the drop count is zero or within a bound the same signed payload declares, and the posture digest equals the arming record's and the pinned one. A clean intercepted row is valid only with the pair. That closes arm-then-drop, silent buffer overflow, and a mid-run posture flip in one instrument. I kept the members semantic on purpose, armed, stayed armed, nothing dropped, posture unchanged, so how a substrate establishes them, a checkpoint chain, a sequence counter, a watchdog, stays producer territory and a substrate with a different mechanism can still comply. I made the drop accounting run-wide, because a per-class rule would need a verifiable mapping from a row to a class inside the seal, and no such mapping exists in carried bytes. A run-wide zero is checkable; a per-class zero would have been the same unverifiable "covers that observation" you objected to, one level down. I am also being deliberate about what even the pair proves: a vantage was armed and stayed armed and the committed set attributes no interception to this attack, which is not the same as no interception having occurred, and because the records are run-wide it is not a claim that this row's specific channel was armed. One more bound belongs on the table now, before someone discovers it later. The attestation speaks for the run it carries, never for a run population. Nothing in this predicate proves I did not run the corpus five times and publish the run I liked. Closing that gap needs a run ledger or a monotonic counter, which is a consumer or policy concern and sits outside the predicate by design.

Making "covers that observation" verifier-checkable meant closing three gaps I had left open in the first pass. The record content is producer-defined, so I had to say what a verifier is allowed to assume it can parse: any record covering a substrate row MUST be a canonical RFC 8785 plus RFC 7493 object whose media type ends in +json, with the reserved members at top level, else it covers nothing. Without that a producer with duplicate aeeMethod keys could make my parser and the signer's canonicalizer disagree, and method inflation would walk back in inside the signature. The record signature is DSSE PAE over payloadType and payload, stated as such, so that member is signature-bound. Then the run binding. My first pass bound five static config digests, which means two runs of the same image under the same policy derive the SAME binding, so a genuine record replays across identical-config runs. I had listed cross-run replay as closed, which is false. It is closed cross-config, not cross-run. v0.6 folds a run-start value the substrate emits into the binding and into the arming signature, so identical-config re-runs derive distinct bindings. The field is called runEntropy, and the name is deliberate: it is not freshness. The binding carries no verifier nonce, these attestations are published rather than challenged, so it is anti-splice, not anti-forge. Replay of a genuine record into a later identical-config run is bounded by a consumer that rejects reuse of a runEntropy value it has seen, not closed outright, and I say so in the text and in the threat model. I cited the CCA composite-token shape for the binding, and I should have flagged that CCA also carries a nonce for freshness that I do not; the binding axis is the only axis where the precedent holds. I also versioned the binding construction itself, a literal inside the pre-image, so if a later version has to change the inputs or the hash the old records stay distinguishable and are not orphaned, and a verifier rejects a construction it does not implement and never guesses between two. And batchRoot was undefined as a tree but I now require the consumer to recompute it. So I pinned it to RFC 6962 with domain-separated leaves and nodes, leaf order matching the array, byte-identical duplicate records rejected, and the tree built by the RFC's own split rule, never by padding the last node, which is the classic implementation divergence in this construction. The mismatch-invalidates rule moved into the batchRoot definition where it belongs; in the tier list it was a category error.

On the reserved members themselves, I would still call them binding structure rather than observation semantics, and I have kept the substrate's own vocabulary out of the wire. It remains the design's most novel joint and I would rather defend it with you now than at vetting: no vetted predicate reaches into a producer-defined payload with reserved members. The alternative I rejected was a producer-declared pointer map telling the verifier where to look and how to decode, because it hands the join back to the party the gate is aimed at. I also dropped the hard exclusivity rule I floated, that an interception index binds one row, because you would have built the counterexample yourself. One captured TLS flow can genuinely carry two exfil payloads for two attacks, and forcing two records over identical bytes manufactures ambiguity. Instead a shared index is allowed when the committed payload evidences each attack, and a row may carry an optional selector member naming the sub-observation it rests on, parallel to its references, with the token content staying producer vocabulary that nothing normative reads. The anti-double-attribution work is carried by the run binding, the batchRoot, and the row's own label. For future evidence shapes I put one forward rule in now: a record whose kind a consumer does not recognize covers nothing and is otherwise ignored, so a later minor version can add a kind, say a TEE quote over the vantage, without old verifiers either breaking or silently crediting it.

On containmentObserved, you were right that one namespace carried a gated meaning and an ungated one. The recompute reads exactly one property, membership in the carried caught set, with out-of-vocabulary fail-closed, and nothing else, not either ordering and not the new gate. I did not split the label set or add an attribution member, and I owe you the reason it is prose discipline here when it was a structural split for basis. The criterion is that an axis earns its own required member exactly when a normative reader consumes it. The recompute reads basis, so basis had to become a member. Nothing normative reads attribution strength or the clean-row window-bleed tolerance, so they stay producer vocabulary under a one-read rule stated at the label's own definition. If you can name any consumer rule, ordering, or gating step that reads the attribution nuance, that criterion says we split it, and I want the example.

As an I-JSON reviewer you would have flagged two smaller completeness gaps, and both are fixed. The run binding pins subject[0].digest.sha256, which is undefined for a multi-subject statement or a subject without a sha256 digest. So v0.6 requires exactly one subject and a lowercase 64-hex sha256 on all six inputs, malformed otherwise, taken verbatim with no case-folding, and the requirement is scoped to statements that carry a substrate row, so a purely artifact-basis attestation does not have to invent an entropy value it has no substrate to emit. And a caught intercepted row with empty references was my only hard validity gate, which a producer dodged by writing any non-empty index. The validity requirement is now that the references resolve and are in range, not merely that the array is non-empty.

The passive-tap reading you traced is untouched, and the frozen shape is untouched: two required closed axes, weakest-input on each, two-sided ordering. The tier is a derived object like result, and the validity half is a parse rule like actualLayer, so neither is a third axis.

Mechanics: version and Type URI move to v0.6 under the meaning-change rule, which the framework's 0.x versioning licenses; the renames are rejections, not aliases. Proto still waits for the shape to settle. observationRecords against evidenceRecords, the reserved-member prefix, and for that matter the tier names themselves, attested in a framework where everything is an attestation invites sentences like "this attestation's rows are unattested", are the maintainers' bikeshed, and I will take their spelling.

Before the freeze I would point you at three seams. The reserved members, per the flag above, are the load-bearing joint; an adversarial producer laundering through them, or a vetted-precedent objection I have underweighted, is where I most expect to be wrong. The runEntropy bound is the second, and I have deliberately left identical-config replay as a stateful-consumer problem rather than a closed one; if a published-attestation predicate can do better without a challenge protocol, tell me how. Third is the run-population bound, where the predicate now says plainly that it attests the run it carries and not the absence of other runs. I would genuinely like to be wrong that no single-attestation format can bind a run population. The second-reviewer offer stands taken on my side.

Edited 2026-08-31: prose only, for readability. No claim, figure, field name or version changed; a few repeat field mentions lost their backticks and nothing else.

astrogilda added a commit to astrogilda/agent-evidence-vectors that referenced this pull request Jul 22, 2026
The source cites spec:NNN line numbers against a specification file that was not
present in the repo (only the JSON schema shipped), so a public reader following a
reference hit a dead path. Vendor a byte-verbatim copy of the v0.6 predicate spec
(tracking in-toto/attestation#570 at b5acaa5) so the repo is self-contained and the
line references resolve. A spec/README records the pin and that the in-toto catalog
namespace, not this repo, is the canonical authority.

Signed-off-by: Sankalp Gilda <sankalp.gilda@gmail.com>
@Rul1an

Rul1an commented Jul 22, 2026

Copy link
Copy Markdown

I have been through v0.6 in full at 484bbe0. The two retractions are the right calls and I will not relitigate them; the four byte-pure validity steps as consumption preconditions, with signature verification as the one trust-relative tier, is the correct partition and it closes the result-only consumer cleanly. Taking your three seams in order, leading with the one where you most expect to be wrong, because I think you are half right about it.

Reserved members. The vetting objection has a better answer than the text currently gives itself, and the joint has one real crack.

The precedent first. "No vetted predicate reaches into a producer-defined payload with reserved members" undersells your own lineage. RFC 7519 does exactly this: a JWT claims set is producer-defined, yet verifiers read registered claim names (exp, aud, iss) from inside it, with collision resistance by registration and prefixing. RFC 6839's +json suffix is the vetted license to parse a media type you do not otherwise know. OCI annotations reserve the org.opencontainers.* prefix inside an otherwise free-form map, and the in-toto Statement itself reserves _type inside a JSON object. Your aee prefix plus +json requirement is the JWT registered-claims pattern wearing DSSE, and I would defend it at vetting in those words.

The crack is in the canonicality gate, and it is an adversarial-producer path. A covering payload MUST be canonical per RFC 8785, and a verifier checks that by re-serializing the parsed object and comparing bytes, or by an equivalent sortedness walk. JCS sorts members by UTF-16 code units; most naive re-serializers sort by code points. Those orders diverge when a member name outside the BMP meets one in U+E000 through U+FFFF: a surrogate-led name sorts first under JCS and last under code points. A producer can mint a payload whose bytes are canonical under one reading and not the other, and the two verifiers then split on "covers" versus "covers nothing", which under your validity gate is attestation-valid versus attestation-invalid on identical bytes. You already close the number half of this with the RFC 7493 safe-integer profile, there so that every rail derives identical bytes; the same clause wants a string half. Cheapest fix: require member names in covering payloads to be BMP-only (ASCII would also do, and your reserved members already are), at which point UTF-16 and code-point order coincide and the divergence is unconstructible. The alternative, mandating a true UTF-16-sorting re-serializer in every verifier, puts the burden on the many rather than the one.

runEntropy. I cannot give you challenge-free replay exclusion without state, and I do not believe anyone can: stateless deduplication against a global set is a global view, which is what logs are for. What I can offer is an upgrade to the bound you already have. Your text says the pre-image is the substrate's run-start checkpoint "or beacon head", and I would promote that aside to a SHOULD: make the pre-image include a publicly datable value, a drand round or an epoch ID in the RFC 9334 section 10.3 sense, with the round reference recoverable by the consumer (carrying it in the arming payload as producer vocabulary suffices, since the digest binds it). That buys two things at no new wire members. The arming record gains a proven floor, since a signature over a beacon value cannot predate the beacon round; issuedAt stays the asserted ceiling, and I am deliberately not calling that pair a two-sided proof, by your own asserted-versus-attested rule. And your consumer-side reuse rule gains comparability: two consumers rejecting runEntropy reuse can order the runs they have each seen against public rounds instead of against the producer's clock. The residual, replay visible only to a consumer who has seen the value before, stays a stateful concern, and the text already says so honestly.

Run population. You are right, and there is a strengthening that does not pretend otherwise. No self-contained attestation can prove the absence of sibling runs; that is the split-view problem, and fork consistency is the known ceiling for it. But your own design already holds the answer one level down: the sealed record's run-wide drop count and the checkpoint chain's each-interception-carries-a-higher-sequence rule make observation loss gap-evident inside a run, and the identical construction lifts to runs. One reserved pair inside the arming record's signed payload, a monotonic run sequence number and the previous run's binding digest under the same substrate key, makes cherry-picking gap-evident across whatever does get published: a skipped run is a numeric gap, a suppressed-and-rerun is a fork, two attestations sharing a predecessor. TUF's snapshot role is the vetted precedent for signing a population, and SCITT registration (RFC 9943, with COSE receipts per RFC 9942, both published last month) is the consumer-side completion that turns gap-evidence into third-party auditability. So the predicate's line that this is "a claim about the run this attestation carries, never about a run population" stays true, while cherry-picking moves from "outside by design" to "detectable across the published set", which I think is the most a single-attestation format can honestly buy.

On containmentObserved, your criterion survives my search for a counterexample: I cannot name a normative reader of attribution strength today. The nearest miss is the shared-selector allowance, "a shared index is allowed when the committed payload evidences each attack", where "evidences" is currently unadjudicated producer territory. If a future version ever makes that clause checkable, that is the moment the attribution member is born, by your own rule, and I am content to leave it as the tripwire.

One offer, since the validity gate is now four pure functions of carried bytes: when you mint conformance vectors for v0.6, I will write the validity-gate checker from the spec text alone, same discipline as the testigo cross, and we will find out whether these sections determine a unique implementation the way we have been arguing they should.

@astrogilda

astrogilda commented Jul 23, 2026

Copy link
Copy Markdown
Author

Thank you for this, it's the kind of review that genuinely makes the spec better :) I've taken all six points, five into committed text and one as an acceptance with a question attached. As before, I'm replying after the push, so everything below is committed text and not intent, landed as a commit series ending at the branch head.

On reserved members, I've turned your precedent framing into the spec's own defense. I added an informative note at the reserved-member definition citing RFC 7519 registered claims, OCI prefix reservation, and the structured-syntax suffix license from RFC 6839, and I mark it as locating the pattern rather than importing any cited standard's rules. One step further along your own argument, EAT (RFC 9711) is the domain-tightest instance, registered claims inside an attestation token, in the RATS family this predicate already leans on. The in-toto Statement itself reads a reserved _type out of a JSON object everyone else populates freely. I also state the two places I deliberately part from the JWT lineage, because the counter you would raise at vetting is that JWT ignores unknown claims. Here I make a colliding or unrecognized aee-prefixed member fail-closed, so it can only weaken coverage and never create it, and I make verify-then-read normative, which closes the parse-before-verify class of deployment mistake that lineage is known for.

You're right that the canonicality crack is real, I've adopted the fix, and it reaches further than the surface you named. Folding your fix, I swept the sortedness clauses and found the identical split live between my own rails one clause over. The labels and caught arrays said "sorted ascending" with the order undefined; my TypeScript rail and the Go reference compared UTF-16 code units, while my standalone Python verifier compared code points. I proved it executably: set a supplementary-plane string against one in U+E000 through U+FFFF and they order oppositely, so the same bytes read attestation-valid on two rails and attestation-invalid on a third. My committed fix does both halves. I pinned the sort to UTF-16 code-unit order explicitly, and I promoted BMP-only from producer hygiene to a verifier rejection obligation on every signed canonical surface, meaning member names and both vocabulary arrays. I upgraded it to a reject deliberately, because hygiene still lets an adversarial producer mint payloads that split a code-point verifier from a UTF-16 verifier, whereas the reject makes the divergence unconstructible for every conforming implementation, which is the property your fix was after. That leaves one honest consequence for the vectors you will check against. Once I enforce BMP-only I cannot construct an accept-side probe for the sort order, because inside the BMP the two orders coincide, which is the whole point. So I carry only the reject side, a supplementary-plane member name and a supplementary-plane vocabulary entry, and I pin the comparator regression in per-rail unit tests, the one layer where it stays expressible.

On runEntropy, I adopted your idea with credit, as a SHOULD, and I added three sharpenings to keep the floor honest. The folded value must be unpredictable before its round, or the floor is fake. It has to augment and never replace the substrate-unique run-start component, or the anti-splice property collapses into whatever the beacon publishes. And I require it fetched at arming time with the round reference recoverable from the arming payload, because the producer selects the round, so an uncoupled or cached round proves age rather than recency and the floor bounds freshness only where consumer policy couples the round to its window. I say plainly in the text what this guarantees and what it does not: a proven floor, an asserted ceiling, deliberately not a two-sided proof, and no floor at all against a producer whose beacon sits inside its own trust domain. Your comparability point survives all three qualifications and I kept it in, since public rounds give independent consumers a shared time axis for reuse observations.

On run population, you're right that the construction lifts, and I carried it into the committed text as the three optional arming members. Two are yours, the run sequence number and the previous-run binding. The third your sketch did not have: I made chain scope a required member whenever the sequence is present. Without a declared scope every rule over the pair goes vacuous, because a producer that chooses its population freely makes any gap uninterpretable, and the obvious default of one global per-key counter leaks the producer's total run volume across customers, so I recommend a minimum of substrate key by subject. I close two more edges. I treat two genesis records under one key and scope as equivocation of the same grade as a shared predecessor, because otherwise the cherry-picker's cheapest move is a chain reset where every winner is sequence one. And I keep the claim language ordering-only, because nothing on the wire anchors when an arming record was signed relative to the run's outcome, so I claim commit-before-outcome only in combination with the beacon floor above or an external registration receipt. I state a numeric gap as unexplained absence and never as fraud evidence, since crashed and private runs produce gaps innocently; what the pair buys is demand-disclosure, where a consumer policy may require a contiguous, fork-free chain over the runs offered to it, fork consistency being the ceiling, as you said. I pulled RFC 9943 and RFC 9942 from the editor and read them before citing; I cite them as the registration completion, with TUF's snapshot role as precedent for the concept of signing a population, and not for this mechanism. If the recommended-minimum scope granularity strikes you as wrong in either direction, that is the one member of the trio I would most value a second reading on.

On containmentObserved, your null search stands and I've written the tripwire down. I put it in the changelog as versioning discipline, not in the member paragraph, so it binds future versions instead of decorating this one: a member is born exactly when a normative reader consumes it. Your near-miss was nearer than you called it. The shared-selector allowance as I had committed it wore the gate verb, "covers each referencing row only where its committed payload evidences each referenced attack," an unevaluable condition I had left sitting inside the section whose headline is coverage as pure byte functions. Your from-spec checker would have had to pick a reading there. So I reclassified it. I now say a producer MUST NOT reference a record from a row its payload does not evidence, stated as a producer obligation outside every gate, and I say explicitly that no validity requirement, recompute input, or tier evaluation reads it and that selector presence changes no gate outcome.

Thank you for offering to build the checker, and yes, I'd love that! Here's what you can hold me to: the suite is deterministic, 34 accept and 91 reject vectors as of this revision's additions, every vector a bare Statement with test keys you can derive from a published seed formula, and per-vector traceability from condition to spec line. So that the experiment stays honest, I declare in the manifest that the verdict, and each accept's result token, is the normative comparison surface and that the per-vector condition codes are informative, since the code set is my implementation's vocabulary and pinning it would rig the uniqueness question. And I numbered the validity steps in the spec, because your "four" against the text's five bullets was two careful readers counting differently, which is itself a legibility datum. I read your four as the byte-pure pipeline partition, statement well-formedness, coverage validity, the recompute, and digest integrity, with the tier excluded as the one trust-relative stage; confirm that is the scope you intend to implement. My one ask is that you have your checker report a free-form reason per reject alongside the boolean, mapped to my codes only informatively. Verdict-only scoring would let a wrong-reason reject score as parity on most of the corpus, and I care about the divergences where two implementations reject the same vector for different reasons, which are the actual product of the exercise. And a gist would be the wrong home for it: land the checker in or alongside the suite under your own authorship when it exists, since a two-independent-authors record is worth more durably than a comment thread. It's public now, Apache-2.0, at github.com/astrogilda/aee-conformance, with a MANIFEST enumerating each vector's expected verdict and result, the Go reference verifier, a standalone Python rail, and a harness that replays the whole corpus. That is the place to land it; the vectors and the spec text above are committed there and on the branch head.

On the verification story you reviewed, one more committed change. I now state the anchors a consumer pins, the expected corpus and substrate digests, as explicit consumer-policy obligations with a single conjoined admission result, and I keep them deliberately outside the byte-pure gates: validity holds identically for every consumer, and which corpus you meant to assess against does not.

Thanks again for the care in this round. The two things I'd most value your read on are the validity-stage scope you intend to implement and whether the chain-scope granularity lands right, but honestly the whole pass has been a pleasure to work through.

Edited 2026-08-31: prose only, for readability. No figure, vector count, citation or claim changed.

@Rul1an

Rul1an commented Jul 24, 2026

Copy link
Copy Markdown

Scope confirmed as you numbered it: the checker implements the four byte-pure stages, statement well-formedness, coverage validity, the recompute, and digest integrity, from the spec text at the branch head, with the signature tier excluded from the parity claim. One boundary note so the corpus and the claim line up cleanly. Where a reject vector is reachable only through the tier, I will still run the DSSE verification against the seed-derived test keys, because a test corpus pins its anchors and pinned anchors make the tier deterministic; the trust-relativity lives in anchor choice, and for the vectors the manifest has already chosen. So the parity claim is stages one through four from spec text alone, with the tier exercised under the corpus's own keys rather than reimplemented as policy. Reason-per-reject is the right experimental design and I would have asked for it if you had not: verdict-only scoring lets a wrong-reason reject pass as agreement, and the divergences are the product. On where it lands, I am taking the alongside arm of your offer: an own repository under my authorship that the suite references, since a second implementation is most legible as a second implementation when it has its own home, history, and CI, and a one-line link from your README is all the coupling the record needs. If you would rather have it in-tree, or would rather the checker not touch DSSE at all, say so and I will follow the suite's lead on both.

On chain scope, the floor is right, and the member is the one of the three that needs one more property to do its job. Key by subject is exactly the consumer's question, whether this image was rerun, and the per-key default you rejected does leak total run volume across customers the way you said. The gap is that a recommended minimum cannot be gated, and your own reset rule tells you where the pressure goes next. Once a chain reset is equivocation, the cherry-picker's cheapest move migrates to scope narrowing: declare scope as key by subject by corpus by posture, and every published run is legitimately genesis one of its own chain, no gap, no fork, nothing to detect. Demand-disclosure binds only if a consumer can check that the declared scope is no finer than the scope its policy demands, and that comparison needs the member to be machine-comparable rather than free-form: a closed set of dimension tokens with a pinned order, compared by subset, so that "no finer than substrate key and subject" is as mechanical as the rest of the validity checks, with an unrecognized token failing closed the way every other closed vocabulary in this spec now does. One reading is worth pinning in the member's definition while you are there, because the two halves of the design read different things. The policy comparison reads the declared dimension set; the equivocation rule has to key on the evaluated tuple, this key and this subject's values, not the token set. Under that reading genesis-per-subject is the normal case rather than a reset, and under the token-set reading every second subject's genesis would collide as equivocation, so the sentence is load-bearing rather than pedantic. With both in place the narrowing move becomes as visible as a gap or a fork, and your recommended minimum can stay a recommendation, because the policy hook is what does the binding.

Everything else in the round reads settled to me, the lineage note locating rather than importing and the changelog tripwire binding future versions where it belongs. I will start from the numbered spec text and the manifest, and the vetting second-reviewer commitment stands.

@Rul1an

Rul1an commented Jul 24, 2026

Copy link
Copy Markdown

Done, and the answer to the question we left open is the strongest one this exercise could return: everywhere the corpus looks, the sections determined the same implementation twice. The checker lives at github.com/Rul1an/aee-checker (Apache-2.0, Rust, no dependency on the reference implementation: own strict I-JSON parser, RFC 8785 serializer with ECMAScript number formatting, RFC 6962 domain-separated root over the DSSE PAE bytes, run-binding derivation, Ed25519 tier). The gate was written against the spec text at 4a36b19 and the public standards it pins, with the gate implemented in full before the first corpus run. That first run scored 125/125: 34/34 accepts including result tokens, 91/91 rejects, and the tier columns on ok-024 under both key policies. No vector-driven fix was ever made, so the mismatch table in PARITY-REPORT.md is empty and the load-bearing content is the eleven interpretation decisions the text forced, each recorded with the spec line that forced it. Those are the places to double-check me at vetting, since two implementations agreeing is strong evidence the text determines the reading, and the decisions list is where that evidence is inspectable.

Reason-per-reject is in report.json as free-form prose in my own words. The manifest's condition codes were never displayed, before or after the run; the manifest was only ever viewed through a field filter selecting id, kind, and the expected verdict, result, and tier. So the divergence measurement you wanted is available next to your codes with no contamination, and the full read and never-read attestation is the last section of the parity report, including one boundary disclosure about locating the key recipe in your README.

Three observations the run handed back. The key recipe publishes the seed formula but names no roles, so the substrate role had to be discovered by deriving candidate strings and probing them against a real vector signature; it would cost one line to publish substrate-observation-test and the keyid convention, sha256 over the raw public key bytes, beside the formula. bad-303 carries no construction-version member, so binding version two is detectable only as a run-binding digest mismatch, which is the fail-closed path doing its job, but it means the version literal inside the pre-image never gets exercised as a distinguishable reject; worth one vector if you want that lever tested on its own. And the tier accepts behave exactly as their names promise: ok-019 attests despite the deadbeef keyid, ok-020 stays unattested because the signature is not over PAE, and ok-023 attests with the embedded key never consulted.

NOTES.md confirms the vendored spec is byte-identical to the branch head, so the suite and the PR cannot drift apart silently today; a pinned upstream commit in the suite README would keep that property once the branch moves. The one-line link you offered is all the coupling the record needs, whenever convenient.

@astrogilda

astrogilda commented Jul 25, 2026

Copy link
Copy Markdown
Author

Thank you, this is the outcome I was hoping for. A second implementation, in another language, built from the spec text alone and landing 125/125 on the first run with no vector-driven fixes, is the best evidence I could ask for that the text determines the reading, not my reference code. The eleven decisions you recorded matter more to me than the score. They are the places where the text made you choose. I worked through all of them and the two seams you raised. Here is what changed.

The chain-scope narrowing attack

You were right, and it ran deeper than the version I had. A recommended minimum cannot be gated, so the cheapest move shifts from a chain reset to declaring a steadily finer scope until every run is a legitimate genesis of its own chain. I replaced the free-form scope string with a machine-comparable one: a duplicate-free array of tokens from a closed, registered vocabulary (subject, corpus, network posture), each pinned to a value already on the wire, sorted the same way the label vocabulary is. There is no string alias. The old form fails closed.

The projection registry goes past your sketch. It makes the evaluated tuple computable rather than declared, and that is what lets your set-versus-tuple reading actually be enforced. I pinned that reading in the text: consumer policy compares the declared dimension set, while the gap, fork, and genesis rules key on the evaluated tuple, so a genesis per subject value is the normal case and only a second genesis under the same tuple is a reset. The comparison goes past your sketch too. It is a two-sided equality, and no-finer on its own is not enough: a strictly coarser scope pools distinct subjects, and then a withheld run of the demanded subject is deniable as a sibling's private run, so a consumer that has demanded a scope admits only the equal set. I also stated the ceiling plainly: a contiguous, fork-free, correctly scoped chain still does not prove completeness, because a producer can mint a dense gap-free set after the fact. Fork-consistency across the published set is all a self-contained attestation establishes, and the rest needs the external registration receipt the predicate already defers to.

The eleven interpretation decisions

I went through all eleven. Where the text forces the reading I added a vector that locks it, and I catalogued each one against the spec line that forces it and the vector that holds it, in a small registry a CI check enforces, so determinacy is checked now and no longer only claimed. Those are the places to double-check me at vetting.

Of your four open corners, two turned out to be a requirement the spec already carries but no rail enforced, so I treated them as bugs and not as choices: a duplicate attackId across rows is now malformed (the exhaustion check set-compares the ids, so a duplicate would have collapsed silently), and the one-subject requirement now applies to a statement of any basis, not only a substrate-carrying one, so an artifact-only two-subject statement is malformed too. Both got vectors. The coverage-overlap corner was a genuine disagreement between us: my rails reject a class that is both assessed and disclosed as a gap, your checker accepts it, and no vector exercised it, so our 125/125 was blind to it. I pinned it to the reject reading, since a class both assessed and out of scope is contradictory, and made the disjoint partition explicit in the text, but that one is an editorial call and I am happy to reopen it at vetting if you read it the other way.

Your eleventh mattered most, and you were right that nothing exercised it. Both of my rails rejected duplicate members inside record payloads but not across the whole statement, so a duplicate at the top level was quietly kept last-wins. Both rails now parse the entire statement as strict I-JSON, and there is a raw-bytes reject vector for it, since the generators build from dicts and a dict cannot hold a repeat.

The two observations, and one bug you found

You should not have had to derive the test-key role by probing a signature. I published the role name and the keyid convention, sha256 over the raw public key, next to the seed formula.

On the binding version you were right that the literal never got exercised on its own. It lived only in the derivation, so a wrong version showed up as a digest mismatch and nothing else. An arming payload can now carry the version explicitly, and a verifier reads it before deriving and rejects a version it does not implement as the record covering nothing, which reads differently from the digest mismatch. The carried value never drives the derivation, so the digest stays authoritative and a record that claims version one but was built otherwise still fails on the digest. There is a vector for it.

The armedAt reading you took strictly caught a real bug on my side. The spec says RFC 3339 UTC, but both my rails accepted a non-zero offset and only compared instants, so an armedAt five hours ahead of UTC parsed as a valid instant and slipped through. Both rails now require a zero offset, the spec pins it, and there is a vector. I also mechanized the drift you flagged: the vendored spec's digest is pinned in the manifest and a CI step recomputes it, so editing the spec without regenerating the corpus fails closed and cannot drift quietly. And an out-of-range reference is now a fault on any row, not only substrate rows.

Your checker

I would like to take the alongside arm exactly as you framed it. Your repository keeps its own authorship, history, and CI, and I will add one line from the suite README pointing to it as an independent implementation verified against the corpus, with the upstream commit pinned so the two cannot drift. That is all the coupling the record needs, and a second implementation reads as one when it has its own home.

The corpus is at suiteRevision 2 now, thirteen vectors larger than the run you did, since a few of these changes add cases your first run could not have seen. When you have a moment I would value a re-run against it. Your second-reviewer offer means a lot, and I will lean on it at vetting.

Edited 2026-08-31: prose only, for readability. No figure, vector, field name or claim changed.

@Rul1an

Rul1an commented Jul 26, 2026

Copy link
Copy Markdown

Ran the checker against suiteRevision 2. Both numbers, because the boundary is more useful than the final score.

Unchanged, the suiteRevision 1 build scores 132/138 on the new corpus (34/35 accepts, 98/103 rejects). After a spec-diff-led update against the revised text, 138/138 (35/35, 103/103). Pinned to suite 55ee73321cd40edd2b4a814948506a60074543a2 and spec digest d3872a02875b2da8de0263e93fb92ca6f5ab0fd75f07ed3762a1b18b0c1712a3.

Six vectors separate the two runs:

Vector Old build Revision 2
ok-034-arming-chain-genesis invalid valid
bad-721-chain-scope-not-array valid invalid
bad-724-artifact-ref-out-of-range valid invalid
bad-728-artifact-two-subjects valid invalid
bad-729-duplicate-attackid-rows valid invalid
bad-730-coverage-class-overlap valid invalid

The six split into three classes. The chain-scope redesign accounts for ok-034 and bad-721: revision 1's string became revision 2's closed token array. Two were defects in my checker: subject cardinality was incorrectly scoped to substrate-carrying statements, and duplicate attackId rows collapsed under the set comparison. The remaining two pin formerly open boundaries: reference range checking on every row and the disjoint coverage partition. I accept the latter reading.

On the overlap: I read it your way, and not reluctantly. The revised text settles it. Three sets that are a disjoint partition of the manifest's classes, a move rather than a copy, and a class both assessed and disclosed as a gap is contradictory. I had been treating overlap as a weaker form of partial assessment, but that is not what the two labels mean together: one says the class was covered, the other says it was not, and carrying both asserts two statuses rather than a nuance. No need to reopen it at vetting on my account.

The ceiling you state alongside it is the part I would keep loudest. A correct partition shows the carried classification is honest about itself. It says nothing about classes or runs that never entered the manifest, and a producer can still mint a dense gap-free set after the fact. Good that the spec now says so in its own voice rather than leaving it to a reader.

Two things worth flagging back. Both reference rails accepted a non-zero offset on armedAt, and bad-727 is useful because it turns "RFC 3339 UTC" from prose into an executable zero-offset boundary. And the interpretation registry is a better idea than the eleven-item list it grew out of, with one qualification I would put in the docs: it is valuable as a post-run reconciliation surface. After an implementation has committed its own readings, the registry shows exactly where those readings diverged without either author having to arbitrate. Read beforehand it is an answer key, and a from-spec claim made against it would be worth less than one made without it.

One corpus edge the round turned up, offered rather than reported. The partition rule says the three coverage sets are a partition of the manifest's classes, and a partition is made of subsets of the thing it partitions, so membership runs both ways. bad-819 forces that for assessedClasses. Nothing forces it for the two reason maps, and my checker only enforced the assessed side: an unknown key in outOfScope or routedElsewhere, with result left alone, passed at full parity. The result recompute does not cover it either, since it ignores non-manifest classes entirely. Fixed here and guarded locally, but two vectors would close it upstream, one per reason map. Not a new reading, just an untested consequence of the rule already written.

One difference from the first run, stated plainly. That one was blind, straight at the corpus with no vector-driven fixes. This one is not, though the order matters: the six divergences came out of the baseline run itself, not out of your changelog. I ran the unchanged build first and it named them, then read vectors/CHANGES.md and the spec passages to work out what each should become. No Go or Python rail source was opened for either run, and neither were the manifest's expected condition codes, so the readings are still from the text. Still, having read the changelog before implementing, the honest description of this pass is an independent checker doing a spec-diff-led update with conformance verified rather than a second blind run, and I would rather say that than let the 138/138 borrow credibility from the 125/125.

All three run records are kept rather than overwritten, including the 132/138 baseline itself, with the six diverging vectors named inside the record instead of only summarised in prose. A suite pin and a spec digest fix the input but not the thing that read it, and the records do not carry that themselves: both revision-2 records have the same suite field and no checker field, differing only in the outcome. So the provenance sits in a sidecar index that has to travel with them, keyed on a deterministic digest of the checker's own source rather than a commit, since a commit cannot name itself from inside the file that carries it. The baseline is sha256:f39a6932…, the 138/138 is sha256:2bea1345…; the merge commit is linked below so those bytes can actually be fetched, since a content digest says what you have and not where to get it. The index carries each record's own sha256 as well, and CI checks the whole binding, so a swapped report or drifted metadata fails rather than passing quietly. The parity report carries the before and the after, with each formerly-open corner marked against the vector that now forces it, and it keeps three claims apart rather than blurring them: all three records are inspectable, all three are reproducible by hand from the checker and suite pins, and only the 138/138 is continuously re-verified by CI on every push.

Checker: Rul1an/aee-checker@47dbaf1

astrogilda added a commit to astrogilda/agent-evidence-vectors that referenced this pull request Jul 26, 2026
The coverage-partition rule (spec L381-383) makes the three sets a disjoint
partition of the manifest's classes, so membership runs both ways, but only
bad-819 forced the assessedClasses side. Add bad-731-outofscope-unknown-class
and bad-732-routedelsewhere-unknown-class: an unknown class key in each reason
map, result left alone, rejected coverage-incomplete. Both reference rails
already enforced it; the vectors lock the rule and mutation-prove the rails.
suiteRevision 3, 140 vectors; registry decision 14 extended; docs record the
registry as a post-run reconciliation surface. Surfaced by the independent
from-spec checker (in-toto/attestation#570 round-8).
@astrogilda

astrogilda commented Jul 26, 2026

Copy link
Copy Markdown
Author

Thank you for running it against the new corpus, and for keeping the boundary. The 132 out of 138 on the unchanged build is the more useful number: it says the six divergences are the round-7 changes and nothing else, which is what a build reading only the text should show. I also value how you drew the line on this pass. You named it a spec-diff-led update with the changelog read first, you kept the 132/138 baseline record, and you were careful that the 138/138 does not inherit the blind run's credibility. That is the honest way to report it.

On the overlap, thank you for reading it the same way, and for not leaving it as a courtesy. The two labels assert two statuses where one would do, and I am glad we got there because the text settles it.

Your reason-map edge was right, and closing it was on us. The partition is of the manifest's classes, so membership runs both ways, and only the assessed side had a forcing vector. I added the two you implied, one per reason map: bad-731 for the out-of-scope side and bad-732 for routed-elsewhere, an unknown class key in each map with the result left alone, each rejected coverage-incomplete. The rails already enforced it, so these lock the written rule and mutation-prove the rails: revert the reason-map accounting and the two vectors flip. That is suiteRevision 3, 140 vectors, with decision 14 now carrying all three.

The point about the registry went straight into the docs, because you are right that it cuts the other way when it is read first. I wrote it down as what it is: a surface for reconciling readings after the fact. Used that way it shows exactly where two implementations diverged; read beforehand it becomes an answer key, and a from-spec claim made against it is worth less. Your run is the proof of the distinction, since the divergences came out of the baseline before you read anything.

The provenance index you built is the right shape for this. It keys on a digest of the checker's own source, so the record names what produced it, and that is close to how we pin the suite and the spec on our side. A line from the suite README pointing at it would let a relying party follow the whole chain.

Where that leaves us: I have no open disagreement left. If you read v0.6 the same way, I think it is ready to come out of draft, and I would rather move it on the strength of an independent implementation that reached it from the text than on my say-so. Your call on the timing; I will follow your read.

Looking past this, and only once v0.6 lands: I have a v0.7 in mind that I would bring as its own PR. The short version is first-class anchors and evidence references, so a verdict can point at the external corroboration it currently only names in prose, and a ledger for chained runs. It is additive, and it does not reopen what v0.6 says. If you would be up for the same eyes on it when it is drafted, I would value that.

@Rul1an

Rul1an commented Jul 26, 2026

Copy link
Copy Markdown

Revision 3 is in. 140/140 on the first run, 35/35 accepts and 105/105 rejects, checker unchanged from the revision-2 build. Pinned to suite cf0d5402327ae5a451efebc914852d1c687753ca and the same spec digest as revision 2, since round 8 changed no normative text.

The part worth more than the number is what bad-731 and bad-732 actually tested. They passed because the rule they force was already compiled, and that is checkable rather than asserted: the reason-map membership check went in at 47dbaf17 at 11:25 UTC, the comment above naming it carries GitHub's own 11:37 stamp rather than mine, and your revision-3 suite commit is 13:11, an hour and three quarters after the code. The checkerSourceDigest on the revision-3 record is byte-identical to the revision-2 one, so "unchanged" is verifiable from the index instead of being a sentence in prose.

What that is not is convergence. I named the gap in the comment above and you wrote vectors for it, so the causation runs from my report into your corpus, not two implementations meeting in the middle. The narrower thing the ordering buys is still worth having: the reading was already running against 138 vectors before your two arrived, so the vectors tested a rule rather than defining one. Those are different claims and I would rather name which one this is than let the 140 read as the stronger one.

On v0.6 leaving draft, I read it the same way, and yes. With one boundary I would keep attached to the endorsement, because it is the same one you wrote into the coverage text. A corpus can only force what someone thought to write a vector for. Where the registry records a decision and no vector pins it, my reading and yours agreeing is untested rather than confirmed, and a third implementation could differ there in silence. That is not an argument for holding v0.6, it is what a 140/140 does and does not mean, and I would rather it be said in the same voice as the partition ceiling than discovered later.

The run records are merged, four of them now, including the 132/138 baseline. Each entry binds its report's own sha256, the checker source digest and the suite commit; the vendored spec digest joins from suiteRevision 2, since the revision-1 corpus did not carry one to pin yet. CI checks that binding on every push to main and every pull request, so a swapped report or drifted metadata fails rather than passing quietly. The rerun recipe follows the current pin, and earlier revisions are reproducible the same way from their own entries.

Rul1an/aee-checker@0cf46c1

The README line pointing at the index: happy to send it as a small PR against the suite so the wording and placement stay yours.

And yes to v0.7. One thing I would want decided early, offered now while it is cheap. A first-class anchor makes external corroboration addressable, which is not the same as grounded. If the reference does not carry what position the corroborating party held relative to the thing it corroborates, a relying party reading a populated anchor will infer independence the field never asserted, and that inference will be the reader's own rather than anything the issuer signed. Same shape as the partition: honest about itself, silent about sufficiency. Either the anchor carries that, or the spec says in its own voice that it does not. On the ledger, if runs are going to chain, the property worth naming early is non-equivocation rather than per-entry soundness, since a ledger can be sound entry by entry and still show two readers different histories.

Edited: the first version of that paragraph said every entry binds the spec digest. Three of the four do. The revision-1 entry predates the vendored digest, and the sentence now says so.

@astrogilda

astrogilda commented Jul 27, 2026

Copy link
Copy Markdown
Author

Heads-up before you re-run the suite: one vector will fail, and the reason is ours.

I pushed a revision that pins two things the text had left open, and the first of them is encoding. Strict I-JSON named only its duplicate-member half, and the string half was scoped to BMP-only, which governs which scalar values may appear, and says nothing about whether the bytes denote scalar values at all. Nothing in the text said that an unpaired surrogate escape, a surrogate encoded directly in UTF-8, an overlong form, or a raw control character makes a record malformed.

Your checker rejected all four from the first build, and ours did not, which I would rather say plainly than bury. A lenient decoder does not fail on ill-formed bytes, it substitutes U+FFFD, and the observationVocabulary digest is recomputed from decoded strings, with the carried bytes never entering the comparison. So a producer could write ill-formed bytes into a label, derive the digest over the substituted form, and end up with something one of our rails called valid while the others called it malformed. Yours was the one implementation that never had the hole.

The second thing is nesting depth, and that is the one that will fail on you. No bound appeared in the text, so each of us picked one. You picked 256 and our rails picked 128, which left 127 depths where the same bytes are valid evidence to one conforming verifier and malformed to another. Nobody could see it until there were two readings of the same document to compare.

It is normative at 128 now, and the counting rule is stated next to it. Your parser increments per parsed value where ours count open containers, so that alone puts two implementations a level apart from an identical constant. On the number itself: the deepest statement in the whole corpus runs seven levels and the deepest payload runs two. So 128 leaves about eighteen times the headroom anything real has used, and the tighter bound is the safer default for a format that fails closed. It is also serde_json's own recursion limit, which is no help to you since you wrote your own parser.

Concretely, suiteRevision 5 is 149 vectors. The new bad-741-payload-nesting-exceeds-max-depth carries a covering payload nested 129 deep with every reserved member intact, so depth is the only fault in it. Your build answers valid there and the reference rails answer invalid. That should be MAX_DEPTH in src/json.rs and nothing else, since the rest of the tier already passes on your side untouched.

I have written 148/149 into the README and the implementation report and have not rounded up, because the gap is real until the constant moves. Say if you would rather the bound went the other way. The case for 128 is headroom and a fail-closed default. It is not a strong preference, and the text is still in review.

Edited 2026-08-31: prose only, for readability. No figure, vector name, constant or claim changed.

Rul1an added a commit to Rul1an/aee-checker that referenced this pull request Jul 28, 2026
The spec pins both halves of the depth rule at v0.6+: a statement or record
payload deeper than 128 is malformed, and depth is the number of arrays and
objects open at a point, with the outermost brace at depth 1 and scalars not
counting. This parser had neither. It incremented in parse_value, so every
value including a scalar leaf moved the counter, and the bound was 256.

The constant was the visible half and the counting rule was the load-bearing
one. Measured on the raw bytes of every document in suiteRevision 5, which
needs no parser and so covers the deliberately ill-formed vectors too, this
parser read exactly one level deeper than the spec rule on all 149 statements
and on every record payload inside them, because every deepest path in the
corpus ends in a scalar. Changing only the constant to 128 therefore rejects a
statement at depth 128, which the spec calls valid.

The corpus cannot see the difference: both the constant-only edit and this one
score 149/149 on it. Not because it is shallow -- bad-741's payload sits at
depth 130 -- but because nothing in it sits at 128, the one depth where the two
readings disagree. A scalar leaf inside 128 open containers reads as 129 to a
per-value counter and 128 to a per-container one; at 129 both reject, and at
128 with an empty-container leaf both accept. The tests carry that boundary
instead.

Refs in-toto/attestation#570.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Rul1an added a commit to Rul1an/aee-checker that referenced this pull request Jul 28, 2026
The unchanged revision-3 checker scored 148/149 against revision 5. The record
for the fixed build is added, revision 3 is retired from continuous
verification, and the workflow moves with it: suite pin, spec pin, the report
the fresh run is compared against, and the parity string the corpus step
asserts. That last one is a grep, so leaving it on 105/105 would have failed
the step against the newly pinned suite rather than failing quietly.

INDEX.json's entry for revision 3 gains its checkerCommit at the same time. It
was the one record whose provenance nothing could check, and 0cf46c1 hashes to
exactly the digest that entry already recorded, so the field becomes a
verifiable binding rather than a label. It names a source tree rather than a
commit, so 47dbaf1 satisfies it equally; that is the digest working as
intended, not a weaker claim than it looks. Revision 4 is listed in NOTES.md as
not run here rather than left as a silent gap in the sequence.

Refs in-toto/attestation#570.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rul1an

Rul1an commented Jul 28, 2026

Copy link
Copy Markdown

Keep 128. The headroom argument holds, fail-closed is the right default for this, and nothing on my side wants the bound moved.

The constant alone would have passed the vector without making my counting right, though, and the counting rule you stated next to the bound turned out to be the load-bearing half. My parser incremented in parse_value, so a scalar leaf moved the counter too. Measured on the raw bytes, which needs no parser and so covers the deliberately ill-formed vectors too, it read exactly one level deeper than your rule on all 149 statements and on every record payload inside them, because every deepest path in the corpus ends in a scalar. Setting MAX_DEPTH to 128 while keeping per-value counting reaches 149/149 and still rejects a statement at depth 128 that the text calls valid. I moved the increment into the container branch instead: Rul1an/aee-checker#3 It is 149/149 on suiteRevision 5 now, if you want the README and the implementation report to stop saying 148.

Worth knowing that the corpus cannot tell those two fixes apart. Not a depth problem, since bad-741's payload sits at 130. Nothing in the corpus sits at 128, the one depth where the two readings disagree, so the constant-only edit scores 149/149 as well. I pinned that boundary in my own tests. If you want it in the suite, an accept vector at open-container depth 128 with a scalar leaf is the whole thing.

That same shape appears on your side, and this is the part I would have wanted told to me. decodeValue takes depth as the number of enclosing containers and recurses per child, so an empty container never charges its own level. Against aee/jcs.go at ea25a1e, through parseJSONValue and so CheckIJSON and Canonicalize with it:

open-containers=129  scalar-leaf         REJECT
open-containers=129  empty-object-leaf   ACCEPT
open-containers=129  empty-array-leaf    ACCEPT
open-containers=130  empty-object-leaf   REJECT

The Python rail disagrees with it. _max_json_depth is a true bracket counter, reports 129 for both shapes, and run_vectors.py:440 and :708 reject above 128. So the two rails split on identical bytes at exactly one depth, which is the thing the comment above MAX_PARSE_DEPTH puts the bound there to prevent: "pinned to match the Go rail ... so the two independent rails accept and reject exactly the same payloads. The depth bound is a cross-rail parity requirement, not only a DoS defense". jcs_dos_test.go sits at 128, inside the agreement region, and bad-741 uses a scalar leaf that Go handles correctly, so neither one can see it.

It looks like the guard in decodeValue moving into the container branch and testing depth >= maxParseDepth. Tightening it where it stands takes a valid scalar at 128 with it. The twin guard in appendCanonical is unreachable with Canonicalize parsing first, so only decodeValue changes behaviour. A reject vector at open-container depth 129 with an empty-container leaf is what would catch this one, which pairs with the accept vector above.

Small thing in that same comment. serde_json's constant is 128, but check_recursion! decrements before testing against zero, so its effective ceiling is 127 open containers. I checked on 1.0.151: object and array chains both accept at 127 and reject at 128. Under your counting rule a serde_json-based verifier therefore rejects at exactly the depth you call valid. That does not argue against 128, it just makes it an awkward precedent to lean on.

One question about the strict I-JSON paragraphs above the depth rule. They say the whole statement is parsed as strict I-JSON, and the MUST underneath is scoped to string literals being well-formed sequences of Unicode scalar values. Noncharacters are scalar values, so the MUST is narrower than the label it sits under: RFC 7493 section 2.1 forbids Noncharacters in the same sentence as Surrogates. U+FFFF in an object member name inside a substrate-signed canonical payload passes both my checker and your Python rail, and I find no noncharacter handling anywhere in the corpus. Nothing substitutes anything in that case, so identical bytes give identical digests on every rail and there is no split to be had, which may be exactly why you scoped it where you did. Either way it seems worth a sentence, because a reader implementing the label rather than the MUST will write the check and reject records you accept.

Rul1an added a commit to Rul1an/aee-checker that referenced this pull request Jul 28, 2026
…at 149/149 (#3)

* fix(json): count nesting depth over open containers, bound at 128

The spec pins both halves of the depth rule at v0.6+: a statement or record
payload deeper than 128 is malformed, and depth is the number of arrays and
objects open at a point, with the outermost brace at depth 1 and scalars not
counting. This parser had neither. It incremented in parse_value, so every
value including a scalar leaf moved the counter, and the bound was 256.

The constant was the visible half and the counting rule was the load-bearing
one. Measured on the raw bytes of every document in suiteRevision 5, which
needs no parser and so covers the deliberately ill-formed vectors too, this
parser read exactly one level deeper than the spec rule on all 149 statements
and on every record payload inside them, because every deepest path in the
corpus ends in a scalar. Changing only the constant to 128 therefore rejects a
statement at depth 128, which the spec calls valid.

The corpus cannot see the difference: both the constant-only edit and this one
score 149/149 on it. Not because it is shallow -- bad-741's payload sits at
depth 130 -- but because nothing in it sits at 128, the one depth where the two
readings disagree. A scalar leaf inside 128 open containers reads as 129 to a
per-value counter and 128 to a per-container one; at 129 both reject, and at
128 with an empty-container leaf both accept. The tests carry that boundary
instead.

Refs in-toto/attestation#570.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* feat: record suiteRevision 5 at 149/149 and repin CI

The unchanged revision-3 checker scored 148/149 against revision 5. The record
for the fixed build is added, revision 3 is retired from continuous
verification, and the workflow moves with it: suite pin, spec pin, the report
the fresh run is compared against, and the parity string the corpus step
asserts. That last one is a grep, so leaving it on 105/105 would have failed
the step against the newly pinned suite rather than failing quietly.

INDEX.json's entry for revision 3 gains its checkerCommit at the same time. It
was the one record whose provenance nothing could check, and 0cf46c1 hashes to
exactly the digest that entry already recorded, so the field becomes a
verifiable binding rather than a label. It names a source tree rather than a
commit, so 47dbaf1 satisfies it equally; that is the digest working as
intended, not a weaker claim than it looks. Revision 4 is listed in NOTES.md as
not run here rather than left as a silent gap in the sequence.

Refs in-toto/attestation#570.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
@astrogilda

Copy link
Copy Markdown
Author

Thanks for this. It is the second time a read of yours has caught something five agreeing rails could not, and this one was in my code. You have decodeValue right. It carried depth as the count of enclosing containers and charged on child recursion, so an empty container never charged its own level, and the Go rail accepted an empty-object leaf at depth 129 where the Python rail, counting brackets, rejected it. Two reference rails splitting on identical bytes at one depth is the parity the bound is there to hold. The DoS test lives at 128, inside the region where they agree, and bad-741 uses a scalar leaf the buggy rail handles correctly, so between them they could not see it. I moved the guard into the container branch, so a container is charged the moment it opens. The canonicalizer parses first, which leaves its second guard unreachable, and the TypeScript payload parse had the same slip and took the same fix. Your suggested pair is in the suite. ok-036 puts a scalar leaf at depth 128, bad-742 an empty-container leaf at 129, and the empty shape is what discriminates, since a per-child counter gets the scalar right and lets the empty one through.

The part worth sitting with is that you found two rails of ours disagreeing, which is a different thing from a spec ambiguity and says something about how we test. A differential harness over our own implementations should have caught the disagreement before you did. It did not, for three dull reasons: it fuzzed the canonicalizer against a fixed hostile pool, its depth axis never climbed past four levels, and its Go member was a different canonicalizer than the reference gate, so the code the bug lived in sat outside the harness entirely. That gap is closed now. A new mode drives the four verifier ingress gates directly, the reference gate CheckIJSON a first-class rail alongside the TypeScript and two Python parsers, over inputs built at the boundaries on purpose: the depth ladder crossed with leaf shape, then the string edges under it. Revert either depth fix today and the lane goes red on the empty-container-at-129 input you sent. My apparatus was watching for drift between rails that already agreed, and watching the canonicalizer, when the thing to watch was the gate and its edges. That was fixable, and it is fixed, so the next slip of this shape fails a build here before it reaches you.

You are at 149 of 149 on suiteRevision 5, and you moved the increment into the container branch instead of only touching the constant, which is the counting rule the text asks for and the reason the constant-only edit would still have been wrong. The README and the report read 149 now, not 148, and the report says plainly that you adopted the bound and corrected the counting. Thank you for not taking the constant-only path the vector alone would have paid out.

You are right about serde_json, and the precedent is gone. Its recursion check decrements before it tests, so the real ceiling is 127 open containers, and such a verifier rejects at the depth the spec calls valid. An awkward thing to lean on, then, rather than inherited conformance. The bound rests on the headroom and the fail-closed default, which is where it should have rested from the start.

Noncharacters you said were worth a sentence, and I think they earn more, so I took the other road. There is no split to be had, since a noncharacter decodes the same everywhere and the digests come out identical. But a one-sentence fix is leaky for exactly that reason. A reader who implements the RFC 7493 label, rather than the narrower scalar-value rule, writes the check and rejects records we accept, which is the divergence the profile exists to close. So instead of narrowing the label to fit the rails, I brought the rails up to the label. All five reject the 66 noncharacters wherever a string literal sits, at any depth, in member names and values alike. bad-743 carries U+FFFF in a vocabulary label and bad-744 in a payload value, the exclusion is written into the spec, and the decision is registered. Your checker admits them today, so those two are a directed difference on your side, the same way bad-741 was, and I have not counted them as yours in the report.

There is a process point I owe you as well. When I told you bad-741 would fail your build, I named the constant and the file, which turned your next run into a directed fix when a blind read of the text is the whole value of your column. The next revision comes with a rule to stop me doing that. I will publish the vectors without the spec diff, or the diff without the vectors, and skip the heads-up that names the fix. Let the divergence surface from your run and then point back at the text, so the corpus carries the authority and not my word for it. Yes to your README line, and please send it as the small PR against the suite, with the wording and placement left to you.

Both v0.7 questions are the right ones to settle early, so take the anchor first. You are right that addressable is not grounded, and the word was carrying two jobs that pull in opposite directions. One is standing, whether the corroborator is independent or has a stake, and the field should carry none of it. A relying party has to map the corroborating key to a known party before it can credit anything, so knowing the key already means knowing the standing, which leaves a declared token redundant when honest and a lie surface when not. The spec will say in its own voice that a corroboration reference asserts nothing about standing, and that a relying party derives standing from its own policy over the key. The second job is the referent, which object was corroborated and at what altitude, and this one the field has to carry, because nothing else does. A timestamp token or an OpenTimestamps proof signs a bare hash with no media type, so a consumer holding it cannot tell whether that digest was the corpus-manifest root, the catch policy, an arming record, or the evidence bundle, and each of those closes a different attack. So the reference carries a referent token from a closed vocabulary, each pinned to a projection onto a digest already in the attestation, alongside the mechanism class. The verifier recomputes that projected digest, and a declared value that does not match is malformed. It reuses the read-first binding-version shape, where the declared value only routes and the recomputed digest governs.

Non-equivocation is the right property to name for the ledger, and I want to name it the way the spec names run-population completeness, which is to disclaim it. The chain members reach fork consistency inside one consumer's view and no further, and two readers can be handed different histories with no self-contained set exposing the difference. So the text will say outright that non-equivocation belongs to a witnessed append-only log and not to a self-contained attestation set. v0.7 then carries the reference shape of a run-start registration receipt, a registration kind that commits an arming record to a log, SCITT with COSE receipts, without parsing the receipt or claiming the log's witnessing for itself. The one neighbor I would fold in is the temporal version of the scope-narrowing you closed. A campaign seal a producer cuts whenever it pleases lets it seal around a bad run, so the cadence becomes a closed-vocabulary token under the same two-sided equality, and a missed cadence reads as a presumed failure under consumer policy. All of that arrives as its own PR once v0.6 lands, and I would want the same eyes on it.

The protobuf rides in this revision, since it was the last thing left before draft could come off. It is transport and codegen only. The closed vocabularies travel as strings, so that an unknown value keeps fail-closing at the recompute instead of vanishing into a zero-valued enum member, which also matches the house convention, and the header states in plain words that its JSON must never be re-canonicalized for signing.

If v0.6 reads to you the way it reads to me after this round, I think it is ready to leave draft. I would rather move it on an independent implementation that reached it from the text than on my own reading of it, so the timing is yours.

Rul1an added a commit to Rul1an/aee-checker that referenced this pull request Jul 28, 2026
…53 (#4)

* fix(json): reject the Unicode noncharacters in every string literal

suiteRevision 6 makes the RFC 7493 section 2.1 exclusion normative: the sixty-six
noncharacters, U+FDD0 through U+FDEF and U+nFFFE and U+nFFFF in each of the
seventeen planes, are malformed wherever a string literal appears, at any depth
and in member-name as well as value position.

This checker admitted them, and the reason is worth recording because it was not
an oversight. The earlier text scoped its MUST to string literals being
well-formed sequences of Unicode scalar values, and a noncharacter is a scalar
value, so the narrower rule was implemented faithfully. What the revision changes
is the rule, not the reading: the strict-I-JSON label above that MUST had always
implied the wider RFC 7493 exclusion, and the revision closes the gap between the
label and the rule underneath it.

Both routes into a string body are covered, because the exclusion is over code
points and a producer reaches them either way: the raw UTF-8 byte, and the escape
including a surrogate pair resolving into a plane-end noncharacter. The plane-end
pairs differ only in their lowest bit, so one mask covers all thirty-four, and a
test walks the whole code space to confirm the predicate selects exactly sixty-six.

Refs in-toto/attestation#570.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

* feat: record suiteRevision 6 at 153/153 and repin CI

The unchanged revision-5 checker scored 151/153. The depth-boundary pair ok-036
and bad-742 passed on the container-branch counter already in place; bad-743 and
bad-744 did not, and those two are what the previous commit fixes.

The record says plainly that this run is directed, and more so than revision 2
was: the rule was written and the vectors named before this checker ran, so what
it shows is that the corrected rule is implementable from the text, not that an
outside reader found something. Revision 5 is retired from continuous
verification and keeps its checkerCommit, 88c37d1, so its provenance stays
checkable after the pin moves. The workflow follows: suite pin, spec pin, the
compared report, and the parity string the corpus step greps for.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
@Rul1an

Rul1an commented Jul 28, 2026

Copy link
Copy Markdown

The revision-6 run is 153/153, and the label on it should be directed, more so than revision 2 was: Rul1an/aee-checker#4

ok-036 and bad-742 passed on the container-branch counter from last round, so the depth pair cost nothing. bad-743 and bad-744 did not, and you had named both the rule and the vectors before I ran, so what the score shows is that the corrected rule is implementable from the text, not that a second reader found anything. Your derived expectation in the suite README was exactly right on both counts, which is worth saying since you were careful to mark it as derived.

The blind evidence stays where it was: 125/125 at revision 1, first full run, no vector-driven fixes. Revision 3 is the other shape worth keeping, 140/140 first-run on the unchanged build, where the reason-map rule came out of the text and your two new vectors met it rather than drove it.

Worth saying why the checker admitted noncharacters, since it was not an oversight. The MUST was scoped to string literals being well-formed sequences of Unicode scalar values, and a noncharacter is one, so the narrower rule got implemented faithfully. You changed the rule rather than the reading, which is the right way round. Both routes needed covering on my side, the raw byte and the escape, including a surrogate pair that resolves into a plane-end noncharacter.

The rule you set for the next revision does the job. Of the two halves I would take the vectors without the diff: the diff on its own still names the rule, so the read is directed anyway, just without the vector names.

On leaving draft, I read the guidelines first, and they put acceptance at the next maintainers meeting, so the only thing my column can carry is what an implementer can attest. Here is that, and its edge.

The mechanical gate I checked row by row against the current head rather than from memory. Template sections in order, the three header fields, the entry in the vetted-predicates list, the protobuf, the parsing-rules opt-in naming the monotonic principle with the one strengthening written down, and lowerCamelCase throughout with the only underscores in the current schema sitting inside vocabulary values. One soft edge: the guidelines ask for RFC 3339 with timezone Z, and armedAt pins a zero offset while issuedAt does not, so 2026-06-23T16:08:07+05:00 is conformant AEE and off-guideline.

What I cannot attest is whether the predicate is the right shape for the framework, and I would not want my column read as saying so. That is a scope judgement and it belongs to them.

So yes from me, in that bounded sense.

One thing worth having in the text rather than saying it live. Eight of the thirteen vetted predicates carry ResourceDescriptor inside the predicate body: link, reference, scai, test-result, runtime-trace, svr, and both SLSA predicates, whose .md files delegate to slsa.dev but whose protobufs in this repo import the descriptor for resolvedDependencies, byproducts and the VSA's policy. AEE never mentions it, while substrate, corpus, catchPolicy and networkPosture are all descriptor-shaped and untyped, so someone is going to ask why they are not descriptors.

You have a good answer already and it is not that the type does not fit. corpus.manifest and networkPosture.posture are not ResourceDescriptor members, and the two places a descriptor would take extra material are both places the framework tells consumers not to rely on: annotations is metadata a consumer MAY use, and an extension field on any object carries the rule that its presence or absence MUST NOT influence the meaning of any other field. The manifest is a required input to a gate that decides validity, so it has to sit where a verifier is obliged to read it. That is a reason with the parsing rules behind it, which reads better written down than improvised.

The README pin is one line now: astrogilda/agent-evidence-vectors#2 Your paragraph is better than the one I first sent, so what was left is that the reference resolves to 0cf46c1, the revision-3 record commit, where the sentence above it says the link points at the build that recorded 149/149. The revision-6 sentence in that paragraph is stale now too, though that one is yours to reword rather than mine.

Both v0.7 answers land the way I would have argued them, and the referent token pinned to a projection onto a digest already in the attestation is the part I would not have got to on my own. Send the PR when v0.6 is through and I will read it the same way.

Last thing, on the harness. The reasons you gave are the more useful half of this round. Fuzzing the canonicalizer while the gate went unfuzzed, and the Go member being a different canonicalizer than the reference gate, are exactly the shape that stays invisible from inside, because everything you are looking at agrees. I would not have found that from outside either. It came out of you asking why your own apparatus missed it, which is a harder question than the one I asked.

astrogilda added a commit to astrogilda/agent-evidence-vectors that referenced this pull request Aug 20, 2026
The type URI appeared in five places as a bare fact, so a reader who
followed it got a 404 with nothing in the repository explaining why,
and the reasonable conclusion from that is that the specification does
not exist.

The in-toto attestation catalog redirects the URIs of vetted
predicates whose specification is merged. This predicate is in review
as in-toto/attestation#570, so its URI is not yet served, which is the
ordinary condition of a predicate at that stage. Each of the four
prose sites now states that, says the URI identifies the predicate
type rather than being fetched during verification, and points at the
vendored copy of the specification that this repository carries.

The fifth site is the vendored specification itself. It stays
byte-verbatim: 121 spec:NNN citations index into it by line number and
its SHA-256 is pinned in VENDOR-PIN.json and MANIFEST.json, so the
note for it lives in spec/README.md, which introduces the copy and
covers the schema $id alongside it.
@astrogilda

astrogilda commented Aug 20, 2026

Copy link
Copy Markdown
Author

A correction I owe you from before you started building, and then the vector.

When I handed the suite over on 23 July I told you I declare in the manifest that the verdict, and each accept's result token, is the normative comparison surface, and that the per-vector condition codes are informative. For a month the manifest carried no such declaration. Its keys were suite, predicateType, specPath, specDigest, tracksUpstream, specUpstreamCommit, counts, corpusDigest and vectors, and expected.codes sat on all 193 reject vectors with nothing anywhere saying what its status was for a second rail. I promised it and did not write it. You built to it regardless: your run reports 250/250 with reason parity 69/193 as a separate number, which is the treatment the promise described. The experiment stayed honest because you kept the two surfaces apart, not because the file made you. It is there now, as a top-level comparisonSurface member on main: expected.verdict and each accept's expected.result are the normative comparison surface, the condition codes are my implementation's vocabulary and measured rather than scored for any other rail, and a second rail reports reason parity separately and does not fold it into the score.

On the arming scope I committed to a statement with every row caught and two rows resolving different subsets of two arming records at divergent postures. I built both halves with the corpus's own generator and measured them on five compiled rails. The every-row-caught half is inert. It produces byte-identical output on every rail I can construct, including the one with the conjunct deleted by the corpus's own mutation tool, and bad-902 moves under that mutant, so the read path is proven. The mechanism is that carriedRecordsCover sweeps every carried covering-kind record bound to the run and refuses any arming record whose posture is not the pinned one before a single row is consulted, so the row-scoped conjunct is reachable only inside statements already refused for another reason. The only thing it can ever change is which condition is reported first, which is exactly the precedence bad-902 already pins. CONTRIBUTING.md forbids the shape a second time over, because the specification sentence it targets says outright that which arming records supply the set on a check that reads no row is not settled by it, and a vector may not settle a question the specification leaves open. So that half goes to the unforced-coverage ledger as a forcible-but-unforced cell, carrying the five-rail measurement as its evidence. That cell is not in the unforced-coverage file on main yet either; it lands with the pair. Shipping it as a vector would have reproduced inside my own corpus the defect I wrote to you about, a rule that reads as forced and is not.

The other half survives and does more than I promised, once it is paired with a second vector I had to invent. Both are built and measured here and neither is on main yet, so do not go looking for them in the corpus: they will land as bad-1018, carrying a divergent arming record no row resolves, and bad-1019, carrying one resolved only by a caught row. Read together they name the reading: both report arming-covers-nothing under the shipped row-local reading, both report sealed-covers-nothing under a statement-wide one, and they split under a referenced-anywhere one. Either alone leaves two of the three open. Replaying all 250 shipped vectors under each rival moves nothing, for statement-wide and for referenced-anywhere alike. Two independent rival readings, zero observable difference across the entire published corpus, so a second implementer can hold either one today and score 250/250. That number is the argument for landing them. Three accepts go with them, because a too-strict rail is the failure on the other side: two arming records both at the pinned posture resolved by different rows, a divergent arming record declaring another run's binding, correctly accepted since it makes no claim about this run, and a registered non-covering kind carrying a divergent posture digest. All three pass on the shipped rail and on all four alternatives.

One reason the corpus could not see any of this is mine. bad-703 carries the same divergent-arming shape, and its expected set names all three of arming-covers-nothing, sealed-covers-nothing and clean-row-uncovered, so it is satisfied by any of them and stops measuring the question instead of starting to. The two new rejects carry single-valued code sets, and the [[reading]] entry that lands with them will declare expect = "DISCRIMINATED" with both witnesses named, since MASKED is what the differential gate returns and never what an entry asks for. READINGS.toml on main carries two entries today and neither is this one.

On your three-consumers finding, here is what a specification sentence has to constrain, since I prefer writing it to admiring it. A refusal message is itself a claim about which comparisons ran, so bind it to the evaluated set: an implementation can name a condition in a refusal only where that condition was evaluated on that statement, and it cannot name a comparison whose operand set was empty. Your hoist satisfies the first clause and breaks the second, which is the part that interests me: the sweep still ran and still refused, and what changed is that the arming term arrived carrying nothing while the message went on describing a comparison against every carried arming record. Written that way the constraint is checkable from outside a rail, since the reported condition set becomes a function of what was evaluated rather than of what the author put in the string. The case I am least sure of is a comparison evaluated over a set the implementation cannot enumerate at message time. Did you hit that in the checker?

Edited 2026-08-20: this named two vectors, a reading entry and a ledger cell in the present tense when all four are built here and not yet on main. Corrected above so nothing sends you looking for something that is not published.

Edited 2026-08-31: prose only, for readability. No vector name, figure or claim changed.

@astrogilda

astrogilda commented Aug 20, 2026

Copy link
Copy Markdown
Author

Two corrections matter if you are reading from this pull request. Both concern the gap between the head here and my vendored copy. I have edited the comments they came from, so the wrong versions no longer stand above the fixes.

On 11 August I wrote that the reporting paragraph was in the branch, and it is not. The head here is 95470f3 and it carries none of that wording; the coverage sentence still reads "the arming record's" at line 1349, so the definite-singular fix I described in the same message is also only in my copy. Everything I said about what those edits do stands, and none of it has landed upstream yet.

The specUpstreamCommit I cited beside the new spec digest, 0dbe10b, resolves in neither fork. Treat it as a dangling pin: the digest 759d2383 is taken over my vendored file, and nothing you can fetch hashes to it, until I replace the pin with a commit that exists.

And from this morning's message, bad-1018 and bad-1019 are built here and not published, along with the reading entry and the ledger cell that go with them, so a grep for any of the four in the corpus will correctly find nothing.

Edited 2026-08-31: prose only, for readability. No commit, digest, line number or vector name changed.

@Rul1an

Rul1an commented Aug 20, 2026

Copy link
Copy Markdown

Yes, three times in one message, and none of them is the case you are least sure of. Applying your
sentence to our own refusals found them, which is the strongest thing I can say for the sentence.

The site is the carried-record sweep, src/check.rs:1701-1707. Its refusal reads:

observationRecords[N] is a sealed record binding to this run whose clean-row conjuncts do not hold:
aeeStillArmed, the drop count against its bound, and aeePostureDigest against both the pinned
networkPosture digest and every carried arming record

It names comparisons that did not run. The conjunction is computed in check_sealed as
still_armed && (drop_count == 0 || bound) && posture == pinned, and && short-circuits. Our
published run measures how far that goes: bad-1003 through bad-1006 emit one byte-identical
reason string across four different failing conjuncts — aeeStillArmed false, drops with no bound,
drops over bound, and a posture mismatch. Four producer errors with four different fixes, one
string. That is your first clause, and it is the same complaint you made about one name covering
three kinds, one level down and in my code rather than in your spec.

It names a comparison whose operand set is empty a third of the time. sweep_arming_ok is
arming_postures.iter().all(|a| a == pd), vacuously true on empty. I instrumented the site and ran
the corpus: of 66 evaluations, 22 reach it with arming_postures empty while the message goes
on naming the comparison. ok-001-caught-intercepted-fail is a minimal witness — one caught
intercepted substrate row, records [interception, sealed], no arming record, accepted. Nothing
earlier guarantees a non-empty set: the only refusal that would, at line 1434, sits inside the
clean-intercepted arm, so any statement of caught or reconstructed rows arrives here with zero.

It names a set wider than the one compared, and wider than your spec. This is the one I would
not have found without your sentence. arming_postures is built from referenced_arming, the
arming records some row resolves. The message says every carried arming record. Your spec says
"the aeePostureDigest of every arming record the row resolves", and says outright that which
arming records supply the set on a check that reads no row is not settled by it. The string "carried
arming" appears nowhere in your specification. So the phrase matches neither your text nor my
code; it is the message's own invention, and it survived the hoist made to fix exactly this class of
overstatement at exactly this site. My own comment 380 lines above concedes the narrowing while the
message tells the producer the opposite.

The honest bound on all three, because it changes what you should do with them. These are
reporting defects, not soundness holes, and I could not turn them into one. Both operands are
separately pinned to the same value — check_sealed requires posture == ctx.posture_digest and
check_arming requires it of any arming record that binds and validates — so I could construct no
statement the two readings decide differently. I mutated the code to match the message, ranging over
every carried arming record: 250/250, reason parity 69/193, byte-identical output. Deleting the
arming conjunct at either site is likewise byte-identical. A positive control on the same line
(deleting sealed_covers_clean) breaks two vectors, so the harness is sensitive there and the
survivals mean what they say. The arming conjunct never independently decides an outcome anywhere in
your corpus.

One consequence I did not enjoy finding: my comment claiming the restoration "keeps this site's
behaviour identical to what it was before the fix" is unfalsifiable on this corpus rather than
verified by it. The corpus cannot tell the restoration from its absence. That is the same shape as
your inert arming-scope half, arrived at from the other side.

On what you actually asked. We did not hit it. At message time arming_postures is in lexical
scope — I confirmed by compiling a version that prints both operands — so we could have enumerated
them and did not. The failure is discipline, not expressibility, which is good news for your
constraint: it is checkable in the common case rather than only in principle.

Where your uncertain case does live in ours is not a set but a commitment. aeeObservedSet is
checked as a digest comparison whose refusal says the value "does not equal the value recomputed
over the carried records". Both operands exist and the comparison genuinely ran, so your rule
permits naming it — but one side is a digest and the membership it stands for is unavailable by
construction: a mismatch means precisely that I cannot say which element differs. batchRoot and
corpusDigest have the same shape. Reaching those needs a clause separate from emptiness: a refusal
may name a comparison against a commitment, and must not describe it as a comparison over a set
whose membership it cannot exhibit.

Which suggests emptiness is the special case rather than the rule. The general form your two clauses
are reaching for is that the set a refusal describes must be the set the implementation
evaluated
— empty is one way to break it, wider-than-evaluated is another and is the one that
actually bit me, and a commitment is a third where no membership is exhibitable at all. Written that
way it stays checkable from outside a rail, since both the described set and the evaluated set are
properties of the run rather than of the author's prose.

Last, the measurement bound that explains why neither of us saw any of it. No vector detects any of
the three; all 250 grade identically before and after, and src/check.rs carries no unit tests of
its own, so the defects live entirely in the free-form reason your manifest now declares informative.
This is the class your reason-parity design exists to surface, and it took your sentence rather than
your corpus to surface it.

All three are fixed, with the message assembly moved into a pure function so a rule the file states
about its own refusals is reachable from a test in that file: conjuncts evaluated individually and
only failures named, the arming clause omitted where its operand set is empty, and the operands
described as the arming records the rows resolve, with their count. Verdicts are untouched, 250/250
at the same pin, reason parity still 69/193 — the whole change is invisible to your corpus, which is
the point. bad-1003 through bad-1006 now emit three distinct strings where they emitted one.

One result from that work belongs to you rather than to me, because it is your inert half arrived at
from the other side. I bite-tested each new test by mutating the property back. Three bite. The
empty-operand-set guard does not: deleting !arming_postures.is_empty() leaves every test green,
because all() is already vacuously true on empty, so no input can distinguish the guard's presence.
Structural zero, not an empirical one. I kept it and wrote the limit down next to it rather than
delete it or let it read as covered, on your own reasoning about the forcible-but-unforced cell —
a guard that reads as forced and is not is worth less than the same guard with its measurement
attached.

One narrowing on your own correction, since it changes what a third party can check. You wrote that
the definite-singular fix is "only in my copy" and that the digest is "over my vendored file, not
over anything you can fetch." The first half holds for this branch — head still reads "both the
arming record's and the pinned networkPosture digest". But the vendored file is fetchable and is
already ahead of it: astrogilda/aee-conformance at 5019931,
spec/predicates/adversarial-execution-evidence.md, 147,709 bytes, sha256 759d2383… matching the
manifest, and it carries the quantifier version together with the paragraph explaining why a
definite singular reads as a promise that a statement carries exactly one. So the text a reader
needs is retrievable and digest-checkable. What dangles is only specUpstreamCommit: 0dbe10bc
resolves in neither in-toto/attestation nor your fork, so the vendored text cannot be tied back to
the branch it claims to represent. Reproducible and traceable-to-the-artifact-it-names come apart
there, which is worth separating in the record rather than conceding both.

One retrieval caveat I hit while re-running, and it is the same trap one commit further out. Suite
commit 5019931 is on no ref: git clone cannot reach it, and git fetch origin 5019931… can. My
CI passes because actions/checkout fetches the SHA directly, so a reproducer following the CI path
succeeds while one following git clone && git checkout fails. Worth a ref if you want the pinned
revision reachable the way a reproducer reaches things — I hit the identical trap on my own side and
repointed a record for it.

The fix and its tests are at Rul1an/aee-checker#16, with the bite results in the description.

AI-assisted; I ran the reads, the runs and the mutations, and am responsible for the claims.

@zlhk100

zlhk100 commented Aug 22, 2026

Copy link
Copy Markdown

@astrogilda asked me to read the substrate half with a custody eye. Against 0dbe10b. Section references are to "Three Jobs, Not One" (Zenodo 10.5281/zenodo.21935891 v6), which sets out the threat model this predicate is written against.

Two points:

  1. A kernel-vantage monitor is not trustworthy under your own threat model.
    §3.1 grants the attacker arbitrary system calls beneath any guard, and names the kernel interfaces beneath the host process among the surfaces it may attack. So a monitor whose signing key lives in the in-kernel keyring shares a failure domain with what it watches, and one privilege escalation puts observer, key and artifact together — Claim 1. A microVM monitor does not have this problem, because guest-to-hypervisor escape is out of scope.
    §4.5 already says it: Class 5 carries Class 2's failure mode under kernel compromise. Both configurations satisfy "MUST NOT be accessible to the subject artifact", and only one of them survives the attacker.

  2. The signed record does not say which kind of monitor produced it.

Both emit "attested". Even with a pinned key, the attestation itself says nothing about where that key sits. A consumer that provisioned the deployment already knows; one that did not — the third-party reader Definition 6 is written for — cannot tell whether the evidence came from a monitor your model supports or one it defeats.

Not asking for a new field — you already carry two closed axes and a third costs real complexity. Whether this belongs on the wire, in consumer key policy, or simply as a stated limitation is your call.

elang2 added a commit to elang2/attestation that referenced this pull request Aug 23, 2026
Revise the AI Agent Action predicate based on detailed review feedback:

- Add checkpoint and chain_break as action.type values with sub-schemas,
  addressing the tail truncation detection gap
- Add parties array with witness/asserter roles for field provenance
- Split canonicalization: signing tuple-array (M/L-tagged) for chain
  integrity, RFC 8785 JCS for content digests (float-safe for MCP payloads)
- Document genesis convention (previousHash: "genesis") and chain_break
  requirement for crash recovery
- Add I-JSON safe integer bound on all integer fields (RFC 7493)
- Add 128-level depth bound on extensions with counting rule per in-toto#570
- Replace placeholder digests with fully recomputable worked example
  (every digest has a shown preimage, verifiable against conformance vectors)
- Add Security Considerations section
- Move listing to community contributions per ITE-63 process
elang2 added a commit to elang2/attestation that referenced this pull request Aug 23, 2026
Revise the AI Agent Action predicate based on detailed review feedback:

- Add checkpoint and chain_break as action.type values with sub-schemas,
  addressing the tail truncation detection gap
- Add parties array with witness/asserter roles for field provenance
- Split canonicalization: signing tuple-array (M/L-tagged) for chain
  integrity, RFC 8785 JCS for content digests (float-safe for MCP payloads)
- Document genesis convention (previousHash: "genesis") and chain_break
  requirement for crash recovery
- Add I-JSON safe integer bound on all integer fields (RFC 7493)
- Add 128-level depth bound on extensions with counting rule per in-toto#570
- Replace placeholder digests with fully recomputable worked example
  (every digest has a shown preimage, verifiable against conformance vectors)
- Add Security Considerations section
- Move listing to community contributions per ITE-63 process
elang2 added a commit to elang2/attestation that referenced this pull request Aug 23, 2026
Revise the AI Agent Action predicate based on detailed review feedback:

- Add checkpoint and chain_break as action.type values with sub-schemas,
  addressing the tail truncation detection gap
- Add parties array with witness/asserter roles for field provenance
- Split canonicalization: signing tuple-array (M/L-tagged) for chain
  integrity, RFC 8785 JCS for content digests (float-safe for MCP payloads)
- Document genesis convention (previousHash: "genesis") and chain_break
  requirement for crash recovery
- Add I-JSON safe integer bound on all integer fields (RFC 7493)
- Add 128-level depth bound on extensions with counting rule per in-toto#570
- Replace placeholder digests with fully recomputable worked example
  (every digest has a shown preimage, verifiable against conformance vectors)
- Add Security Considerations section
- Move listing to community contributions per ITE-63 process
@astrogilda

astrogilda commented Aug 25, 2026

Copy link
Copy Markdown
Author

@Rul1an, @zlhk100: both of you are right, and in one case righter than you claimed.

Rul1an

You are right on all three. The third one is aimed at my text, so I checked it against the tree.

"carried arming" is not in the specification. Zero hits across all four files this PR changes, on three search shapes: the literal phrase, a loose carr\w*\s+(the\s+)?arming, and the phrase again after collapsing every run of whitespace to a single space so a line break between the two words could not hide it. Controls in the same run: carr\w* returns 246, arming returns 51. So the empty result is a real negative and not a broken read. The phrase is your implementation's invention, and you found it by applying my sentence to your own code, which is the part I would not have got to on my own. My recollection of what I wrote was not going to settle any of it.

The narrowing you concede is the one my text already makes. The equality in my sentence is scoped at SPEC:1364-65 to "the aeePostureDigest of every arming record the row resolves", and SPEC:1370-73 says outright that which arming records supply the set on a check that reads no row "is not stated here and is not settled by it". I added that last sentence in this PR's head commit, so you are quoting a concession I wrote three days before you needed it.

For arming records the set question is already moot on any valid statement. SPEC:1327-28 requires every arming payload to carry an aeePostureDigest equal to the pinned networkPosture digest, and SPEC:595-98 evaluates kind constraints over every carried record that binds to the run "whether or not any row resolves an observationRefs index to it". A record violating its kind constraint covers nothing (SPEC:1344-47). So every carried arming record already equals one pinned value; whichever subset a no-row check chose, they agree, and the ambiguity cannot be reached through them. You did not claim that, and it halves your own finding in your favour.

It is the seal where this is open, and that is a real hole. Compare the two kind constraints: the arming bullet carries its equality clause inline at SPEC:1327-28, and the sealed bullet at SPEC:1332-33 requires aeePostureDigest as a member and states no equality at all. The seal's equality to the pinned digest exists only inside the row-scoped sentence. On a check that reads no row, nothing compares the seal's run-end posture to anything. I would rather have that written down as the residue than the version I was defending.

On your three reporting defects: I have no argument with any of them, and the short-circuit one is the same complaint I made about one name covering three kinds, one level down and in my direction. The 22-of-66 empty-operand measurement is the kind of thing I should have asked for and did not.

zlhk100

Right on all four legs, and the fourth is the one that costs us something.

§3.1 does grant arbitrary system calls beneath any guard and does name the kernel interfaces beneath the host process among attackable surfaces. The trust-domain definition then licenses your inference directly: a process, privilege or address-space boundary between a component and a record "does not alter the result", and components in one trust domain fail together. §4.5 puts it more strongly than you did. "A kernel privilege escalation collapses the observer and the observed into one trust domain", and "Once a workload reaches Ring 0, it also reaches the observer". Your quote drops the flattering half of that sentence.

On the wire your reading is exact. basis: substrate names a class of vantage and says so: "not the identity of the enforcing substrate", with syscall supervision enumerated by name as qualifying. The evidence tier at SPEC:766-74 derives attested from a signature verifying against a key the consumer's policy names, and key location is not an input to that function. The discriminating fact lives in consumer key policy (SPEC:1197-98), which is exactly what a Definition 6 reader does not have.

There are three closed axes now, where you counted two: basis, method and attribution, all REQUIRED, per SPEC:1093-94; attribution became normatively read in this revision. And at the revision you read, SPEC:1704 still said "The two axes this predicate does order", which was stale against SPEC:1063 in the same document. That one is against us: an internal inconsistency in the PR, independent of your comment, and I would not have gone looking for it if you had not made me count the axes. It is fixed below.

Appendix E of the paper already states your finding as a general rule: "A reader who cannot tell which method produced a record must treat the record's independence claim as unproven." §4.4 levels the same complaint at a commercial product and calls it "the check a buyer should ask for". So you have not found a gap in the argument; you have found the argument applied to my own wire format, which is worse for me and better for the document.

The asymmetry worth naming: the spec states the non-identification as a design intention at SPEC:998-1002, and its residuals section at SPEC:663-760 lists four things the 0.7 commitments do not close, none of which is vantage-class opacity. The paper says it three times and the spec never says it as a limitation. That is the fix I owe, and I agree with you that it does not need a new field to make.

You said the placement is my call. I took the third option you offered, a stated limitation in the residuals list, plus a pointer to the refinement path the spec already carries at SPEC:775-78, where consumer policy MAY subdivide attested into stricter refinements such as requiring a hardware-attested observation key. That names the escape without spending an axis on it.

Pushed as a4cb887

  • The sealed kind constraint now carries the same equality the arming bullet has, inside the same MUST carry scope, so the no-row case is settled on both sides rather than one.
  • The axis sentence is corrected to three. It now reads "defines" instead of "orders", because writing that the predicate orders three axes would have been a fresh error: pinned "does not make the row's method stronger, does not raise its evidence tier, and does not enter the result recompute except through the fail-closed arm every required row member with a closed vocabulary shares", and both SPEC:766-68 and SPEC:1058 say "either strength ordering". Three axes with normative readers, still two orderings.
  • Vantage-class opacity is now a fifth residual, placed after the "One limit is common to all four" capstone so the section's existing counts stay true, and opening by saying it belongs to no member.

None of it needs a new member on any closed vocabulary. The residual says why a carried value would not help: a vantage-class member would be a producer assertion about the producer's own stack, exactly as forgeable as the rest of the payload, and it would state at the predicate level a thing the consumer's key policy already decides.

Edited 2026-08-25. The quotation of the pinned sentence above was cut before its final clause. It now runs to the end. The omitted words say that pinned does enter the result recompute through the fail-closed arm, so cutting there made the value look more inert than the text does, and it cut in favour of the point I was making. Correcting it here rather than in a reply, so nobody reads the shortened version first.

Edited 2026-08-31: prose and formatting only. No SPEC line reference, quotation, commit or claim changed; some repeated field names lost their backticks after first mention.

@Rul1an

Rul1an commented Aug 25, 2026

Copy link
Copy Markdown

Re-read a4cb887 against Rul1an/aee-checker main at 25b9dfa.

The seal side is closed. With the equality now inside the sealed kind constraint's MUST carry scope, the no-row sweep has a specified comparand on both sides; the pinned-posture check our implementation already applies there no longer depends on an unwritten row-scoped reading. No checker behaviour changes as a result.

Your zero-hit result for "carried arming" is also right: the phrase was ours, not a quotation from this specification. We used it to name the wider quantifier reading while rejecting it, and recorded that the corpus could not distinguish that reading from the narrower row-resolved one. The current checker no longer emits that phrase after the reporting fix; it remains only in historical, digest-pinned records and explanatory tests/comments.

Your narrowing of the arming half stands, and we had not claimed otherwise. Thanks for checking this against the tree rather than recollection.

elang2 added a commit to elang2/attestation that referenced this pull request Aug 27, 2026
Revise the AI Agent Action predicate based on detailed review feedback:

- Add checkpoint and chain_break as action.type values with sub-schemas,
  addressing the tail truncation detection gap
- Add parties array with witness/asserter roles for field provenance
- Split canonicalization: signing tuple-array (M/L-tagged) for chain
  integrity, RFC 8785 JCS for content digests (float-safe for MCP payloads)
- Document genesis convention (previousHash: "genesis") and chain_break
  requirement for crash recovery
- Add I-JSON safe integer bound on all integer fields (RFC 7493)
- Add 128-level depth bound on extensions with counting rule per in-toto#570
- Replace placeholder digests with fully recomputable worked example
  (every digest has a shown preimage, verifiable against conformance vectors)
- Add Security Considerations section
- Move listing to community contributions per ITE-63 process

Signed-off-by: Elan Ansrinivasan <5340827+elang2@users.noreply.github.com>
elang2 added a commit to elang2/attestation that referenced this pull request Aug 27, 2026
Revise the AI Agent Action predicate based on detailed review feedback:

- Add checkpoint and chain_break as action.type values with sub-schemas,
  addressing the tail truncation detection gap
- Add parties array with witness/asserter roles for field provenance
- Split canonicalization: signing tuple-array (M/L-tagged) for chain
  integrity, RFC 8785 JCS for content digests (float-safe for MCP payloads)
- Document genesis convention (previousHash: "genesis") and chain_break
  requirement for crash recovery
- Add I-JSON safe integer bound on all integer fields (RFC 7493)
- Add 128-level depth bound on extensions with counting rule per in-toto#570
- Replace placeholder digests with fully recomputable worked example
  (every digest has a shown preimage, verifiable against conformance vectors)
- Add Security Considerations section
- Move listing to community contributions per ITE-63 process

Signed-off-by: Elan Ansrinivasan <5340827+elang2@users.noreply.github.com>
astrogilda added a commit to astrogilda/agent-evidence-vectors that referenced this pull request Aug 27, 2026
VENDOR-PIN.json named in-toto/attestation and left ref empty. The commit
it pins is not in that repository: a plain clone of it resolves neither
0dbe10bc nor 639ec56c, while the same clone resolves its own HEAD, and a
clone of astrogilda/attestation resolves 0dbe10bc on branch
predicate/adversarial-execution-evidence, where it is the direct parent of
a4cb887 and its spec file is 147709 bytes hashing 759d2383, byte-exactly
the pin's own specDigest. So the digest was right and the address was
wrong, and a reproducer following the pin arrived at a repository the
bytes are not in.

The cause is one field answering two questions. A pull request is REVIEWED
in the upstream repository and opened FROM a branch in a fork, and
upstreamRepo was being read as both. It stays as the review venue, because
gen_manifest.py builds the citation in-toto/attestation#570 out of it and
that citation is correct. Where to fetch becomes commitRepo, ref and
refKind, and all three are derived from the checkout's remotes rather than
typed, for the same reason the commit already was.

vendor-spec.py now refuses to write a pin whose commit is not reachable
from the ref it names. That refusal fired on its first run against a real
tree: the local branch is one unpushed commit ahead of the fork, so
vendoring from it would have pinned a commit no reproducer could fetch.
--at separates the commit vendored from the ref that contains it, which is
the situation here, since the corpus certifies against an ancestor of the
branch tip.

refKind is the part that says the pin is currently-true rather than
permanent. A branch head moves and this one already has. The tag that
fixes that is a remote write and is left for the operator, with the
commands in TODO.md. Dry-running those commands first is how the
annotated-tag peel bug surfaced: rev-parse on an annotated tag returns the
tag object, git show dereferences it, so the digest check passed while the
pin recorded an id that is not a commit.

The two documents that quote the provenance are regenerated from their
generators. Both said "upstream commit <sha>" beside a tracksUpstream of
in-toto/attestation#570, which reads as an instruction to fetch from
there; both now name the fetchable location and the review venue
separately.

Staging the pin in the forcing gate's test rig is the other half. The gate
reads a file the rig did not copy, so every rendering case died on a
missing file and reported that as its own verdict: the absent-prior case
failed saying the prior record had not stopped the run, when the run had
stopped one file earlier. The gate also refuses now instead of raising,
because a traceback exits 1, which is this gate's code for a stale
document.
@zlhk100

zlhk100 commented Aug 27, 2026

Copy link
Copy Markdown

Thanks — the limitation as written reads correctly, and the vantage-class decline is a reasonable place to land it.

One data point you may already know, in case it's useful. SLSA meets both of your objections and lands the other way: builder.id is a producer-supplied string naming the platform rather than the key, and the spec keeps it REQUIRED even if it is implicit from the signer. It also asks that modes with differing security attributes each carry a different id — GitHub-hosted versus self-hosted runners is the worked example — to minimize the risk that a less secure mode compromises a more secure one.

Not arguing it's the better call here; builder.id is self-declared and carries the same forgeability you name. Only that neither forgeability nor overlap with key policy settled it in that predicate, which I found interesting given the family.

Happy to leave it there. Good luck with the vetting.

elang2 added a commit to elang2/attestation that referenced this pull request Aug 28, 2026
…JSON

Adopts the canonicalization and chain-shape replacement prose contributed
in review by Sankalp Gilda (@astrogilda), adapted from the text of
in-toto#570.

- bad-101..bad-104: the chain hash preimage is now the record canonical
  form: RFC 8785 (JCS) over the complete audit record including its
  attestation member. Producers MUST write the JSONL line as exactly these
  bytes; verifiers MUST recompute and reject on byte mismatch, fail-closed.
  JSON.stringify is banned from deriving the record canonical form.
- bad-105: strict I-JSON statement-wide. Duplicate members at any depth
  reject fail-closed; well-formed-string rules on raw bytes and \u escapes;
  the 128-level depth bound now covers the whole record.
- bad-107: checkpoint linkage wired. Every record type carries
  predicate.chain.previousHash; checkpoint.previousHash restates the head
  and MUST equal it; deleting a checkpoint now breaks documented linkage.
- Unnumbered findings: previousHash constrained to lowercase 64-hex or the
  literal genesis; second-genesis detection upgraded SHOULD -> MUST reject;
  content digest preimages pinned (params member for requests, result
  member for success responses, error member for error responses); floats
  permitted in content payloads only; the signing-form field list
  enumerated in the spec text for all three record types.
- Widened the tool_call signing tuple to cover type, errorClass, the
  content digests, attestorVersion, and configHash (adopting the reviewer's
  proposed additions), and added the Underlying record shape section
  pinning record-vs-Statement membership and the three protection layers
  (signing tuple, chain hash, DSSE envelope).
- Hardening from adversarial self-review: RFC 2119 requirements notation;
  attestation byte encoding pinned (lowercase 64-hex HMAC-SHA256, 128-hex
  Ed25519); malformed JSON-RPC responses recorded with success false and
  no response digest rather than suppressed; predicate.chain REQUIRED on
  tool_call and checkpoint records (null-priorHead chain_break is the
  single legitimate omission); chain_break prior* members always present,
  explicit null when unknown; id pinned as opaque, at most 128 bytes,
  unique per chain; JCS string rules applied universally in the signing
  form; protocol and upstream.transport declared Statement-only,
  DSSE-covered annotations with fixed v0.1 vocabularies.
- Conformance corpus subsection pinning astrogilda/aee-conformance, with
  the conformance MUST binding at the pin regenerated against this text.
- Security Considerations: planted-break residual risk named with three
  implementable mitigations; signature-scheme trust model documented
  (Ed25519 for attestor accountability, HMAC-SHA256 only inside a single
  trust boundary).
- Extensions retention pinned: post-signing stripping is forbidden (it
  corrupts the chain preimage); a never-inlined workflow emits
  extensionsDigest with extensions absent at emission time. Scope
  semantics clarified: scopes describe witnessing, not signing;
  structural members are emitter-witnessed by construction; unscoped
  fields remain unknown provenance, fail-closed.
- Markdownlint conformance against the repository config: signing-form
  field lists moved to fenced blocks, fence languages and list-marker
  spacing normalized. Checkpoint and chain_break Statement schemas now
  show the metadata block their worked examples carry, and
  decisionContextDigest is pinned to lowercase 64-hex with a
  deployment-defined preimage at v0.1.
- Worked example recomputed under the record canonical form and widened
  tuple, with subject digests fixed to the genesis chain hash on every
  statement in the chain.

Co-authored-by: Sankalp Gilda <23521054+astrogilda@users.noreply.github.com>
Signed-off-by: Elankumaran Srinivasan <5340827+elang2@users.noreply.github.com>
@astrogilda

Copy link
Copy Markdown
Author

Rul1an, four things have landed since your last read: a tag, a repository name in the vendor pin, a digest pin, and the refusal-set clause. I announced none of them. A silent push and no push look identical from outside. The checks are written out below so you can run them yourself.

Start with the suite commit that sat on no ref. You suggested a ref, if I wanted the pinned revision reachable the way a reproducer reaches things. There is one. It went up the same evening: an annotated tag, cited/5019931.

Its message records why. History was rewritten after the revision was published. The commit is an ancestor of nothing. A plain clone still carries it, because clone fetches tags.

I checked that the way a reproducer would, and not the way my CI does. A plain git clone, then git cat-file -e 5019931^{commit}, which exits 0. A bogus SHA in the same clone exits 128. The check is known to discriminate.

On the vendored specification's dangling upstream commit. Your finding was that 0dbe10b resolves in neither in-toto/attestation nor the fork. The real defect was one level up. The vendor pin named a commit. It never named the repository holding it, so a reader had to guess, and the natural guesses fail. be67a74 adds commitRepo: astrogilda/attestation to spec/VENDOR-PIN.json.

A plain clone of that repository reaches the commit. git branch -r --contains puts it on the branch this pull request is opened from. The digest checks out at 147709 bytes, sha256 759d2383. That is the figure you published.

One retrieval caveat worth passing on, because it gave me a wrong answer first. The GitHub API resolves that same SHA under in-toto/attestation as well, since forks share an object store. It answers 200, not 404. So an API lookup cannot settle the question you actually asked. Only a clone can, and the two disagree in the direction that reassures you.

For the agent-action corpus the fix was to stop pinning a commit at all, since its upstream commit was 639ec56. That one is genuinely orphaned. The fork branch was rewritten. A plain clone of elang2/attestation exits 128 on it. That clone's own HEAD resolves.

7aed3cc moves the manifest onto specAuthority: specDigest over vendored bytes in the directory, which the checker recomputes on every run. The orphaned commit is now provenance only, since integrity no longer depends on it resolving. That is stronger than pinning a ref. It stops depending on anybody's history staying put.

Finally, the refusal-set clause, and this is the part I most want you to check. Commit b1513f6 states the general clause in the specification text. Where a refusal names a comparison, the set it names must be the set the implementation evaluated. All three of your shapes are there. Each has its own remedy, and none is folded into a single caveat.

An empty operand set means the comparison did not run. A verifier must not name it. It should report the empty set, which is what it found.

A set wider than the one the check ranged over tells a producer to repair records the check never read. A verifier must not name a wider set. Where the evaluated set is a function of the statement, it should name that set and its count. The arming records a row resolves are exactly such a set.

A comparison against a commitment genuinely ran, and may be named. It must not be described as a comparison over a set whose membership it cannot exhibit. A digest mismatch says the recompute differs, and says nothing about which element differs.

The general form is yours. You wrote that emptiness is the special case, and that the set a refusal describes must be the set the implementation evaluated. I took your sentence over my narrower one, and the commit message says so.

The limit is worth stating too. No vector can enforce any of it. Your own bite test found the reason. Deleting an emptiness guard leaves a suite green, because the enclosing universal is vacuously true on the empty set. The obligation is diagnostic and never a validity rule, and it sits in the paragraph that already carries that hedge.

One thing I have not done, so you do not go looking for it: the vendored copy in the suite is still pinned at 0dbe10b. It carries neither a4cb887's seal-posture equality nor this clause. The pin is deliberate and its digest matches. It moves when the suite re-vendors, which is a separate change from this one. But if you re-read the vendored text expecting the new paragraph, you will not find it there; it is at the branch head.

Sankalp.

@astrogilda

astrogilda commented Aug 28, 2026

Copy link
Copy Markdown
Author

@zlhk100, thank you, and the SLSA point is better than a data point. It counters the reasoning I gave, so I want to answer it directly.

My residual declines a vantage-class member on two grounds. The value would be a producer assertion about the producer's own stack, as forgeable as the rest of the payload. And the discriminating fact already lives in consumer key policy. You have shown me a predicate in the same family where both hold of builder.id, and neither settled it. That is a real problem for the argument as written, because I offered those two grounds as though they were enough on their own.

The practical difference is in what the field is for. That field is a partition key rather than a graded claim. A consumer's policy matches on it, and SLSA keeps it mandatory even when it is implicit from the signer. That is what makes it usable: the field is there to be keyed on, not to be believed. The guidance you quote about modes with differing security attributes is the same thought, since a partition is useless if two modes share a label.

My axes are graded. They feed the evidence tier and the result recompute. A self-declared value in that position would be forgeable in a way that changes a verdict rather than a lookup.

So the correction is narrower than a reversal. I still decline a graded vantage axis. But what I actually wrote argued against any carried value at all, and that is wider than my grounds reach. An ungraded partition identifier is a different proposal, it is the one SLSA validates, and I have not evaluated it. So I will narrow the residual's wording to the graded axis it actually rules out. That is a text change in the residuals section, and it adds no member to any vocabulary.

None of that changes the limitation itself, which stands either way. A third-party reader still cannot tell a kernel-vantage monitor from a monitor outside the workload. An identifier the producer chooses would not by itself let them. It would no more do so than builder.id lets a SLSA consumer judge a runner they know nothing about. What it would give is something for a policy to key on, which is a smaller and more honest thing to claim.

Thank you for reading the substrate half with a custody eye. The comparison to the SLSA family is useful context, and I am glad you raised it.

@Rul1an

Rul1an commented Sep 1, 2026

Copy link
Copy Markdown

Sankalp, I reran these as clone checks rather than API lookups.

  • In a plain clone of astrogilda/aee-conformance, git cat-file -e '5019931^{commit}' exits 0; a bogus 40-hex object exits 128.
  • In a plain clone of astrogilda/attestation, 0dbe10bcc959b63dc42370a5db09812c9476f59a resolves and git branch -r --contains places it on origin/predicate/adversarial-execution-evidence.
  • The specification bytes at that commit are 147709 bytes and hash to 759d2383e5da36fa509dc335e6159a20b87641b25ebbadcf1676c55d75ffd8b0, matching spec/VENDOR-PIN.json.
  • In a plain clone of elang2/attestation, its own HEAD resolves and 639ec56 exits 128.

The refusal-set clause also found a defect in our checker rather than only confirming the earlier fix. Two aeeObservedSet refusals said the value was recomputed over “the carried records”, while the implementation evaluates only carried interception and examination records. We corrected both sites, added behavior-level guards for each refusal, and then an independent reviewer found the first guard was asymmetric: dropping Examination from the production filter still left it green. The fixture now carries both evaluated kinds and also makes widening the filter visible. All four mutations bite independently: two wording regressions, narrowing to Interception-only, and widening to include Sealed. The fix and SHA-bound review are in Rul1an/aee-checker#18; the post-merge provenance binding is in #19.

On the remaining wording question: I found no occurrence of “short-circuit” or “conjunct” in the clause. Our earlier && implementation could emit one byte-identical refusal for four distinct failures because later conjuncts were never evaluated. I read the general MUST as covering that: a refusal cannot name comparisons the implementation did not reach. But that mechanism is not literally one of the three shapes the following sentence enumerates. Are those three intended as non-exhaustive examples under the general rule, or as the complete set of shapes the paragraph means to constrain?

I did not run the current corpus against this checker or derive a number. The checker targets predicate v0.6; the corpus is v0.7 with no alias or dual-accept window, so the type refusal would make such a figure meaningless.

@astrogilda
astrogilda force-pushed the predicate/adversarial-execution-evidence branch from b1513f6 to 7c6499b Compare September 4, 2026 14:03
@Rul1an

Rul1an commented Sep 4, 2026

Copy link
Copy Markdown

The squash is content-neutral, and I checked rather than assumed it: spec/predicates/adversarial-execution-evidence.md is the same blob at b1513f6 and 7c6499b, b315e77b7bf3eb6bdb3516916483a4a96cb5ce47, 150,849 bytes on both. So nothing in my last read moves, and a single commit is the right shape to carry into vetting.

The reachability did move. In a plain clone of astrogilda/attestation today:

  • 0dbe10bcc959b63dc42370a5db09812c9476f59a no longer resolves. Three days ago I reported that it did, and that git branch -r --contains placed it on origin/predicate/adversarial-execution-evidence. That was true when I ran it and is not true now, so anyone re-running those checks at vetting would fail on that line.
  • b1513f6221e0a1ecadc6e6ee44b6f9c2b315a592 no longer resolves either, which is the commit my last comment cites for the refusal-set clause.
  • Both remain fetchable by full SHA, so the objects are there and it is the clone path that misses them. A bogus 40-hex object exits 128 in the same clone, so the check discriminates.
  • git tag -l there returns only v0.1.0 through v1.2.0. The cited/ annotated tag you cut for suite commit 5019931 is the mechanism that carries a commit across a rewrite, and it is not applied in this repository.

The consequence sits in aee-conformance's spec/VENDOR-PIN.json. Its specDigest still validates the vendored bytes, which are the 147,709-byte text at 0dbe10b rather than the head text, so integrity is untouched. But commit now names an object a plain clone cannot reach, and ref with refKind: branch no longer places it on that branch. A reader following the pin as written arrives at nothing; a reader who already knows to fetch by SHA gets there.

That cuts both ways, and my side is the better illustration. My own conformance workflow pins SUITE_COMMIT: 5019931751041c815463faa569fbb159e01612a0 beside the spec digest, and that commit is on no branch either. It survives a plain clone only because of your cited/5019931 tag, and it survives CI because actions/checkout asks the server for the SHA directly. So the mechanism you cut on my suggestion is currently what holds my own pin up, and the digest is the half that carries itself. 7aed3cc already moved the agent-action corpus onto specAuthority for that reason. A commit pin is an address, and addresses fail in more than one way: a rewrite, a wrong repository, an orphaning.

Still open from my last message and unchanged by any of the above: whether the three shapes following the general MUST are non-exhaustive examples under it, or the complete set the paragraph means to constrain. The short-circuit case reads to me as covered by the general clause, but it is not literally one of the three.

Adds the Adversarial Execution Evidence predicate specification and its
protobuf definition, and registers both in the spec and protos indexes.

The predicate records signed, recomputable evidence from executing an
untrusted artifact against an adversarial corpus inside a containment
substrate. A verifier re-derives the reported outcome from the attestation
rather than trusting the party that produced it.

Signed-off-by: Sankalp Gilda <sankalp.gilda@gmail.com>
@astrogilda
astrogilda force-pushed the predicate/adversarial-execution-evidence branch from 7c6499b to 25ac858 Compare September 4, 2026 17:43
@astrogilda

Copy link
Copy Markdown
Author

Non-exhaustive.

The general requirement governs: the set a refusal names must be the set the implementation evaluated. Short-circuiting breaks that directly, since the refusal names comparisons that were never reached. But you're right that your case is none of the three shapes listed. Those turn on set membership. Yours turns on evaluation order.

So I've changed the text to say so, and added short-circuiting as a fourth shape: a verifier MUST NOT name a conjunct it did not reach, and SHOULD name the one that decided the refusal.

Thank you for reporting the aeeObservedSet defect against yourselves.

The residual narrowing I owed @zlhk100 has landed as well. It declines a graded axis only now; the wider claim did not survive builder.id.

I agree on the version point too.

@astrogilda

Copy link
Copy Markdown
Author

The branch is rebased onto current main and squashed to one commit: two new files, the spec and its protobuf definition, plus two registry lines. 2741 additions, no deletions.

@puerco, would you be willing to review? You took SPDX-3 and SVR, and this has the same shape.

@Rul1an has written an independent implementation and re-ran its verification against the conformance suite on 1 September, which turned up a defect in his own refusal wording. @zlhk100 compared the predicate against SLSA, and that comparison produced a correction to the residuals section, which is now in the branch.

One question above is still open: whether the refusal-set clause enumerates its cases exhaustively. I answered it in the thread and changed the text to match. It needs your eye now.

If splitting the commit or reworking the proto would make review easier, say so.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants