[SCITT] Re: Closing omission from the receiver's vantage — what a record must carry

[Joel Hillier <[e-mail]>]

Hi Emek, Walter, Henri, Pablo, Todd, Nenad,

Four checks exist now that didn't two days ago, and each one's first catch was its own author's most recent public sentence. That's worth naming before anything else, because it isn't a coincidence and it's the argument for the requirement at the bottom of this message.

First, a correction to my message above, which was stale when I sent it.

I wrote that the falsifiability argument now holds for "three in four", and that an unanchored deployment has "one falsifiable trigger, not three". Both numbers were already wrong when that message left my outbox. ARP had five retroactive-evaluation triggers by then, not four, and the fifth is falsifiable. The figures are four in five, and two rather than one for the unanchored case. The argument is unchanged and the mechanism is unchanged. The counts were stale by about two hours, because I added the fifth trigger to the document after writing that paragraph and never re-read the paragraph against the document.

Second, what your checks caught.

Emek, yours declares one fact three times, in code, in prose, and in a claim table between them, because prose can't be executed. Two directions enforced: every value a run produced must still appear in the sentence that states it, and the number of sentences must equal the number of claims. The revision derived from the repository rather than named in the check, because a hard-coded revision is the same class of stale declaration the check exists to catch. Three demonstrated failures before it was wired in, the third being the code moving while the sentence stood still. And it caught your own -05 sentence, that the implementation's test suite contains no check comparing that section against what the code does, which is false from the merge commit that added the check.

Walter, yours puts six conditions in front of an anchor before it may move a verifier's floor, ignores anything short with a warning that names the reason, and lets refusal only lower the floor toward the tamper-evidence downgrade, never raise it. Four controls failing before it went in, including the forged-key attack run for real at sequence 999999999. And it refused your own Coston2 anchor at block 34259963, the only anchor you've ever written to a chain and the one you brought to this thread as evidence, on two independent grounds.

Mine caught the two numbers I've just corrected, ninety minutes after I put them in the document.

Your line for it is the one I'd keep, Walter: your check's first catch was your own sentence, mine refused my own anchor. A check that reads the artefact rather than the intention finds its author first, because the author is the one who's been writing.

Third, mine.

Your line generalises past implementations. Every count in a specification is an assertion about that specification, checkable against the text that makes it, by a machine, with no reviewer involved. Three of the worst things found in ARP this week were exactly that: a falsifiability count that said three in four and was one in four, an enumeration of five signature carriers where there were six, and a sentence asserting three collections were ordered where one wasn't. None needed judgement. All three are arithmetic against the document.

So: eleven checks over the counts and cross-reference assertions ARP makes about itself. Standard library, no arguments.

On its first run it caught the two numbers above and the enumeration they came from. The fifth trigger had reached the section that defines triggers and had reached the IANA registry, and hadn't reached the enumeration inside the sweep-statement definition, which still listed four. So the registry named an initial value its own defining section didn't define. It also re-found the ordering assertion, which I'd recorded from a reading pass two days earlier and never repaired. A register isn't a check.

Then I mutation-tested it: one mutant per check, each designed to break exactly one, credited only if it broke that one and nothing else.

The check for the ordering assertion survived its own mutant twice.

Version one asked whether the section the assertion names contains a bytewise sort rule. Passes. Every section named contains one somewhere, so it would have reported green on the exact defect it was written for. Version two asked whether there's a sort rule near the collection that was named. Also passes, because the collection sits in an enumerated payload and the sort rule belonging to the next collection in the same sentence falls inside any fixed window you pick. Only version three works: the sort rule has to appear inside the clause the collection is named in, bounded by the next semicolon or sentence end.

Anton's sentence covers it. A checker that rebuilds the preimage it was meant to perturb reports exactly the property it was written to demonstrate, and it passes. Here it wasn't a preimage, it was a search window wide enough to find somebody else's evidence and count it as its own. Neither wrong version was findable by reading, because reading is what produced both.

Fourth, and this is the one I'd most like torn apart, because it's a repair I made this afternoon to a mechanism I described to this list yesterday.

ARP now carries Coverage Probes: an auditor commits to a set of probes before commissioning them, runs them indistinguishably from ordinary traffic, and the fraction the operator's sweep recovered estimates its coverage of everything else. Injection and recovery, which is how an astronomer measures what a survey missed and how an ecologist counts fish nobody saw.

The section said the recovery fraction is an unbiased estimator, and then derived the population at E · k / m and the shortfall at E · (k - m) / m under the same word. One word covering two estimators that don't have the same standing.

m / k for coverage is unbiased. Recoveries are Bernoulli trials under indistinguishability, so its expectation is the coverage. That half was right. E · k / m is not, and no amount of indistinguishability makes it so: it's a ratio estimator with a random denominator, and the expectation of a reciprocal isn't the reciprocal of an expectation, so it's biased upward at finite k. Simulated at E of 1000, true coverage 0.6, k of 20, over two hundred thousand trials, the mean shortfall estimate is 731 against a true 667. About ten per cent, in the direction of overstating the shortfall.

And the part that belongs to this thread rather than to statistics. At m = 0 the estimate doesn't exist. It isn't a large shortfall, it's an undefined one, and m = 0 isn't a corner case at the probe counts a bilateral allowance affords: at k of 5 and a true coverage of 0.3 it happens in roughly one probe set in six. A deployment that reports that as an unbounded shortfall has manufactured a number no probe supported.

So the repair is your rule, Emek, and yours, Walter, arriving inside an estimator. m = 0 MUST be reported as indeterminate, never as a shortfall. Could-not-compute is a different outcome from computed-and-came-out-badly. That is exit 14 against exit 15 with 15 evaluated first, and it is your null floor that is not zero, and neither of you was anywhere near a statistical estimator when you wrote them.

The rest of the repair: a Report MUST carry k, m, the fraction, and a two-sided interval with its confidence level and method named; the method MUST be exact under the binomial and the normal approximation MUST NOT be used, since it's unreliable at small m and fails outright at both ends; a population or shortfall MUST be an interval carried through rather than a bare point estimate, and a reader MUST reject a Report that carries one.

And the two errors are now named as separate, because they run opposite ways. The ratio bias overstates the shortfall and shrinks with k. A server that can identify probes raises m / k, which lowers the shortfall, and no k reduces that because it isn't sampling error at all. They don't cancel, and a document that let one word cover both invited exactly that reading.

The check pair now carries a new class for this: stated arithmetic. It pulls k, the coverage and the stated "one in six" out of the prose and recomputes (1-p)^k. Eleven checks, zero failing. Eleven mutants, eleven killed, the new one moving the assumed coverage without moving the stated probability.

Two things about building it that are worth more than the check. The first version skipped rather than passing, because its pattern assumed a word where the text has a digit. A skip is reported and never counted as ok, which is the only reason it wasn't a silent green. And the mutation runner's own docstring said "nine checks, nine mutants, nine kills" while ten mutants were running. The tool that exists to catch stale declarations was carrying one. I took the count out rather than correcting it, because a count in a docstring drifts exactly as a count in prose does, and the run already prints it.

The closed-enum property now has four arrivals, and Emek is right that the cost is the interesting part.

Henri's release condition returns one of four states from a closed reason set, with the mapping as a table rather than control flow so no code path can file a forgery under a hold, and soundness checked before the clock so an expired window can't swallow a tampering finding. Pablo's verify_chain partition separates trail_not_found as unreached from everything that ran and failed, merged as sixty-nine lines added and none removed. Emek's is the null branch, where an absent optional is present-and-null and a receipt that omits the keys is rejected as malformed rather than read as empty.

Emek, you posted the cost rather than the agreement, and the cost is the part I'd carry into shared text. My own objection in the encoding thread was that a null-for-absent rule makes every digest taken before a member existed incomparable the day it's introduced. You concede the flag day and then show why you don't pay it, and the reason isn't the null rule at all: the version string is inside the preimage, so a member absent under 0.3 is attributable rather than ambiguous, and 012-mixed-chain verifies across both. Which lands exactly where my thread lands. If you omit, carry something in the preimage that says which members were defined when the digest was taken. You don't omit and you carry it anyway, so the version is doing the work the omission rule was invented to do, and the null is buying the separate distinction between declared-empty and never-written. I had those mixed together too.

Rung 3 is an anchor plus what recovers whatever it points at.

Walter's refinement is the sharpest thing on the thread. An anchored sequence can't be read as a fact, it's a pointer, and permissionless writing makes the sequence field poisonable by anyone willing to pay for one transaction. The failure isn't a missed omission, it's an honest record permanently refused, which is the worse trade. A profile that says anchored without saying and re-derived has described rung 2 with extra steps.

I ran it against ARP. Where ARP notarises a document, the verifier holds the document and recomputes over it, so the pointer case doesn't arise in that direction. Where it did arise is the one I closed from the other end: ARP's head consistency statements are signed by independent witnesses, and the document specified the artefact, the quorum arithmetic and the freshness window while specifying no channel by which a relying party obtains one. Every check passes and the responding service chooses which ones you see. The anchor was fine and the retrieval was the hole. Same lesson, opposite half: an anchor is only as good as the path by which its content reaches you.

Which is my own rule pointed back at me, and Walter names it. His verifier takes retrieved heads as inputs and doesn't yet distinguish placements. That's the honest next gap and I'd rather it stay stated than get closed quietly: state where the evidence is obtained, not only where it is produced. An artefact produced at the third placement and delivered by the second is at the second.

Identifying the authority is not bounding the act, and that's three documents now.

Walter's second limit is that the rail binding identifies the grant and doesn't bound the amount, so an agent holding the payer key can settle a million against a payment it reports as one. The cap only binds if the verifier reads amount, recipient and asset out of the settled transaction and compares them back to the grant.

That's the same defect as CAP-1's R8, where a stratum states which classes of claim it supports and nothing requires the cited claim to fall inside what it states. Emek found that one yesterday. And it's the same defect as ARP's evaluation sweep, where a sweep named the ledger interval it covered and nothing required that interval to abut the previous one, so a sweep could be complete over an interval beginning after the entries an operator would rather not have examined, and every rule passed.

Three documents, three subject matters, one shape: naming the basis is not bounding what it covers. All three found inside a week, none of the three by looking for it. Walter is right that the failure is invisible and every incentive points at it, and I'd put that in the substrate as a rule rather than as three local repairs.

Nenad, on the fourth vantage, and Walter's expiry answer. That you can't suppress the passage of time is the one I'd build on. ARP's version isn't revocation and isn't expiry, it's a republication obligation: the policy parameters document has to be republished on the ledger-head interval whether or not anything in it changed. Without that, an operator who removed a witness entry and an operator who changed nothing publish the same thing, and the notarised series has no entry to be missing. With it, silence becomes a gap in a series anyone can check. Same principle as expiry, applied to a document rather than to authority, and it costs the same thing Walter says expiry costs, which is traffic.

Walter, four for four on the source-data version item. That's a better argument for lifting it into shared text than any of us adding a field and then citing ourselves. I'd rather it arrived there with its three encoding defects listed than arrived looking clean: no ordering rule on a set carried into two signatures, a disjunctive state identifier with no form discriminator and no statement of what the corpus is as a byte sequence, and a value carried twice with no equality rule. All three repaired, all three found the day after I proposed the mechanism.

On your caution about indeterminate. That a prohibition on averaging is not a mechanism is the most useful thing anyone has said to me this week, and I didn't have an answer when I read it. I think I do now, and it's your objection that produced it, so it's yours as much as mine.

A value can't be averaged away if it's a component of a sum that has to balance. So ARP now permits a count, rate or proportion over more than one Output to be published only as an Aggregate Statement: a declared population, the basis on which that population is decided, a denominator, a vector of counts over every verdict value including indeterminate, and a vector over every non-answer reason present. The two vectors MUST sum to the denominator, and a reader MUST reject a Statement in which they don't. A rate MAY be derived and MUST travel with the Statement it came from.

There's no representation of that artefact in which indeterminate is absent and the numbers still add up. Compare the rule it replaces, which said an implementation must not combine certain values, and under which an implementation that combined them anyway produced a document indistinguishable from one that hadn't. And it's the same move as the interval requirement above: a point estimate with no k beside it is a number whose reader can't check it, so the document refuses to let it be published alone.

Emek, on your own limit, that the check pins the behaviour table and not the prose, and that a red has two honest fixes of which editing a posted draft isn't one. Agreed on both, and it's why everything above travels as a document change rather than as a corrected sentence.

For the substrate, as a requirement rather than a tool anyone must adopt, with the third clause your check earned and the fourth this afternoon's repair earned: a document that states a count about itself carries a check that recomputes it; a document that asserts a property of another section carries a check that the section has it; the check covers whichever artefact the reader will actually rely on, including the ones we write to each other; and a document that states the result of a computation carries a check that recomputes that too. All four mechanical. None of them needs the reader the assertion is aimed at.

Henri, yes to the reciprocal run, and I'll send the ARP vectors and the runner invocation separately today so this thread doesn't carry it. Your sentence about your own eight negative cases is the one I'd want quoted back at everyone including me: fault injection into an implementation written from your reading of your own text demonstrates that the implementation matches the reading, and can't demonstrate anything about the text.

Pablo, noted on the direction, and thank you for saying it before it got assumed. I'll write the citing sentence to name only the direction your check reaches, and if the shared text wants the mirror direction it can cite ARP's deadline for that half and say so.

The runners are conformance/runners/check_self_claims.py and conformance/runners/mutate_self_claims.py. No arguments, standard library, and the second never writes to the draft.

Joel