feat(represent): the representation attestation plane, from sidecar to enforced fidelity floor (ATTESTATION-1) - #447
Merged
Merged
Conversation
…1 step 1) Step 1 of seven: what a represented operand INSTANCE achieved, as opposed to what its codec's scheme guarantees. A codec can state a radius when its error is a property of the SCHEME — `F32_PLANES` truncates bit planes and the bound follows from which planes are read. `VQ8_SHARED` cannot, because a vector quantiser's assignment error is a property of a fitted codebook against actual weights: the same codec, the same 256 entries and the same grouping give a different error on every tensor they were fitted to. VQ-1 closed on exactly that, and this is the authority the codec plane cannot carry. `RepresentationAttestations` is an optional versioned sidecar, declared by the index the way `auxiliary_references` is and absent from every container written before it. One row binds a measurement to the operand and parent extent, the codec family and revision, the logical shape, the content digest, the source digest, each dependency's TERMINAL baseline, and the encoder recipe plus attesting authority and method. Judging produces a real `FidelityCertificate` — the codec plane's own type, so an attested claim and a declared claim compose through one algebra rather than two. Binding to each dependency's terminal identity rather than to whatever depth a plan selects is what keeps this from exploding: otherwise every parent x dependency-depth combination needs its own attestation, and an attestation goes stale for reasons unrelated to the measurement. The selected depth is composed on top at planning time, which is step 5. Structural refusals, all readable with no container, no registry and no bytes: a schema another build wrote (named both ways), an empty operand, an empty codec family, content digest, source digest, recipe or authority, a shape with no elements, an empty dependency baseline, a malformed metric, domain or method id, a radius that is not a finite non-negative number, and one operand attested twice at one extent — that last refuses rather than keeping the last row written, because nothing says which was meant and picking one would make a container's guarantee depend on its serialisation order. Three distinctions the table keeps apart, none of which is zero: ABSENT (nothing attested), and later STALE (bound to bytes that changed) and UNRECOGNISED (an authority or method this build does not know). Step 1 witnesses the first; steps 2 to 4 add the others. A measurement at one extent is never offered for another, and a table the index names and the container does not hold is a refusal rather than an empty table — silently reading a missing attestation file as "nothing attested" would turn a packaging mistake into a quiet loss of every guarantee. A method id is validated by the same rules as a metric id and is deliberately not one: "how it was measured" and "what the number means" are different questions, and giving the method a `MetricId` would invite composing against it. The claimed radius is behind an accessor rather than a public field, because a caller reaching past recognition to the number is precisely the "presence implies trust" failure this plane exists to prevent. Also records the user's B3 scope ruling as a forecast addendum, given after the freeze merged and before any implementation: B3 stays in, the planner must compose the attested parent certificate with the selected auxiliary certificates when enforcing the floor, and without that the sidecar is stored evidence nobody relies on — hollow carriage. The decisive witness is one artifact and one floor: attestation alone passes, plus a shallow codebook fails, plus a deeper codebook passes. Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against x86_64-apple-darwin, cargo test -p larql-vindex (4828 passed, 0 failed), cargo test -p larql-cli, doc links. Coverage policy passed at 93.66%; the new module is at 100%.
Stage one of two: does this attestation still describe what is actually there? Answered from metadata alone — the tensor table, the codec's declared identity, the reference table — with no payload read, exactly as VQ-1 admits an auxiliary closure. `AttestationStatus` keeps apart three answers a single `Option` would blur, none of which is zero. ABSENT: the container attests nothing here, and it says which depths it DOES attest, so "no guarantee" is never mistaken for "the file did not load". STALE: something is attested and it was measured against something that is no longer what is there, named by cause. BOUND: the tuple holds — which is not yet trust, because recognition and the content digest are still to come. Each cause is a variant rather than a string, so a caller can act on the difference — a changed dependency baseline is worth re-attesting, a changed codec revision usually means re-encoding — and so a test can assert WHICH check fired rather than that something did. The order is most-fundamental-first: an operand stored under a different codec entirely reports the codec, not the shape difference that follows from it, because comparing shapes across codecs sends a reader after the wrong thing. A FINDING against the forecast. X3 asked for six staleness causes refused by name. Two of them are not container-checkable at all: the index says outright that once encoded the source checkpoint disappears as an authority, so an artifact holds neither the source tensor it was fitted to nor the recipe that produced it. They are carried as IDENTITY and compared only when a caller who actually has them supplies the expectation — a re-encode pipeline, a qualification harness, an external verifier holding the checkpoint. Recording them uncheckably is not decoration: it is what lets a verifier outside this process do the check this process cannot. The test asserts both halves, because a field that is only ever checked when nobody supplies it is how an unverifiable claim quietly becomes a decorative one. Two test-quality corrections made in passing. An assertion that a staleness message contains no `0` was pinning a coincidence — it would have failed the moment someone put the operand address `block.0` into the message, and a correct change failing a test is worse than no test. It now asserts the refusal does not hand over the specific radius it is refusing. And the seven `describe` arms were 88% covered because only one cause was ever described; a refusal message nobody reads is one nobody can act on, so all seven are now exercised and asserted to name both sides of their comparison. That took the file to 100% by testing the gap rather than by waiving it. Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against x86_64-apple-darwin, cargo test -p larql-vindex, cargo test -p larql-cli, doc links. Coverage policy passed at 93.68%; both new modules at 100%.
An attestation that is well-formed, current and bound to exactly the
right bytes is still only a claim: someone wrote a number into a file,
and nothing about the file makes it true. A build that reads a radius
because one is present has replaced a measurement with a rumour.
So recognition is a fourth answer, not a shade of the other three.
UNRECOGNISED means the container is fine, the artifact is fine, the
attestation describes exactly what is there, and this build does not take
that authority's word or does not implement their method. That is the
reader's limitation rather than the artifact's fault, and collapsing it
into "no certificate" would tell an operator to re-encode when what they
actually need is to configure recognition.
NOTHING IS RECOGNISED BY DEFAULT. No encoder in this build produces
attestations, so this build has qualified no authority and no method, and
`RecognisedMethods::none()` says so. A convenience default — recognising
anything calling itself `larql-encoder`, say — would mean any file
claiming that name could assert any radius it liked, defeating the plane
with its own default. The cost is deliberate and asserted: an artifact
full of perfectly good attestations is worth nothing until a caller
states whose measurements it accepts.
Recognition is exact, version included. `measured-rms@1` says nothing
about `@2`: a method version exists precisely because the measurement
changed, and accepting any version of a known name would honour a
definition nobody read. The same rule VQ-1 applied to metric and domain
ids. The refusal is useful about it — being told "you have that method at
version 1" is far more actionable than "unknown method" — and authority
is reported before method, because a reader whose word is not taken at
all does not need a lecture about versions.
PRECEDENCE, PINNED DELIBERATELY: when an attestation is both stale and
unrecognised, staleness is reported. Staleness is a fact about the
container and holds for every reader; unrecognition is a fact about this
build. Reporting recognition first would send an operator to configure
trust, after which they would discover the attestation had expired
anyway. A judgement call, so a test asserts it rather than leaving it to
whichever check happens to run first.
The discriminating control the forecast asks for is here: the same
attestation against the same artifact, usable under one policy and
refused under another, so the refusal is the recognition and nothing
else. And a test asserts the three refusals do not read alike, because
"absent", "stale" and "unrecognised" send an operator to three different
places.
Also starts the wave's notes file, which accumulates findings AS THEY
OCCUR rather than at the close, so a finding is durable at the moment it
is made. Two so far:
ATT1-N1 Two of X3's six staleness causes are not container-checkable.
`index.rs:154` says once encoded the source checkpoint
disappears as an authority, so an artifact holds neither the
source it was fitted to nor the recipe that produced it. They
are carried as identity and checked only when a caller who has
them supplies the expectation.
ATT1-N2 A SECOND process-global test instrument races, in the same
class as PR1-N5. `the_counters_only_move_for_mapped_images`
failed once during this step's gate run and was green on the
next full run. The cause is structural rather than a rerun
story: `STAGED_BYTES`/`STAGED_IMAGES` are process-global
atomics, the test reads an exact delta under `#[serial]` — which
serialises it only against other `#[serial]` tests, not the
binary — and `experts.rs` and `weights/mod.rs` both reach
`StagedF32::stage` with no serial annotation at all. This wave
stages no f32 images; adding tests changed the interleaving.
Recorded, not fixed and not worked around: relocating the test
would make the assertion pass while leaving the defect intact,
which is the reasoning that produced the PR1-N5 waiver.
Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against
x86_64-apple-darwin, cargo test -p larql-vindex, cargo test -p larql-cli,
doc links. Coverage policy passed at 93.70%; `recognition.rs` at 100%.
Stage two of two, and the check that cannot be metadata-only. The container holds no per-tensor digest — that is finding B4 from the freeze — so an attestation binding to content is verifiable only against the content, at preparation, where the payload is being read anyway. The check costs a hash and not a second load. VERIFIED IS A STATE OF ITS OWN, and only it hands over a certificate. `Bound` now means the tuple holds and the authority is recognised and nobody has looked at the bytes; `AttestationStatus::certificate()` returns `None` for it. That distinction is the point of the step: an ergonomic accessor that handed over a radius before the payload was checked would defeat the entire plane in one method, and every caller who forgot stage two would silently get an unverified guarantee. The forecast's X2 arm and its control are one test, because the tamper arm means nothing without it: the same operand, the same attestation, the same policy, one byte flipped in the middle — no length change, no metadata change, so every tuple check still passes and only the payload can catch it. The untampered control verifies; the tampered one goes stale naming both digests. Truncation and extension are covered too, since a partial write is a likelier failure in practice than a deliberate flip. Bytes cannot promote a status that already failed. An absent attestation stays absent against exactly the right bytes, a stale one keeps its ORIGINAL cause rather than having it overwritten by the content check, and an unrecognised authority stays unrecognised. Without that, `verified_against` would be a back door: hash the right bytes and promote anything. The digest is prefixed `sha256:` rather than bare hex like the container's own `payload_sha256`. That field names its algorithm and this one does not, and an attestation outlives the build that wrote it: a bare hex string that turns out to be some other algorithm is unfalsifiable, because it simply never matches and nobody can tell that from a tampered payload. Two assertions from steps 2 and 3 failed against this change and were corrected rather than preserved. Both asserted that a `Bound` status was `unavailable_because(..) == None`, which was true when `Bound` was the terminal good state and is false now that the payload check is part of the binding. They now assert the payload-unchecked reason. The tests catching a semantic tightening is them working, not them being wrong. Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against x86_64-apple-darwin, cargo test -p larql-vindex, cargo test -p larql-cli, doc links. Coverage policy passed at 93.70%; `mod.rs` and `recognition.rs` at 100%, `tuple.rs` at 98.58%.
…step 5, B3)
VQ-1 built a composition algebra and nothing called it: the floor reads
`option.certificate.radius`, the CODEC's declared bound, with no
knowledge of any dependency. That was harmless only because no shipped
codec both declares a radius and requires an auxiliary. Attestation
removes the accident — an attested VQ operand HAS a radius — so wiring
composition into selection belongs to this wave. Without it the sidecar
is stored evidence nobody relies on, and the silent over-promise VQ-1
exposed stays possible.
SELECTION IS PHASED EXPLICITLY, because verification needs the payload:
1. Metadata admission — candidates derived, absent/stale/unrecognised
rejected, no payload read. A test asserts the store's read counter
does not move.
2. Evidence verification — hash only what admission bound. No
executable pin exists at this point, by construction.
3. Final selection — the option's certificate is built from Verified
claims only, composed parent with dependency, and the floor decides.
There is NO provisional selection from `Bound` evidence, even if it would
be checked later: a plan built on unverified claims and corrected
afterwards would, however briefly, assert a guarantee it had not earned,
and "briefly" is not a property a guarantee can have. The types enforce
it rather than a rule someone must remember — a `Candidate` carries no
certificate at all, and `derive` accepts only `VerifiedEvidence`, which
nothing but `verify` can construct.
THE DECISIVE REGRESSION, one artifact and one floor:
attested parent radius: 0.003
shallow codebook: 0.003 -> composed 0.006 -> rejected
deeper codebook: 0.001 -> composed 0.004 -> selected
floor: 0.005
Neither half decides it — 0.003 is inside the floor and so is each
codebook bound — so only the composition separates them, which is what
makes this a witness for B3 rather than for arithmetic. The premises are
`const` asserts: editing the constants so that one half alone decides
fails the build rather than quietly turning the test into a tautology.
The test also asserts that a floor consulting only the parent would have
admitted BOTH, which is the over-promise stated as a fact.
TIME OF CHECK, TIME OF USE. Hashing proves nothing about the bytes a
later decode reads unless both come from the same immutable object, so
the `SourceStamp` — store id plus overlay generation — travels with the
evidence. Two guards, because there are two windows: `verify` refuses a
source that moved since ADMISSION, and `ensure_current_for` refuses one
that moved since VERIFICATION. The second is easier to miss because
nothing has been read yet when it opens.
Verification reads are reported as preparation work rather than absorbed:
a ledger that hid them would price a plan as though guarantees were free.
The number is the operand's stored length, because that is exactly what
had to be hashed, and a plan that admits nothing reads nothing.
An attested claim REPLACES the codec's declared one rather than widening
it. They are two statements about the same quantity — one measured on
this instance, one derived from the scheme — and adding them would
double-count.
An API footgun found by coverage and fixed rather than tested around:
`verify` originally took the subject list a second time, so a caller
passing a different slice than `admit` received would have silently
dropped candidates. Verification now carries what admission decided and
looks the attestation up by key; an attestation withdrawn between the
phases is refused by name instead of vanishing. The content comparison
also moved to one home, `JudgedAttestation::content_mismatch`, so the
phased path and `verified_against` cannot drift about what "the right
bytes" means.
Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against
x86_64-apple-darwin, cargo test -p larql-vindex, cargo test -p larql-cli,
doc links. Coverage policy passed at 93.72%; `attested_fidelity.rs` went
86.89% to 100% by testing the three paths the gap exposed — the
admit-to-verify stamp guard, a payload failing verification, and a
withdrawn attestation — each of which was a real hole rather than a
coverage technicality.
chrishayuk
changed the title
…TION-1 step 6)
Step 5 built the composition algebra and proved it against hand-built
options. Nothing called it. `attested_fidelity` had ZERO production
callers, `AttestationTable` was never imported into `prepared.rs`, and
every `ExtentOption` the planner built came from `codec.extents()` alone
— the codec's declared bound, with no knowledge of any dependency. The
mechanism was complete and the guarantee was not: the floor that gates
selection still made exactly the over-promise this wave exists to remove.
CARRIAGE, in the order the boundary demands. `select_records` now runs
the three phases after refusals and before anything consults the floor:
admission over every planned operand from metadata alone; verification
hashing only what admission bound; derivation replacing each option's
declared certificate with the composed one. Refusals come first so a plan
that is already refused never pays for verification.
The store learns two things at open, both mirroring the reference table
beside them. The attestation table, where a table the index NAMES and the
container does not hold is a refusal rather than a silent loss of every
guarantee. And `RecognisedMethods`, defaulting to `none()` — an
attestation is carried and checked either way, but acting on one is a
TRUST decision and belongs to the caller, not to the container making the
claim about itself.
UNAVAILABLE, NEVER OPTIMISTIC. A missing dependency pin, a dependency
whose codec declares no radius, and a composition the metrics refuse all
leave the option with no radius at all. `RepresentationFloor` already
reads that correctly — an undeclared error is not a small one — so each
case refuses a shallower extent instead of admitting it on a bound nobody
computed. A composition refusal is deliberately not fatal: a floor of
`Exact` never consults a radius, and a container whose metrics disagree
should still be plannable at full depth.
ONE CANONICAL DERIVATION for a dependency's terminal baseline. There are
two independent producers of that string — the encoder that writes an
attestation and the planner that checks one — and a format they agree on
only by convention is one they will eventually disagree on. Drift there
does not fail loudly: every attestation simply goes `Stale` with a
changed-baseline cause, indistinguishable from a legitimate re-encode.
THE FORCING CASE, end to end through `select_realizations_within`, with
codecs that exist because no SHIPPED codec both declares a radius and
requires an auxiliary — which is why nothing in the suite could tell the
declared and composed readings apart:
parent radius (declared, depth 0): 0.003
coarse codebook: 0.003 -> composed 0.006 -> refused
fine codebook: 0.001 -> composed 0.004 -> selected
floor: 0.005
Neither half decides it, asserted at compile time. A companion test states
the over-promise as a fact: the declared bound is identical in both
containers and inside the floor in both, so a planner reading it alone
would have admitted the coarse artifact too. Under a preparation budget,
the fine container spends the depth and the coarse one is REFUSED, naming
the floor it could not meet.
And the wave's exit claim, in the planner: an attested 0.001 against the
SAME coarse codebook composes to 0.004 and is admitted — a lossy artifact
satisfying a quality requirement without anyone inventing a number. The
control is the same container, the same attestation, the same bytes, read
by a build that recognises nobody: the guarantee is unavailable, selection
falls back to the declared 0.006, and the floor refuses it.
Verification reads are preparation work and are reported as such: they
resolve through `load_raw`, so they land in the store's consumption
ledger, asserted as one read per attested operand and none for a plan that
attests nothing. The `ResourceLedger`'s own `prepare` figure is priced
from declared extents and does NOT include them — that is debt D1, named
by the freeze and not paid here.
Both carriage tests were confirmed to fail with the composition call
removed, while the declared-bound control stayed green — the gap is
demonstrated, not asserted.
Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against
x86_64-apple-darwin, cargo test -p larql-vindex (4867), cargo test -p
larql-cli (911), doc links. Coverage policy passed at 93.72%, unchanged
from before carriage; the attested path was uncovered on first run and was
tested rather than waived.
chrishayuk
changed the title
…loors that read it are enforced
`RepresentationFloor::Exact` has ALWAYS meant "the deepest extent this
codec declares" — `admits` compared depths and never once consulted a
radius. For a lossless progressive codec the two readings coincide. For a
lossy one they are not the same claim: `VQ8_SHARED` at full depth is
every byte the artifact holds AND no bound whatever against the tensor it
was fitted to. This build would eventually have printed "exact
reconstruction" while planning terminal Q4 or VQ data.
THE REFERENT, settled and written down where the type is defined. A
certificate measures decoded values against the TYPED LOGICAL SOURCE
TENSOR presented at the representation boundary. Not against the stored
representation — that reading makes every terminal extent trivially
exact, since decoding all of an artifact always reproduces the artifact,
and collapses the distinction this commit exists to draw. Not including
kernel arithmetic — what a direct kernel over codes rounds to is a
property of the kernel and belongs to realization qualification.
The vocabulary follows, and the two questions are now asked separately:
TerminalExtent how much of the artifact is read. STRUCTURAL, states no
source-fidelity claim, still the default — so existing
plans keep their behaviour without inheriting a quality
claim nobody earned.
CertifiedExact a verified compatible certificate whose radius is 0.0.
Within(r) a verified composed certificate at or under r.
Neither evidence floor is satisfied by being terminal. `admits` no longer
short-circuits on depth for them: an operand with no certificate has made
no claim about its source, and no claim is not a small error.
DECLARATIONS BECOME HONEST rather than uniform. A lossless carrier can
say 0.0 and now does — raw `F32` is the identity, `F16`/`BF16` widen
exactly, `BF16_ZLIB` is byte-identical once inflated, and compression is
not approximation. A codec that FITS its source still says nothing:
`Q4_K`, `Q6_K`, `Q8_0`, `NVFP4`, `MXFP4` and `VQ8_SHARED` carry an error
that belongs to the instance encoded, and only an attestation can supply
it. The old contract test asserted "a single-extent codec declares no
radius", which conflated the two questions — it is not the extent count
that decides, it is whether anything was thrown away.
AND THE FLOORS ARE NOW ENFORCED, which is the half that made the rest
worth committing. `RepresentationFloor` was consulted in exactly one
place, `shallowest_saving`, which judges candidate MOVES under
preparation pressure. Under `ResidencyBudget::UNBOUNDED` there is no
pressure, so nothing consulted it at all: a caller could declare
`CertifiedExact`, plan a Q4_K model, and be refused nothing. The
requirement was real and no code ever asked it — the same hollow shape
step 6 removed from the composition itself.
Enforcement lands on the INITIAL selection, and deliberately nowhere
else. The only assignment to `extent.selected` after the initial pin
takes its extent from `shallowest_saving`, which already filters by
`fidelity.admits`, so reselection is enforced at the point of choice; a
re-check on the way out could never fire, and a refusal that cannot
happen is decoration. That reasoning is recorded at the return rather
than left for the next reader to re-derive.
The witnesses, on a real Q4_K container compiled from the fixture and
planned under a budget that asks for nothing:
TerminalExtent plans it, claiming nothing about it
CertifiedExact REFUSES, naming the operand, the representation, that
it states no source-fidelity bound, and that a verified
attestation is the one thing that could supply one
Within(1e9) REFUSES too — no bound is loose enough to buy a claim
that was never made
Plus the opposite half of the refusal: a composed bound that EXISTS and
is merely too large is refused by its number and metric, not by absence.
Removing the enforcement call turns both Q4 refusals red while the
structural arm stays green.
Structural, and confined to code this branch introduced: the step-6
carriage moves out of `prepared.rs` (already far over any sane length)
into `fidelity_carriage`, which now also owns enforcement — one module
for "what bound applies and who may rely on it", knowing nothing of
realizations, backends or budgets. `prepared.rs` drops 224 lines net. The
900-line `composed_floor.rs` becomes six files, none over 330, with every
premise in one `vocabulary` module so no value is spelled twice. No
pre-existing file was reorganised.
Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against
x86_64-apple-darwin, cargo test -p larql-vindex (4878), cargo test -p
larql-cli (911), doc links. Coverage policy passed at 93.72%;
`fidelity_carriage.rs` came in at 89.77% and was brought over by testing
the branch it exposed and deleting one that could not be reached.
…p 7)
An integration test is a separate crate in cargo's model, so this one sees
only what `larql-vindex` exports. Nothing under `src/` was edited for this
provider: no match arm names it, no planner branch knows it has two
extents, and no policy anywhere knows who `acme-metrology` is.
The crate contributes four things this build does not ship — a parent
representation, the dependency it decodes through, the ROLE name binding
them, and the authority and method that attest an instance — and every
one of the five identifiers is spelled in `provider.rs` alone.
THE GENERICITY CLAIM IS CHECKED, NOT ASSERTED. A test walks every `.rs`
under `crates/*/src` that is not itself test code and fails if any of the
five appears. A plane that works only for identities its own build knows
is a match statement with extra steps. The scan carries its own control:
a second test looks for `VQ8_SHARED` — a label this build DOES ship —
through the same walk, so an empty result means "nothing there" rather
than "nothing looked at", and a scan pointed at the wrong directory fails
loudly instead of passing vacuously.
The arms, each with the control that isolates its mechanism:
RECOGNITION the same container, bytes and floor, differing only in
whether this build takes the authority's word. Recognised,
the measured 0.001 replaces the declared 0.004; under
`RecognisedMethods::none()` the declared bound stands and
the budget has nothing it may spend.
VERIFICATION the tampered attestation differs from the truthful one in
the content digest ALONE — same operand, shape, revision,
baselines, authority and method — so every metadata check
passes and only the payload can catch it.
COMPOSITION with no attestation at all the declared 0.004 is inside
the floor on its own, and 0.006 composed with the anchor
table is not; a floor raised to the composed bound admits
the same extent, which is what makes the refusal about the
composition rather than about the extent being unreachable.
CERTIFIED the parent certifies 0.0 at the extent selected and the
plan is STILL refused, because what reaches the caller is
decoded through a table certifying 0.002. An exact parent
through a lossy dependency is not exact.
IDENTITY either provider removed, and the parent substituted at a
revision that means different bytes: preparation is
invalidated and the refusal names which provider.
THE Q4 LESSON, KEPT AS AN ASSERTION. A test of representation policy must
prove the plan actually CONTAINS that representation. The earlier witness
for this wave passed while planning f32, because the store resolves the
source representation unless opened for the compiled one — it was testing
nothing and looked green. `assert_plan_is_the_providers` now checks the
operands are the provider's, that both its extents reached the pin, and
that its dependency resolved through the role it declared.
Each mechanism was mutated in production code and the corresponding arm
verified to fail: recognition (the gap check) fails the recognition arm
alone; the content check fails the verification arm alone; composition
fails all four fidelity arms. Two of those mutations were no-ops on the
first attempt — one patched a short-circuited path, one patched the wrong
file after the carriage moved — and both LOOKED like evidence the arm was
weak. The mutation edits now assert they applied, because a mutation that
silently does nothing is indistinguishable from a test that proves
nothing.
Gates: fmt, clippy (larql-vindex, larql-cli), cargo check against
x86_64-apple-darwin, cargo test -p larql-vindex (4886), cargo test -p
larql-cli (911), doc links. Coverage policy passed at 93.72%.
chrishayuk
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
All seven steps. The forecast is on main (#443); this is the code against it. The forecast is already on main (#443); this is the code against it.
What changed since this PR was opened: it described steps 1–2 and said "nothing here yet makes an attested radius reach a floor, so nothing here can over-promise." That is no longer true of this branch — steps 3, 4 and 5 have landed, and the composition algebra now exists and is exercised. This body has been rewritten to match what the branch actually carries.
The wave's exit claim is met: a represented operand instance carries a measured error for its own extent, bound to the exact bytes, source, recipe and codec revision that produced it and to its dependency's terminal baseline; stale or unrecognised attestations leave the guarantee unavailable rather than optimistic; and the resulting certificate — composed with the dependency extents actually selected — reaches the floor that gates selection.
Step 1 — the sidecar
A codec can state a radius when its error is a property of the scheme:
F32_PLANEStruncates bit planes and the bound follows from which planes are read.VQ8_SHAREDcannot, because a vector quantiser's assignment error is a property of a fitted codebook against actual weights. This is the authority the codec plane cannot carry.RepresentationAttestationsis an optional versioned sidecar, declared by the index the wayauxiliary_referencesis and absent from every container written before it. One row binds a measurement to the operand and parent extent, codec family and revision, logical shape, content digest, source digest, each dependency's terminal baseline, and the encoder recipe plus attesting authority and method. Judging produces a realFidelityCertificate— the codec plane's own type — so an attested claim and a declared claim compose through one algebra rather than two.Binding to each dependency's terminal identity rather than to whatever depth a plan selects is what keeps this from exploding: otherwise every parent × dependency-depth combination needs its own attestation. The selected depth composes on top at planning time.
Step 2 — the tuple check
Metadata alone, no payload read, exactly as VQ-1 admits an auxiliary closure.
AttestationStatuskeeps apart three answers a singleOptionwould blur, none of which is zero: Absent (and it names which depths are attested, so "no guarantee" is never read as "the file didn't load"), Stale (attested, but measured against something that is no longer there — named by cause), and Bound (the tuple holds; not yet trust).Causes are variants rather than strings, so a caller can act on the difference and a test can assert which check fired.
A finding against the forecast
X3 asked for six staleness causes refused by name. Two are not container-checkable at all — once encoded, the source checkpoint disappears as an authority. They are carried as identity and compared only when a caller who actually has them supplies the expectation. The test asserts both halves (refused when expected, silent when not), because a field only ever checked when nobody supplies it is how an unverifiable claim quietly becomes a decorative one.
Steps 3 and 4 — recognition, then the bytes
Recognition refuses an unrecognised authority or method distinctly from absent and from stale: trusting an authority you do not know is not the same failure as having no measurement.
The digest check is the one thing that cannot be metadata-only. The container holds no per-tensor digest (finding B4), so an attestation binding to content is verifiable only against the content, at preparation, where the payload is being read anyway — a hash, not a second load.
Verifiedis a state of its own, and only it hands over a certificate.Boundnow means the tuple holds and the authority is recognised and nobody has looked at the bytes;AttestationStatus::certificate()returnsNonefor it. An ergonomic accessor that handed over a radius before the payload was checked would defeat the entire plane in one method.The tamper arm and its control are one test: same operand, same attestation, same policy, one byte flipped in the middle — no length change, no metadata change, so only the payload can catch it. Bytes also cannot promote a status that already failed; without that,
verified_againstwould be a back door.Step 5 — the composition, and the phases that protect it
Verification needs the payload, so selection is phased explicitly:
Verifiedclaims only, composed parent with dependency, and the floor decides.There is no provisional selection from
Boundevidence, even if it would be checked later. A plan built on unverified claims and corrected afterwards would, however briefly, assert a guarantee it had not earned, and "briefly" is not a property a guarantee can have. The types enforce it rather than a rule someone must remember: aCandidatecarries no certificate at all, andderiveaccepts onlyVerifiedEvidence, which nothing butverifycan construct.The decisive regression, one artifact and one floor:
Neither half decides it — 0.003 is inside the floor and so is each codebook bound — so only the composition separates them. The premises are
constasserts: editing them so one half alone decides fails the build rather than quietly turning the test into a tautology. The test also asserts that a floor consulting only the parent would have admitted BOTH, which is the over-promise stated as a fact.Time of check, time of use. Hashing proves nothing about the bytes a later decode reads unless both come from the same immutable object, so the
SourceStamp— store id plus overlay generation — travels with the evidence. Two guards, because there are two windows:verifyrefuses a source that moved since ADMISSION, andensure_current_forrefuses one that moved since VERIFICATION.An attested claim replaces the codec's declared one rather than widening it: two statements about the same quantity, one measured on this instance and one derived from the scheme. Adding them would double-count.
Step 6 — the composed bound reaches the real planner
Step 5 built the composition algebra and proved it against hand-built options. Nothing called it.
attested_fidelityhad zero production callers,AttestationTablewas never imported intoprepared.rs, and everyExtentOptionthe planner built came fromcodec.extents()alone — the codec's declared bound, with no knowledge of any dependency. The mechanism was complete and the guarantee was not: the floor that gates selection still made exactly the over-promise this wave exists to remove.select_recordsnow runs the three phases after refusals and before anything consults the floor. Refusals come first so a plan that is already refused never pays for verification.The store learns two things at open, both mirroring the reference table beside them: the attestation table, where a table the index NAMES and the container does not hold is a refusal rather than a silent loss of every guarantee; and
RecognisedMethods, defaulting tonone(). An attestation is carried and checked either way, but acting on one is a TRUST decision that belongs to the caller, not to the container making the claim about itself. The dependency composition is not gated on recognition and applies to declared certificates too — that half is the actual over-promise fix.Unavailable, never optimistic. A missing dependency pin, a dependency whose codec declares no radius, and a composition the metrics refuse all leave the option with no radius at all, which the floor already reads correctly. A composition refusal is deliberately not fatal to the plan.
One canonical derivation for a dependency's terminal baseline. Two independent producers form that string — the encoder that writes an attestation and the planner that checks one — and a format they agree on only by convention is one they will eventually disagree on. Drift there does not fail loudly: every attestation simply goes
Stalewith a changed-baseline cause, indistinguishable from a legitimate re-encode.Why the suite stayed green either way
No shipped codec both declares a radius and requires an auxiliary, so nothing in the suite could tell the declared and composed readings apart.
VQ8_SHAREDhas one terminal extent with no radius;F32_PLANESgrades radii but needs no auxiliary. The forcing case needs purpose-built codecs, andcomposed_floor.rshas them:Neither half decides it, asserted at compile time. A companion test states the over-promise as a fact: the declared bound is identical in both containers and inside the floor in both, so a planner reading it alone would have admitted the coarse artifact too. Under a preparation budget the fine container spends the depth and the coarse one is REFUSED, naming the floor it could not meet.
And the wave's exit claim, in the planner: an attested 0.001 against the same coarse codebook composes to 0.004 and is admitted — a lossy artifact satisfying a quality requirement without anyone inventing a number. The control is the same container, the same attestation, the same bytes, read by a build that recognises nobody: the guarantee is unavailable, selection falls back to the declared 0.006, and the floor refuses it.
Both carriage tests were confirmed to fail with the composition call removed, while the declared-bound control stayed green — the gap is demonstrated, not asserted.
Verification reads are preparation work and are reported as such: one read per attested operand, none for a plan that attests nothing. The
ResourceLedger's ownpreparefigure is priced from declared extents and does not include them — debt D1, named by the freeze and not paid here.Test-quality corrections
0was pinning a coincidence — it would have failed the moment someone putblock.0into the message. It now asserts the refusal does not hand over the specific radius it is refusing.tuple.rscame in at 88% because only one of sevendescribe()arms was ever called. Those are user-facing refusal messages, and an unread one is one nobody can act on. All seven are now exercised, 88% → 100%, by testing the gap rather than waiving it.verifyoriginally took the subject list a second time, so a caller passing a different slice thanadmitreceived would have silently dropped candidates. Verification now carries what admission decided and looks the attestation up by key.Gates
fmt, clippy (larql-vindex, larql-cli),
cargo check --target x86_64-apple-darwin,cargo test -p larql-vindex,cargo test -p larql-cli, doc links — all green. Coverage policy passed at 93.72%.The contract finding — a certificate's referent, and floors that are actually asked
Step 6 exposed an ambiguity worth fixing before an out-of-tree provider freezes this API.
RepresentationFloor::Exacthad always meant "the deepest extent this codec declares" —admitscompared depths and never once consulted a radius. For a lossless progressive codec the two readings coincide. For a lossy one they are not the same claim:VQ8_SHAREDat full depth is every byte the artifact holds and no bound whatever against the tensor it was fitted to. This build would eventually have printed "exact reconstruction" while planning terminal Q4 or VQ data.The referent, settled and written where the type is defined. A certificate measures decoded values against the typed logical source tensor presented at the representation boundary. Not against the stored representation — that reading makes every terminal extent trivially exact, since decoding all of an artifact always reproduces the artifact. Not including kernel arithmetic — that belongs to realization qualification.
TerminalExtentCertifiedExact0.0Within(r)rNeither evidence floor is satisfied by being terminal: an operand with no certificate has made no claim, and no claim is not a small error.
Declarations become honest rather than uniform. A lossless carrier can say
0.0and now does — rawF32is the identity,F16/BF16widen exactly,BF16_ZLIBis byte-identical once inflated. A codec that fits its source still says nothing:Q4_K,Q6_K,Q8_0,NVFP4,MXFP4,VQ8_SHARED. The old contract test asserted "a single-extent codec declares no radius", which conflated extent count with losslessness.And the floors are now enforced, which is the half that made the rest worth committing.
RepresentationFloorwas consulted in exactly one place — the search for a shallower extent under preparation pressure. UnderResidencyBudget::UNBOUNDEDthere is no pressure, so nothing consulted it: a caller could declareCertifiedExact, plan a Q4_K model, and be refused nothing. Enforcement now runs on the initial selection, and deliberately nowhere else — the only assignment toextent.selectedafter the initial pin takes its extent fromshallowest_saving, which already filters by the floor, so a re-check on the way out could never fire, and a refusal that cannot happen is decoration.The witnesses, on a real Q4_K container planned under a budget that asks for nothing:
TerminalExtentplans it while claiming nothing about it;CertifiedExactrefuses, naming the operand, that it states no source-fidelity bound, and that a verified attestation is the one thing that could supply one;Within(1e9)refuses too, because no bound is loose enough to buy a claim that was never made. A companion test covers the opposite half — a composed bound that exists and is merely too large is refused by its number. Removing the enforcement call turns both Q4 refusals red while the structural arm stays green.Step 7 — the out-of-tree acceptance test
An integration test is a separate crate in cargo's model, so it sees only what
larql-vindexexports. Nothing undersrc/was edited for this provider: no match arm names it, no planner branch knows it has two extents, and no policy anywhere knows whoacme-metrologyis.The crate contributes four things this build does not ship — a parent representation, the dependency it decodes through, the role name binding them, and the authority and method that attest an instance.
The genericity claim is checked, not asserted. A test walks every
.rsundercrates/*/srcthat is not itself test code and fails if any of the five external identifiers appears. It carries its own control: a second test looks forVQ8_SHARED— a label this build does ship — through the same walk, so an empty result means "nothing there" rather than "nothing looked at".Each arm has the control that isolates its mechanism:
RecognisedMethods::none()the declared bound stands and the budget has nothing to spendCertifiedExact0.0at the selected extent and the plan is still refused, because the anchor table certifies 0.002Each mechanism was mutated in production code and the corresponding arm verified to fail: recognition fails the recognition arm alone, the content check fails the verification arm alone, composition fails all four fidelity arms.
Two of those mutations were no-ops on the first attempt — one patched a short-circuited path, one patched the wrong file after the carriage moved — and both looked like evidence the arm was weak. The mutation edits now assert they applied, because a mutation that silently does nothing is indistinguishable from a test that proves nothing.
The Q4 lesson, kept as an assertion. A test of representation policy must prove the plan actually contains that representation. An earlier witness in this wave passed while planning f32, because the store resolves the source representation unless opened for the compiled one — it was testing nothing and looked green.
assert_plan_is_the_providersnow checks the operands are the provider's, that both its extents reached the pin, and that its dependency resolved through the role it declared.