Repository navigation
authority(0.7.1g1P2-Step3a): establish certificate consumption as a positive fact - #473
Conversation
b6ea2e6 to
20caeda
Compare
…ositive fact M40-M43 in MutationAuthorityDigestCertificateConsumption, one predicate per function and chained with ?: so the refusal order is readable and the whole consumption is a single expression: only a certificate passing every predicate yields the valid consumption. M44 (single use) is new. M47 now takes the established fact as a parameter instead of rediscovering it, so a disappearance can never become its own evidence - the enforcement is the shape of the API, not a convention a refactor can quietly undo. validConsumptions defaults to the empty set, the fail-closed state, so existing behaviour is unchanged: the eight pre-existing ceremony tests pass untouched. M43 is a named rule with its own diagnostic rather than an implicit consequence of how a certificate was found, so provenance stays visible. Consumption stays bounded: toDigest must equal the verifier's fresh projection, fromDigest must match the cited admission, and admissionSetDigest must equal the exact base authorization set. Two genuine Detekt findings fixed by hand, not baselined: ReturnCount in the consumption chain and the MaxLineLength on the same line.
20caeda to
65fe44c
Compare
|
Merge hold — authority-boundary blocker in Step 3a.
M43 has the same structural gap: Please make successful consumption a first-class attributed result (for example The rest of the slice looks directionally correct. Hold is specifically on making 'valid consumption' and M43 provenance structural facts rather than caller claims. |
There was a problem hiding this comment.
Copilot review overview
🔵 Needs a closer look
It modifies high-stakes quality-gate authority/governance machinery whose consumption rules are only verified at the rule level with the real-task transport lane deliberately deferred, so final human review is warranted.
Review effort: Balanced
Findings: None
What changed in this PR
This PR advances the mutation-authority digest-migration certificate machinery (0.7.1g1P2, Step 3a) in build-logic. Building on #472 — which minted the base-side raw-v1 → authority-v2 certificate as base authority — this slice adds the consumption rules (M40–M43) that establish a positive "this certificate validly authorises this migration" fact, and wires the lifecycle rules M44 (single-use) and M47 (removal custody) to act on that established fact rather than on a certificate's mere disappearance. The design deliberately passes the established consumption set into the ceremony as an input (validConsumptions), so a disappearance can never be re-derived into evidence of consumption, and an empty set remains the fail-closed default. The transport half (wiring the rules to a real Gradle task / certificate ledger loader, and the full T1–T19 matrix) is explicitly deferred to the next slice, so this code is verified at the rule level only.
Changes:
- New
MutationAuthorityDigestCertificateConsumptionobject implementing M40–M43 as a fail-closed?:predicate chain returning a diagnostic ornull. MutationAuthorityDigestCertificateCeremony.checksgains a defaultedvalidConsumptionsparameter, a new M44 single-use check, and M47 removal now permits only established consumptions.- New rule-level test suite with 11 discriminators (T14/T15/T16/T19 and M40–M44/M47 behaviors).
| File | Description |
|---|---|
MutationAuthorityDigestCertificateConsumption.kt |
New consumption verifier: M43 provenance, M40 target-digest, M41 algorithm-pair + source-digest, M42 admission-set, chained fail-closed. |
MutationAuthorityDigestCertificateCeremony.kt |
Adds validConsumptions input, M44 single-use check, and M47 removal gated on established consumptions; backward-compatible default. |
MutationAuthorityDigestCertificateConsumptionTest.kt |
New rule-level discriminators covering the happy path and each refusal (M40–M44, M47). |
I verified that all referenced symbols (admissionSetDigest, byFromDigest, VerificationDiagnostic.failure, DiagnosticCode.MUTATION_RATCHET_AUTHORITY_INVALID, the ALGORITHM_* constants) exist, that the new validConsumptions parameter is defaulted so the existing 8 ceremony tests and the only 3-arg call site still compile, and that the combined M44/M47/M46/M45 behavior is internally consistent for the retained-vs-removed-vs-consumed cases. I found no concrete, objective defect in the logic, diagnostics, or tests.
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
…act, not a caller claim Review blocker on the previous head: Set<String> let a caller state "trust me, this digest was consumed", and certificateFromBase: Boolean let a caller assert M43 provenance. Both are now closed structurally rather than by convention. - CertificateConsumption is a sealed result. M44 and M47 take Set<CertificateConsumption.Valid>, never raw digests, so the attribution travels with the value: there is no way to express an unproven consumption in the lifecycle API. - M43 is derived inside verifyCertificateConsumption by looking the certificate up in the base ledger and comparing enforced payloads. The fromBase Boolean is gone, so provenance cannot drift from the truth, and the two failure modes (absent from base / base payload differing from the cited certificate) are distinct diagnostics. - The Valid constructor is internal, so the normal public API cannot fabricate a fact. Not a capability system: the point is that no ordinary call site can bypass the proof. - verifyCertificateConsumption returns the fact, so Step 3b's call site cannot become part of the authority proof: a refactor cannot add a digest under the wrong condition and have M44/M47 still trust it. Every Valid fact in the tests is obtained by running the real verifier over a real base ledger; none is hand-constructed. Rules untouched: M36/M37 literally unchanged, and validConsumptions still defaults to the empty fail-closed set, so the eight pre-existing ceremony tests pass unmodified. Verification: 33 tests / 0 failures (consumption 13, loader 12, ceremony 8); spotless clean; Detekt baseline 4792 -> 4792 with 0 added; verifyChangePolicy PASSED, class build-logic. All formatting and Detekt findings fixed by hand - no suppression, no baseline entry.
|
Follow-up on the authority-boundary review: the two original blockers are substantially fixed, but one narrow structural hole remains.
CertificateConsumption.Valid(fromDigest, toDigest, admissionSetDigest)and pass it to M44/M47 without running Please make Once that constructor path is closed, the original review blockers are closed from my side; the remaining Step 3b transport/fresh-path proof stays correctly deferred. |
…de the proof
Follow-up blocker: `internal` on the constructor is module-wide, and the Gradle call sites
live in this very module, so Step 3b could still legally write:
val fake = CertificateConsumption.Valid(fromDigest = "...", ...)
and hand it to the ceremony without ever running M40-M43. The fact was attributed, but still
forgeable by ordinary same-module code.
- Valid's constructor is now `private`, so nothing outside the class can construct one -
including other files in build-logic.
- The verification itself moved inside Valid's companion (`Valid.verify`), because that is the
only scope from which a private constructor is reachable. So the proof and the fact live in
the same place by construction: there is no path to a Valid that skips M43-M42.
- The top-level verifyCertificateConsumption now delegates to it, keeping the call-site name
stable while leaving exactly one implementation of the proof.
- @ConsistentCopyVisibility keeps the generated copy() private too, so it is not an escape
hatch under Kotlin 2.3's visibility behaviour.
This property is verified by the compiler, not by a test: the forgery snippet above no longer
compiles. No test needed editing, because the existing tests obtain every fact through the
verifier and never construct one.
Verification: 33 tests / 0 failures; spotless clean; Detekt baseline 4792 -> 4792 with 0 added;
verifyChangePolicy PASSED, 3 changed files, class build-logic.
|
Re-review at head
One non-blocking documentation nit: the file-level KDoc still says "The Valid constructor is Merge gate from my side is now only exact-head CI/freshness. |
… internal Review nit on 861d31a: the file-level KDoc still claimed the Valid constructor is `internal` while the class KDoc and the implementation correctly say `private`. A stale description of a security property is worth correcting rather than leaving, because it is the kind of line a later reader trusts instead of the code. Documentation only - no behaviour, no rule, no test changed.
d192e2e
into
epic/0.7.1-control-plane-authority
Base
9ebe7b4430760ac313874750e7c5ac9bbe56ef1e— the post-#472 epic tip, where the migration certificate already exists as base authority.Scope
Step 3, first slice: the consumption rules the certificate now makes possible, plus M44/M47 acting on the fact they establish.
MutationAuthorityDigestCertificateConsumption.kt(new) — M40, M41, M42, M43. Establishes the positive consumption fact.MutationAuthorityDigestCertificateCeremony.kt— M44 (single use) added; M47 now takes the established fact as a parameter.MutationAuthorityDigestCertificateConsumptionTest.kt(new) — 11 discriminators.Per the design record (§8), M40-M44 belong with the admission-consumption machinery rather than in a new ledger-side file, so the rules live next to the consumption they gate.
The one architectural point
removalChecks(base, candidate, validConsumptions)takes the fact as an input. It does not call the semantic predicates and has no access to them, so it cannot re-derive consumption from a disappearance. "Absence is never evidence of consumption" is enforced by the shape of the API, not by convention — a later refactor cannot quietly reintroduce the inference.M43 is a named rule with its own diagnostic, not an implicit consequence of how the caller found the certificate, so provenance stays visible in diagnostics and tests.
validConsumptionsdefaults to the empty set, which is the fail-closed state: a caller that establishes nothing gets exactly the pre-Step-3 behaviour.Invariants preserved
checks(base, candidate, baseSha)behaviour with no consumptions is unchanged: the existing 8 ceremony tests pass unmodified, so a bare certificate disappearance still fails.fromDigest, one exacttoDigest, one exact admission set, andtoDigestmust equal the verifier's own fresh projection — never candidate-supplied data.Verification
:build-logic:test --tests 'dev.tramai.build.quality.MutationAuthorityDigestCertificate*' --rerun-tasks— BUILD SUCCESSFUL, 31 tests, 0 failures (consumption 11, loader 12, ceremony 8)spotlessKotlinCheck(ratchet-scoped to the base) — BUILD SUCCESSFULverifyStaticAnalysis— BUILD SUCCESSFUL, Detekt baselinebase 4792 -> current 4792; 0 removed, 0 addedverifyChangePolicy -PchangePolicyBase=9ebe7b44…— PASSED, 4 changed files, no policy violationsTwo genuine Defekt findings were found and fixed by hand rather than baselined:
ReturnCountin the consumption chain (restructured into one predicate per function, chained with?:) andMaxLineLengthon the same line.Discriminators in this slice
T14 (candidate-minted authority cannot enter the consumption fact set → M43), T15 (source-digest and admission-set bounds → M41/M42), M40 target-digest refusal, T16 (consumed certificate retained → M44), T19 (removal without an established consumption → M47 fail; removal with one → permitted; removal with a consumption for a different digest → fail).
Not in this PR
The complete matrix and the step's transport half:
AGENTS.mdrequires, and where T7's "fresh path is used" is proven);config/quality/AGENTS.mdfile-roles row for the certificate ledger.Both levels are required by
AGENTS.md, and this slice deliberately stops at the rules so the next one is purely transport plus matrix.Remaining risks
The consumption rules are not yet reachable from a real Gradle task: nothing loads the certificate ledger at a call site, so no real transition can consume a certificate yet. That is the next slice, and until it lands this code is verified at the rule level only.