[chernistry]

What this changes

Adds section 3.1.4 to spec/trace-v0.2.md, a reproducibility row in the section 3.1 logical-schema table, and a marked change to the appraisal row. Normative and non-breaking: one new OPTIONAL record member, an OPTIONAL appraisal.method, and appraisal.re_execution, present exactly when method is re-execution. No required field changes and the wire format does not change.

The four parts, in the shape ruled on #249 on 3, 6 and 7 September:

1. Claim definition ("Definition" in 3.1.4). Re-executing a named deterministic function of the run, the producer's coordination logic rather than the workload's side effects, over a pinned input closure yields a transcript whose RFC 8785 digest equals the claimed value. Three parts, all explicit in the record: the code and the function it exposes (code_identity, function, and code_resolver where the digest alone does not locate the artifact), input_closure as {id, digest, resolver} entries covering everything the function reads with model calls included, and transcript_digest. A closure that omits anything which can change the transcript makes the claim malformed; the text says that is the definition, not a quality bar, and gives it a consequence: a malformed claim is detected at re-execution as a read beyond the closure.
2. Verifier holdings as a MUST. The implementation at the pinned digest, every closure blob, and the claim itself, each with its own bar: availability for the implementation, which is shipped software and can be required to be publicly obtainable; integrity for the closure blobs, each matching the digest the producer signed, since a run's closure is run-private by construction and a producer being its only retainer is within §3.1.2; and no bar for the claim, which is signature-covered. "If re-execution requires state that only the producer's environment can supply, it is not reproduction" is in the text close to verbatim, with its operational form: a verifier supplies the function nothing but the closure, and a read beyond it, refused or let through, fixes the outcome at not-attempted with the read named, whatever the re-run would otherwise have produced.
3. Tri-state outcome. reproduced; diverged, which MUST record the verifier's observed digest; not-attempted, which MUST carry the reason. not-attempted MUST NOT be reported as either of the other two. It has a row of its own in the outcome table rather than a trailing sentence.
4. appraisal.method: "re-execution", with the outcome scoped under it in appraisal.re_execution. appraisal.status is untouched and stays the closed EAR set spec: where a verifier records an unresolvable citation: the cross-surface question from #187's review #190 holds. The section states why not-attempted is not status: none, so the two are not collapsed later as a tidy-up.

Also in the text, from @lywinged's review on the issue: one OPTIONAL member of the result, verifier_code_identity, carried on any outcome so that results which disagree can be read together, with the two-row reading table and the statement that the verifier's own digest carries no weight singly. It adds no requirement; it gives a divergence a correlation key. (resolved_closure_digest was in the first cut and is withdrawn: the read-beyond case it existed to detect is now fixed at not-attempted by the holdings rule, and the field could neither express a read of something with no id nor name its own preimage.)

A closing paragraph states how the two recomputable commitments a software-only record can now carry, runtime.measurement over the preimage its producing profile documents and transcript_digest over the preimage this section fixes, sit together: different objects, neither outcome implies the other, checked separately unless the profile says its measurement preimage is a function of the closure.

Deliberately not in this PR

• Schema, models.py, docs/schema.md. They track the text once it is agreed, as a follow-up that needs no sponsor (CONTRIBUTING: schema changes tracking a merged spec change). Until then a record carrying the member does not validate against additionalProperties: false, which is the right order: the text decides the shape and the schema follows it. The interval is filed as a defect with its severity per the Four surfaces state the rules and nothing says which wins: schema, reference model, normative spec and docs disagree #247 ruling, so it does not stop being read on merge.
• Producer vectors. Records carrying the claim, and appraisals that re-ran it, follow with the schema change. A vector that cannot validate is not yet a vector.
• Journal format, transcript shape, how a closure is stored and resolved. The annex on Vendor platform annex: software-only deterministic multi-agent orchestrator (Bernstein) #231, sequenced after this. The text cites "the profile or annex that describes the function" without a section number, so it does not depend on §4.4's scope sentence, which no maintainer has ruled on.

Type of change

• Non-breaking spec change (new optional field)

Spec section

Section 3.1 (table) and the new section 3.1.4. Also CHANGELOG.md and two glossary entries (docs/glossary.md).

Checklist

• DCO sign-off on all commits
• CHANGELOG.md updated, crediting the sponsorship arrangement
• New normative text marked with <!-- CHANGED: #249 -->; the one modified normative line (the appraisal row) carries a marker too
• python tools/check_dashes.py clean, pytest 1655 passed

Sponsorship

Carried by @imran-siddique as sponsoring maintainer, per the ruling on #249; the writing and the authorship are mine. This is the PR from the 13 September check-in. The two other items on me, the #247 coverage guard (#365) and the #245/#231 producer-side vector (posted on #231), do not gate this.

Refs #249, #231. #279 quotes the shape and does not gate this either.

[github-actions]

🟡 Contributor Check: MEDIUM

Check	Result
Profile	MEDIUM
Credential	LOW
Overall	MEDIUM

Automated check by AgenTrust Contributor Check.

[lywinged]

Verdict: Request changes. Two blocking findings. The first needs a decision I cannot make for you. The second is one clause, in two places.

Reviewed at 54bdd82, base cd92e16. Read first: #249 and #231 in full, which gives the 30 August ruling, the 3 September ruling with its placement decision, your 6 September acceptance, the 7 September confirmation and the 13 September check-in; #247 and #190 in full; and #279, #245 and #240 as bodies. The last of those is the one that changed something, below.

1. A read beyond the closure has three dispositions across four sites, and the field that would settle it cannot express the observation, over bytes the section never names

Three dispositions, across four sites. Line 243, rule 1: the claim is malformed, with no outcome attached anywhere in the section. Line 253: "the outcome is not-attempted, with the read named as the reason". Line 260, the diverged row: "producer tampering, verifier drift and an under-pinned closure are indistinguishable". And line 271, reading-table row 1, which is not a fourth disposition but the reading taken off a diverged result: resolved_closure_digest differing is read as "under-pinned closure". Line 263 then forbids not-attempted and diverged being interchanged, so an implementer cannot satisfy both readings.

The sharpest way to see it: computing resolved_closure_digest requires the verifier to have observed every input the function read, and a verifier that has observed that has observed the read beyond the closure, which line 253 makes not-attempted. So the under-pinned reading at row 271 can never be delivered for the case it exists to detect: whenever the function reads beyond the closure, line 253 has already fixed the outcome at not-attempted, and line 263 forbids reporting that as diverged.

Row 271 does stay reachable, and the ways it is reachable are ways of being wrong. The clean case is the array ordering set out below: two verifiers with identical reads can compute different digests, and one of them lands on a row that says the producer under-pinned. A second case is a claim that pins an input the function does not read. Rule 1 at line 243 makes only omission malformed, and nothing in the section disposes of the reverse, so if the transcripts differ for any other reason the result is diverged with resolved_closure_digest differing and the row calls a producer under-pinned who over-pinned. You may read line 238's "the complete content-addressed set of everything function reads" as excluding that by definition, and if so the answer is that it has no disposition rather than that it cannot happen, which is the same gap one level up.

Either way line 267's "exactly when" holds in one direction only: a read beyond the closure does make the digests differ, and differing digests do not imply such a read. Line 282 lists both optional members on the result generally, with no outcome condition, unlike observed_digest and reason in the same row, so the fix may belong at 267 rather than at 253.

And the field cannot carry the observation either way, which is the half with no cheap answer.

Line 267 defines resolved_closure_digest over "every input the function read, content-addressed the same way as input_closure". Closure entries are {id, digest, resolver} with resolver required. The case this field exists for is a read of something the claim did not pin: a clock, an environment variable, a socket, none of which has an id in a resolver's system or a party obliged to retain it.

Then the pre-image. Line 267 compares against "the digest of the claimed closure", and no member carries such a digest: reproducibility has function, code_identity, input_closure and transcript_digest and nothing else. So a verifier computes it, and the section never says over what bytes. Three candidates, whole entries with their resolver strings, {id, digest} pairs, and the digests alone, give three answers. resolver is producer-chosen and a second verifier may legitimately resolve from a mirror, which is a fourth. And input_closure is an array: §3.2.2 canonicalises object keys and says nothing about array order, the claimed closure's order is fixed by the signature and the resolved closure's is specified nowhere, so read order, declared order and any concurrent interleaving give different digests over an identical set of reads. Every one of those lands on row 271, the only row that says the producer under-pinned.

On #249 I asked for "a digest of the closure manifest as resolved" and you took the phrase up as a heading. The word manifest is where the pre-image was going to be pinned, and it did not survive into the text.

One thing to watch in whichever fix you take. Deleting line 253's consequence on its own leaves a hole: a function that reads an unpinned input and still produces the claimed transcript, a TZ it ignores or a clock it never writes down, completes with matching digests, and the only outcome the table then permits is reproduced, on a claim rule 1 calls malformed. The disposition has to cover the read-beyond case under both digest outcomes, which is also what gives rule 1's malformed the consequence it currently lacks.

Saying where the disputed clause came from, because it changes whose call it is: the not-attempted consequence is not in the 3 September ruling, which asks for the verifier-holdings sentence "close to verbatim" and stops there. It is your own extension, stated deliberately in the PR body, and entirely yours to withdraw.

2. The independence bar is stated once for three holdings that need different answers

Lines 247 to 251, your preamble to the sentence that was ruled:

A verifier MUST hold three things before it reports any outcome other than not-attempted, and none of them may be supplied by the producer's environment:

• the implementation at code_identity, obtained as a public artifact;
• every blob in input_closure, each resolved through its own resolver and each matching its own digest;
• the claim itself, from the signed record.

The ruled sentence is the one at line 253, "If re-execution requires state that only the producer's environment can supply, it is not reproduction", and you reproduced it close to verbatim as asked. The trouble is in the summary above it, which was nobody's ruling.

Taken literally the clause does not hold on its own third bullet, since the claim comes from the signed record and the record is the producer's output. There is a reading that saves it, where the umbrella is specialised by each bullet's own qualifier and "the producer's environment" means live state at re-execution time, which is what 253 says. So this is ambiguity rather than falsity, and the cost is in what the literal reading does to the second bullet.

That bullet gets no independence bar of its own. code_identity gets one twice, at line 237 ("MUST resolve to an artifact a verifier can obtain without the producer") and at line 249 ("obtained as a public artifact"). For input_closure the section says only that each blob is "resolved through its own resolver", and line 238 sends the reader to §3.1.2 for that field. §3.1.2 line 195, in bold and under its own heading: "resolver names who must retain, not who adjudicates … Naming yourself as the party who must retain an artifact is ordinary and non-circular … An operator naming themselves as resolver for their own artifact is therefore within this section". §3.1.2's rule 4 at line 189 looks like the bar, since it forbids a "self-asserted resolver", and the paragraph just quoted disposes of that reading too, in its last sentence: "Rule 4 is aimed at a producer who can name no obliged party at all, not at one who is that party."

So either the preamble governs, and a producer that is the only party holding its run closure gets not-attempted on every verification for ever, because line 247 permits no other outcome when the holdings fail; or §3.1.2 governs, and the clause is decorative for two bullets of three.

The asymmetry that resolves it is availability rather than integrity. An implementation is shipped software and can be required to be publicly obtainable. A run's closure is run-private by construction, and a producer being the only party that holds it is not a defect, so the only independence available for it is that the verifier can check what it got against a digest the producer signed. That is a different requirement from the one code_identity carries, which is why one clause cannot state both.

So the ask is to state the bar per bullet rather than once above all three: public obtainability for code_identity, integrity against a producer-signed digest for input_closure, and for the claim itself no bar at all, since it is signature-covered and coming from the producer is the point of it.

Four surfaces carry the clause, and two are outside the diff: spec/trace-v0.2.md:247, CHANGELOG.md:16, the commit message, and part 2 of the PR body. The last I cannot edit from here, so it needs an exact find-and-replace from you.

Smaller

The section's first sentence narrows software-only. Line 228: "defined by what it lacks: nothing measured the execution, and the party asserting the evidence also wrote it." §3.1.1 line 143 gives those as two alternative cases, not two properties of one: "the correct value for a dev-mode record, where nothing attested the execution, and for a record transcribed from another vendor's control plane, where the party asserting the evidence also wrote the log." §3.1.1 also defines log-import at line 156, a SIEM export or an audit trail, where the importer is by construction not the party that wrote the log, and line 158 makes such a record MUST-carry software-only. The conjunction is false of a whole origin.kind.

The changelog inverts a prohibition into a permission. CHANGELOG.md:16 reads "not-attempted may be reported as neither of the other two". Line 263 states two MUST NOTs and the PR body has it right; the commit message does not state the prohibition at all, so this is a one-file fix. One word, and it is the release-note summary of the requirement the whole #279 pattern exists to protect.

Three parts, four required rows, on one surface only. "The claim has three parts, all explicit in the record" sits over a four-row table. CHANGELOG.md and the PR body both nest function under code_identity already, which is one of the two fixes and the one I would take. Keeping the field is right: it carries "a named deterministic function" from the ruled definition.

input_closure's shape is wrong by one member. "the shape §3.1.2 uses without rel" is four members, not three: §3.1.2's entry is rel, id, resolver, retention, digest. The text names the digest override and not the retention omission. Dropping retention is defensible, since §3.1.2 flags it under "Unsettled, and deliberately named rather than hidden" and nothing in 3.1.4 uses it, so this is one clause: "the shape §3.1.2 uses, without rel or retention, with digest required on every entry."

code_identity also has no resolution path. Beyond the two bars in finding 2, there is no field to resolve it through while every closure entry has one. I looked before raising it: build_provenance.provenance_uri is documented at docs/schema.md:158 as "URI to the SLSA provenance document", an attestation about the artifact rather than the artifact, and §3.3.1 at surface has the verifier check digest against an artifact it "independently held". A sibling code_resolver, or making code_identity an object, would close it; it is a scalar digest today, so a member cannot hang off it. Not reopening the verifier-holdings rule ruled on #249: the sentence at line 253 is right, and neither this nor finding 2 touches it. Both are gaps on the bullets it summarises.

What diverged does to appraisal.status, raised as a question rather than a block. Line 265 imports "the verifier fails the appraisal" from §3.3.1, where the only place that phrase is given a value is lines 486 to 487, attached to a different trigger. Line 284 says appraisal.status is untouched, and the example at line 306 sets contraindicated. affirming is decided, since nothing reads it as failing; what is not is warning against contraindicated. I am not asking you to settle it: the hole is in §3.3.1 and predates your text, and the 3 September ruling says "Take the method discriminator. Do not touch appraisal.status", which is what line 284 does. Raising it for @imran-siddique rather than for you.

The one modified line in the diff carries no marker. The appraisal row at line 130 is the only normative line this change edits rather than adds, and CONTRIBUTING.md:67 says to mark changed normative text, not only new normative text. Stating it accurately, since I had it wrong in an earlier draft: all four pre-existing markers sit on added text, so this would be the first marker in the file on a modified line, which is presumably why nobody has done it. (.github/PULL_REQUEST_TEMPLATE.md:21 states the same rule with a colon instead of a hyphen and scopes it to breaking changes only, so the two disagree. Not yours, and a #247-class instance in the file a contributor is told to follow.)

§4.4's text is narrower than the ruling behind it, and the gap is narrower than I first wrote. The annex itself is settled: @imran-siddique accepted it on #231 on 30 August and reaffirmed it on 3, 7 and 10 September. What no maintainer has ruled on is §4.4's scope sentence, which still reads "one per silicon-root and cloud-attestation surface" at line 722 over five hardware co-editor slots, with CONTRIBUTING.md:87 pointing at it. You raised that on #231 on 27 August and I raised it again on #249 on 31 August; none of the maintainer comments on either thread answers it. §4.1 line 690 already cites §4.4, so this is not the first citation, but it is the first normative text to depend on that sentence. Citing "the profile or annex that describes the function" without the section number decouples you from an edit that has not happened.

The out-of-scope sentence defers to a question that was closed ten days ago. Line 317 says "runtime.measurement is unchanged, and its meaning under software-only is a separate question", and the body cites #240 for it. #240 closed on 6 September, by #242, and docs/trust-levels.md:29 on your own base now states that meaning: "Under software-only, the field is not a hardware measurement: it is a software commitment defined by the producing profile ... and that profile must document its preimage so a verifier can recompute it. All-zero is reserved for a producer that has no commitment to offer at all."

So the premise of the deferral is stale, and the thing underneath it is worth a sentence rather than a pointer. After this section a software-only record can carry two producer-defined recomputable commitments: runtime.measurement, whose preimage the producing profile documents, and transcript_digest, whose preimage this section fixes. They commit to different objects, inputs and state against the coordination function's output, and nothing says how a reader should take them together or what a reproduced outcome implies about the first. This is not hypothetical for the reference implementation either: #242's own body says both shipped adapters "deliberately emit non-zero, documented measurements under software-only", and sandbox.py:413 and agt.py:160 do exactly that. You are the producer who now has both digests, so you are the person who can say in one line how they sit together.

function delegates its invocation convention out of band. The row says the implementation's own documentation defines how a verifier invokes it. That document is not content-addressed and not in the closure, so a verifier holding all three required things still needs something from the producer to begin.

Two claims in the body an approval would co-sign. "two new OPTIONAL appraisal members" is right in JSON Schema terms and reads oddly beside line 284, which makes appraisal.re_execution MUST-present whenever method is re-execution; it is on three surfaces including the commit message. And "two glossary entries, which cite the section so the keyword guard is satisfied" is decorative: docs/glossary.md carries no RFC 2119 keyword at all, so tests/test_requirement_keywords_are_attributable.py never looks at them. I stripped both Defined in §3.1.4 of the specification. sentences and the guard still gives 12 passed.

The schema interval. You disclose it and your reasoning for the order is right. The 11 September ruling on #247 names this condition and gives it a severity ("A schema that is narrower than the spec rejects conformant records. That is a defect with a severity, not a documentation nit, and it should be filed as one"), so it is worth an issue rather than a PR-body paragraph that stops being read on merge. Measured here: examples/amd-sev-snp.json validates clean, adding reproducibility gives Additional properties are not allowed ('reproducibility' was unexpected), adding the two appraisal members gives ('method', 're_execution' were unexpected), and a record omitting the member is unaffected.

A line in a file this diff opens, which is not yours and which I will take. docs/glossary.md:37-38, five lines below your new Input closure entry, says JCS is "Unicode code-point-ordered keys". spec/trace-v0.2.md:395 says "Object keys are sorted by UTF-16 code unit (ascending), per RFC 8785 §3.2.3. This is not the same as Unicode code-point order." It dates to #56, nothing under tests/ reads that file, and it is the distinction your #231 vector turned on this morning. I will send it as a one-line change of my own unless you would rather have it here.

Checked and clean

Four cross-references resolve and say what they are cited for: §3.1.1's closed-set reason at line 152, §3.2.3's rule that an unavailable revocation bundle is reported as an absent check rather than a pass, §3.3.4's receipt_gap_disclosed against receipt_missing_required with "Collapsing them discards the distinction" verbatim, and §3.3.1's contradiction sentence itself. §3.1.2, §3.3.1's applicability and §4.4 are findings above rather than clean. The sha384: alternative is not a new algorithm and the non-breaking box is right. Both new markers match the form of the four already in the file. DCO is on the commit, the changelog entry is under Unreleased and credits both proposer and sponsor, and runtime.measurement appears only inside the out-of-scope sentence. pytest gives 1655 passed and 1 skipped and tools/check_dashes.py exits clean. I also checked "appraisal.status stays the closed EAR set #190 holds", expecting it to over-read an issue whose own text calls itself "a home for the decision, not the decision": it does not. #190 records the enum as closed and parks the question of changing it.

One thing I checked because it looks like a slip and is not: row 3 of the reading table, "no reproducing verifier found a benign explanation", is your own wording from #249 verbatim. Leaving this here so nobody tidies it later.

Not approving, on 1 and 2.

[chernistry]

Both findings taken, at a6480ad. The decision on 1 is made below, and it is mine to make since the clause was my extension.

1. One disposition

A read beyond the closure, whether the verifier's environment refused it or let it through, fixes the outcome at not-attempted with the read named, whatever the re-run would otherwise have produced. That is the single site now. It covers both digest outcomes, which closes the hole you flagged (a TZ the function reads and ignores: the run completed on something the claim did not pin, so it is not the run the claim describes, and the matching digest says nothing). It also gives rule 1 its consequence: a malformed claim is detected at re-execution as exactly that read. Over-pinning gets its sentence: an entry the function does not read is surplus and has no effect.

resolved_closure_digest is withdrawn. You were right on both halves: the case it existed to detect is now decided before any digest is compared, and the field could neither express a read of something with no id nor name its preimage. I did not try to rescue it with a manifest definition, because once the read-beyond case is not-attempted there is nothing left for the field to distinguish. The diverged row's list is now "producer tampering, a function that is not the deterministic one it is named as, and verifier drift". The reading table is two rows on verifier_code_identity alone; row 2 keeps the wording from #249.

2. Per-holding bars

Stated per bullet: availability for code_identity (shipped software, publicly obtainable); integrity for input_closure (each blob matches the digest the producer signed; a run's closure is run-private, and a producer being its only retainer is within §3.1.2, cited); no bar for the claim. The umbrella clause is gone from the spec, the CHANGELOG and the PR body. The commit message at 54bdd82 still carries it; I have not rewritten history on a reviewed branch, and the second commit's message states the correction.

Smaller, all taken except the two you routed elsewhere

• software-only first sentence: "nothing attested the execution", which is the property all three §3.1.1 cases share.
• CHANGELOG: "MUST NOT be reported as either of the other two".
• "three parts" is now named over the table: the code and the function it exposes, the closure, the digest.
• input_closure: "without rel or retention, with digest required on every entry".
• code_identity resolution path: optional code_resolver, resolver in the §3.1.2 sense, omitted when the digest alone locates the artifact. Added as a row, no MUST, so nothing new for the sponsor to answer for.
• function: the invocation convention is part of the artifact at code_identity, content-addressed with it; anything held elsewhere is excluded by the holdings rule.
• Marker on the modified appraisal row. First one on a modified line in the file; the CONTRIBUTING/PR-template disagreement I leave with you.
• §4.4: cited as "the profile or annex that describes the function", no number, so the text does not depend on the scope sentence.
• runtime.measurement: the stale deferral is replaced by a paragraph on the two commitments. As the producer with both digests: they commit to different objects, inputs and state against the function's output; neither outcome implies the other; checked separately unless the profile says its measurement preimage is a function of the closure, in which case one closure pins both.
• PR body: "two new OPTIONAL appraisal members" rephrased to the presence condition; the keyword-guard claim about the glossary dropped, the entries stay.
• Schema interval: filed as Schema narrower than spec after #364: reproducibility and appraisal.method/re_execution rejected #366 with your measurements and the severity from the Four surfaces state the rules and nothing says which wins: schema, reference model, normative spec and docs disagree #247 ruling. I take it after this merges.
• diverged and appraisal.status: left as is, since line 284 does what the 3 September ruling asks and the hole is §3.3.1's. For @imran-siddique.
• Glossary JCS line: yours, thank you. Fewer surfaces here.

pytest 1655 passed, 1 skipped; check_dashes clean.

[chernistry]

One correction on re-reading, at bb29b05: the drift reading compares verifier_code_identity across results that disagree, so the member has to be carried on the reproduced result too, not only on diverged. The sentence now says "carried on any outcome". Also dropped "the one observation", which read as "the only". Nothing else changed.

[lywinged]

Both taken, and the withdrawal was the harder of the two calls. Rescuing resolved_closure_digest with a manifest definition was available and would have looked like progress. Taking it out, because the case it existed to detect is now decided before any digest is compared, leaves less to go wrong, and it is more than I would have insisted on.

Re-measured on bb29b05. The member is gone from the spec and the changelog, and the body records the withdrawal. The diverged row no longer lists the cause that is now not-attempted, and the one it gained, a function that is not the deterministic one it is named as, belongs on that list. reproduced and diverged both now say "on the closure alone", which ties them to the holdings rule instead of leaving it to be inferred. The three bars read as three different requirements, which is what they are. The changelog modal, the software-only first sentence, the retention clause, the marker on the modified row and the two-commitments paragraph all check out, and citing the profile or annex without a section number does decouple the text from a scope sentence nobody has ruled on.

One thing the tightening opened, and it is one clause.

reproduced and diverged both now require that the re-run completed on the closure alone. The not-attempted row lists four triggers: a blob unresolvable, code_identity unobtainable, the function read beyond the closure, and the re-run not completing. A verifier whose environment let a read through and did not record it cannot establish the closure-alone property, and fits none of the four. The paragraph under the table already decides the case, "an inability to check is reported as that, with its cause", so the outcome is not-attempted by the principle. The row that enumerates the reasons reads as a closed list and does not name it.

A clause on the not-attempted row makes the two agree: or the verifier could not establish that the re-run used the closure alone. Naming the capability as a fourth holding would do the same work with a larger edit, so I would take the clause. With the clause in, I have nothing else.

pytest 1655 passed and 1 skipped on bb29b05, check_dashes clean, the keyword guard 12 passed. #366 reads correctly and carries the measurements. The glossary line is mine and I will send it separately.

[chernistry]

Clause taken, at HEAD: the not-attempted row now ends "or the verifier could not establish that the re-run used the closure alone". The row and the paragraph under it agree, and a verifier that cannot observe reads has a named reason rather than a principle to derive one from. Nothing else changed; pytest 1655 passed, check_dashes clean.

Thank you for the two rounds. The withdrawal was the right call and I would not have got there without the preimage half of the finding.

[lywinged]

Approved at b461b6b. The clause is the one proposed, word for word, and the diff against bb29b05 is that line and nothing else. pytest 1655 passed, 1 skipped; the keyword guard 12 passed; check_dashes clean.

[imran-siddique]

Merged as 0ec0453. From here I answer for the MUSTs in §3.1.4, as agreed on the 13th, and the schema follow-up you queued in #366 is the next step on this line.