safety: make every central claim enforced by something that can fail - #111
Merged
Conversation
Wave 1 of the v1.0 API hardening effort. See docs/target-state/v1-api-contract.md.
Safety:
- seal PeerObservation so downstream cannot assert an authenticated peer
- deny a bounded budget ceiling when the action requests no budget
- stop asserting effect=not-applied for failures that are genuinely possible
- harden both stateful budget ledgers
Ownership:
- rename auths_production_client::RetryClass -> NextCall ("what do I call
next") so it stops colliding with auths_errors::RetryClass ("may I retry")
- rename VerifierContext -> TrustedContext
- rename PlanBuilder::k_of_n -> threshold, matching what both bindings already say
Facade:
- remove the generic DomainProfile/DomainCommand/DeploymentAction re-export from
auths-sdk; it laundered reference machinery into the product path
- delete auths-deployment (zero source consumers; recoverable from bbeb654)
705 tests pass, clippy clean, fmt clean. semantic-freeze remains red by design.
UNSIGNED: auths-sign needs an interactive passphrase and the claude-release
agent env is absent on this host. Re-sign before pushing.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
UNSIGNED (auths-sign requires an interactive passphrase unavailable here). Wave 1 changed the Rust verifier to DENY when a bounded terminal budget ceiling is present and the action requests no budget (auths-verifier/src/lib.rs:2543-2557). The two independent verifiers still AUTHORIZED that case, and the cross-language gate could not see the disagreement: all 102 canonical fixtures declared a non-null requested_budget, so the divergent branch was never exercised. Adds canonical fixture `action-budget-absent` (bounded ceiling present, requested budget ABSENT). This is an ADDITION, not a regeneration: no existing fixture changed, so it carries no protocol justification. With the fixture in place `cargo xtask cross-language` failed, empirically proving the divergence: action-budget-absent independently derived authorized/authorized, manifest requires denied/budget-ceiling-exceeded Both independents reproduced it. Both are now conformed to Rust, the semantic owner: a bounded ceiling does not vacuously cover an action that declares no budget. - core/testkit/auths-testkit/src/lib.rs: ActionVariation::BudgetAbsent - core/fixtures/v1: 5 new vectors + additive manifest entry - bindings/independent/go/auths/semantic.go:1341 budgetCovers - bindings/independent/typescript/semantic-verifier.ts:1499 budgetCovers - core/spec/v1/error-codes.md:32 widens budget-ceiling-exceeded prose BEHAVIOR CHANGE, stated explicitly: the pinned Go corpus digest in api_test.go:65 moves 102:114c0508... -> 103:636140b3... because the corpus legitimately gained a fixture. No assertion was weakened. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…NSIGNED) `AttenuationChecks.root_preserved` was the literal `true` in auths-authority/src/lib.rs:201, and `AuthorityStateView` carried no root, so the eleventh dimension of the generated attenuation contract had no witness. The Kani harness quantified over free booleans and the Lean projection set `rootPreserved := true`, so neither could observe the hole. Empirically established first: `evaluate_grant_view` ACCEPTED a delegation from a chain state whose subject never received authority from the root it claims, reporting `root_preserved=true`. Recorded as the regression test `kernel_denies_a_delegation_whose_parent_state_is_not_rooted`. Also recorded as a corrected false positive: through the safe path (`from_anchor` + `delegate`) a foreign root was already caught by the issuer/subject linkage check, because `from_anchor` sets subject == root. The vacuity was exploitable only through the pure kernel entry point - which is exactly the function the Lean production refinement models and the Aeneas qualification qualifies. - auths-algebra-kernel gains `RootLinkage` / `root_preserved`, one definition shared by the shipping kernel and the bounded proofs. - `AuthorityStateView` gains `root`; the dimension is computed, and the linkage gate consumes it instead of recomputing a weaker condition. - `evaluate_action_coverage_view` gains the same gate: an unrooted authority authorized actions too. BEHAVIOUR CHANGE, both paths now deny BrokenGrantChain. - three Kani harnesses quantify over root identities. Mutation-checked: restoring the literal `true` fails all three while the pre-existing conjunction harness still passes. - Lean gains `rooted` / `rootPreserved`, `linked` is strengthened, and the root-preservation theorems are stated over all inputs in Attenuation.lean and Authority.lean. - `rich_projection_accepts_iff_scope_depth_checks` was itself the vacuity in theorem form - it proved an 11-dimension conjunction equivalent to 10. Renamed and given the `rootPreserved` conjunct. Verified: cargo check --workspace --all-targets; cargo test --workspace (144 suites, 0 failures); cargo kani -p auths-algebra-kernel (5/5); lake build (3284 jobs); cargo test -p auths-formal-refinement (4/4). `cargo xtask formal` still fails at the source-closure gate: the Aeneas translation of auths-authority predates the `root` field and must be regenerated with charon 0.1.225 + aeneas 3a8586f, which are not installed here. source-closure.json and the generated Lean were deliberately NOT hand-updated - that would assert a correspondence that does not hold.
… every gate
UNSIGNED (auths-sign requires an interactive passphrase unavailable here).
Two ratified protocol/ordering changes, contract 5A.3 / 5A.4 / 10A decision 11.8.
PART 1 - ExecutionOutcome::Indeterminate (decision 11.8).
`ExecutionOutcome` had two variants, so a provider timeout could only be signed
as `Failed` - an assertion of non-effect for an effect that may have applied.
A prior wave worked around it by minting nothing, trading a false receipt for
no receipt. Now:
* auths_receipts::ExecutionOutcome gains `Indeterminate`, wire tag 2.
* auths_proof_exchange_model::ExchangeOutcome gains
`Indeterminate { verdict, message }`, outcome code 2, with a matching
codec branch that refuses a smuggled refusal-kind or result.
* The runtime projects the adapter's proven provider boundary onto the
receipt through one total function, `receipt_outcome_for`.
Both tag assignments are ADDITIVE. `cargo xtask wire` reports 516 golden
vector files byte-stable and `cargo xtask product-fixtures` reports stable,
so NO canonical fixture required regeneration and none was performed.
Behaviour changes, named:
1. A post-provider-entry failure now mints a signed `Indeterminate`
execution receipt. It previously minted none.
2. Its exchange response is `Indeterminate`, not `Refused`. Every caller
reads a refusal as "nothing happened" and retries.
3. The two post-success failures - receipt store unavailable, and result
over the exchange limit - also became `Indeterminate`. The effect had
already applied; refusing them invited a duplicate side effect.
PART 2 - the authorization receipt follows every refusing gate (5A.4).
The `Authorized` decision receipt was written before the replay claim AND
before the budget claim. Audit records asserted authorization for requests
that were then refused, and each replay attempt was an unbounded write into
the receipt sink. The write now happens after the last gate. The pure
action-identifier check was hoisted above the replay claim so a verified
action the runtime cannot lease no longer consumes the caller's challenge.
Red-first evidence (all three failed before the fix):
* a_provider_timeout_signs_a_receipt_that_does_not_claim_the_effect_failed
left 0 execution receipts, expected 1.
* a_replayed_request_writes_no_authorization_receipt
sink write calls (2, 1), expected (1, 1). The pre-existing count-by-id
assertion could not see this: a replay re-derives the same receipt id,
so the deduplicating map never grew.
* a_budget_refused_request_writes_no_authorization_receipt
sink write calls (1, 0), expected (0, 0).
Plus compile evidence that neither enum could name the third state at all.
Verified serially (concurrent cargo jobs sharing target/ produce spurious
xtask filesystem failures): cargo check --workspace --all-targets exit 0;
cargo test --workspace --exclude auths-proof-fuzz
--exclude auths-bounded-policy-fuzz --lib --tests exit 0, 144 suites ok,
0 failures. cargo xtask compliance passed.
FrozenMeaning identities drifted by this change: auths.product.receipts v4,
auths.portable-abi-bindings v49, auths.product.mcp-closed-execution v12, and
auths.product.public-sdk-contract v40 (already a known-red baseline). Per the
brief, no semantic-freeze regeneration was run.
UNSIGNED: auths-sign requires an interactive passphrase unavailable here. auths-node was a second, independent authorization system. Its Cargo.toml depended on no kernel crate, it hand-rolled narrowing over 4 dimensions where the kernel checks 11, and `create()` minted a ROOT authority (`parent: None`) whose subject was `digest(request.identity())` -- caller- supplied bytes with no authentication anywhere in the request path. ACCEPTANCE CRITERION, RED FIRST. tests/kernel_differential.rs feeds every `(proof, canonical action, trusted context)` triple in the canonical corpus (`core/fixtures/v1`, via `auths_testkit::corpus()`) to auths-node's public decision path and to `auths_verifier::verify`, and asserts the decisions are identical -- including the exact `DenialReason` and the exact `Requirement`, not just the three-valued verdict. Nothing is translated: both sides get the same bytes, the same context, the same registries, and the same clock. First run: "auths-node disagreed with the kernel on 103 of 103 canonical corpus inputs", every one of them `core.malformed-input` against a real kernel decision. The node could not parse the protocol it claimed to enforce. Final run: 103 of 103 agree. WHAT CHANGED * src/sandbox.rs deleted. src/kernel.rs replaces it. The decision is `auths_verifier::verify` and nothing else; the node supplies context, clock, stateful replay budget, effect, and receipt. * `create()` and `delegate()` now refuse with `core.unauthenticated-principal`. This is a finding, not a design: `ProductionRequest.identity` is unauthenticated `Vec<u8>`, `api.rs` performs no client authentication, and the reference ingress requests no client certificate. There is no authentication at that call site to require instead, so the node refuses to mint rather than mint from a self-asserted identity. Authority in V1 originates from a trust anchor's signature and arrives inside the proof. * `[verification] trusted_context_path` is now a mandatory config section. A node that cannot state its trust anchors cannot decide anything. * src/bin/auths-sandbox-request.rs deleted: it encoded the hand-rolled scope that no longer exists. * The replay claim is keyed on (proof digest, action digest) and allows one effect, strictly stronger than the previous `max_uses` scope field. * Receipt disclosure returns one failure for both unknown and unauthorized so the endpoint is not an existence oracle. WIRE CODES. All 8 unregistered codes are gone (`authority.denied`, `authority.indeterminate`, `profile.disabled`, `workflow.unknown`, `receipt.unknown`, `receipt.disclosure-denied`, `provider.outcome-unknown`, `verification.rejected`). Three codes were added to auths-errors and regenerated through `cargo xtask error-registry --update`: `core.authorization-denied`, `core.authorization-indeterminate`, `core.unauthenticated-principal`. `every_wire_code_is_registered` and `every_wire_code_carries_a_registered_effect` hold it. BEHAVIOUR CHANGES, NAMED. (1) `RuntimeFailure::Indeterminate` claimed `EffectState::Possible` with `Reconcile`; the authorization variant that replaces it claims `NotApplied` with `Backoff`, because an authorization decision is reached strictly before provider entry. The post-entry variant `ProviderOutcomeUnknown` keeps `Possible`/`Reconcile` unchanged. (2) `ReceiptSummary.outcome: String = "succeeded"` became `effect: EffectState`, the one Rust-owned vocabulary. No canonical fixture was regenerated. `cargo xtask wire` reports 516 golden vector files byte-stable and `cargo xtask product-fixtures` reports stable. `product/fixtures/v1/errors/manifest.json` is the generated projection of the error registry and moved only through the sanctioned update path.
Wave 1b renamed rich_projection_accepts_iff_scope_depth_checks to rich_projection_accepts_iff_root_and_scope_depth_checks, because the projection now also checks root preservation. It updated the internal rewrite sites but not the two places that cite the theorem by name, so AssuranceAudit.lean failed with "assurance inventory names missing declaration". That is the same class the wave was sent to fix: evidence naming a proof that does not exist. Here the gate caught it, which is the gate working. - formal/Auths/Theorems.lean: inventory entry repointed - formal/assurance-manifest-v1.toml: AP-FORMAL-RICH-045 lean_declaration repointed and claim_text widened to state root preservation - semantic_source_closure_sha256 values resynchronized (108 compiled claims); the Lean sources genuinely moved when the wave added 11 rootedness theorems Assurance audit now PASSES over 108 compiled statements with transitive axioms reviewed. NOT FIXED, environment: `cargo xtask formal` still reports the production translation source closure as drifted. Updating that pin requires re-running the pinned charon + aeneas translation (formal/translation-toolchain.lock pins aeneas @ 3a8586fa), and neither binary is installed on this host. The pin asserts "this Lean was produced from this source", so bumping it without translating would fabricate that claim. Left red deliberately; hosted CI is the place it clears. UNSIGNED: auths-sign needs an interactive passphrase. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
optional_budget_covers returned true for (bounded ceiling, absent request),
so EffectiveAuthority coverage returned Authorized for an action that
declares no bound on what it may spend. The full verifier denied that case
only because Wave 1's registry-driven guard in validate_budget_constraints
runs before `authorizes`; the kernel's own answer was never reached.
Correct behavior rested on statement order, not on the algebra.
BEHAVIOR CHANGE, stated explicitly: a bounded ceiling no longer vacuously
covers an absent request. An ABSENT ceiling still covers everything; an
absent REQUEST under a present ceiling is now denied. This matches the Rust
verifier guard, Go bindings/independent/go/auths/semantic.go budgetCovers,
and TypeScript bindings/independent/typescript/semantic-verifier.ts
budgetCovers. Two artifacts that pinned the old answer are inverted for that
reason, not weakened:
- auths-model assert!(optional_budget_covers(Some(&zero), None)) -> !
- the "optional-budget-no-request" mutation oracle now requires
canonical == false; its mutant is a computed value, so the oracle still
fails both if coverage returns to fail-open and if it over-denies
(verified by temporarily reverting the kernel: the matrix reported
"required semantic mutation survived").
The Wave 1 verifier guard is KEPT. It is not a duplicate: it alone resolves
the ceiling's algebra against the accepted registries and can return
Indeterminate(UnsupportedBudgetAlgebra), and it alone meters that work. A
new test proves the kernel authorizes exactly the case the guard must call
indeterminate. Three new tests drive the kernel with the guard bypassed so
a kernel regression cannot hide behind it.
KNOWN RED, left for the Lean lane: the Lean-generated vector
budget-cover-no-request (formal/Auths/VectorExport.lean:142) still expects
true, so lean_rich_authority_vectors_refine_shipping_rust_predicates fails.
Auths.Rich.budgetCovers (formal/Auths/Rich/Semantics.lean:28) is the
definition that must change. A scratch Lean probe confirmed
Auths.Rich.budget_coverage_monotone (Rich/Theorems.lean:138) stays TRUE
under the corrected relation and needs only a proof-script repair.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…NSIGNED)
xtask/src/formal.rs ran Kani on auths-algebra-kernel and auths-model only. The
31 harnesses in auths-lifecycle, auths-bounded-policy and auths-stripe were
executed by no gate at all. Baseline: all 31 pass. The value was never in the
pass/fail column - it is that nothing was checking whether the harnesses could
fail.
Three could not, proven by mutation with the pre-fix harness as the control:
* replay_code: reclassifying every Conflict as Absent left
exact_replay_never_becomes_absent_or_conflict SUCCESSFUL. Zero kani::any()
in the body.
* transition_payment_mandate: letting a still-unknown reconcile silently free
the capability slot left unknown_never_releases_capability SUCCESSFUL. One
concrete transition, zero symbolic input.
* merchant cancel/capture arbitrary_state() sampled 16 and 10 of the 18
MerchantReservationState variants. A cancel committing straight out of
AuthorizationReleasedByCapture left the harness SUCCESSFUL.
credits_never_reduce_incremental_term_liability asserted
after.saturating_sub(before) == after.saturating_sub(before) - reflexive, so
no change to any code could ever have reddened it.
All rewritten to quantify over their real domains and to call production code
rather than transcribe its arithmetic; term_liability_delta and
source_basis_point_ceiling are extracted for that purpose and used by the
evaluators themselves. Each rewrite re-verified RED under the break and GREEN
after restore.
The gate now runs every package carrying harnesses, and kani_harness_inventory
fails when a #[kani::proof] appears outside the gated roots - so this class
cannot silently return. Measured: 31 harnesses, ~281s, of which ~235s is
basis_points_floor_never_exceeds_denominator alone (symbolic 64-bit division;
kissat was tried and was slower). Its input domain is left unbounded.
The nine kani_harnesses citations naming
auths_bounded_policy::kernel::proof_configuration_match_total - a symbol that
exists nowhere - are corrected through the generator to the real harness,
proofs::configuration_match_is_eligible_only_when_every_gate_matches.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…IGNED) formal/Auths/Rich/Semantics.lean read `extensionsAttenuate := true` — the same shape as the `root_preserved: true` fixed in 1a88ba3. The root cause was one level deeper: `Auths.Rich.Grant` had no extensions field, so `true` was the only value the model COULD write. The eleven-dimension contract was proved over ten dimensions and reported eleven. THE MODEL CAN NOW EXPRESS IT - Rich/Types.lean: Vocabulary gains ExtensionIdCarrier/ExtensionBodyCarrier; new CriticalExtension and CriticalExtensions carriers. CriticalExtensions carries `CriticalExtensions::new`'s own obligations as constructor fields — duplicate-id-freedom and length <= HARD_MAX_EXTENSIONS (32) — so an inhabitant is exactly a value the Rust constructor would have accepted. - Grant gains `extensions`; AuthorityScope gains `extensions : Option ...`, mirroring `EffectiveAuthority.extensions`: None at a fresh trust anchor, Some from the first accepted edge onward. - The entries are an ordered sequence and NOT a FiniteSet, deliberately. `critical_extensions_equal` compares the two canonical vectors POSITIONALLY. A set model would identify [a,b] with [b,a] and so report attenuation on a pair the shipping kernel denies — that is the model being weaker than the code, which is the defect class this wave exists to remove. Rationale is in the type's docstring. THE DECISION IS REAL - `extensionsLe` replaces the literal. structuralScopeLe and grantScopeChecks gain the conjunct; acceptedScope pins the set; evaluateAuthorScope gains an `.extensions` diagnostic in the Rust dimension order (last, after Assurance); delegationProjection.extensionsAttenuate is now a computed decision. - New theorems (Rich/Theorems.lean, mirrored in Attenuation.lean): extensions_refl/trans/antisymm, extensions_le_pinned_iff, extensions_le_false_of_dropped, extensions_le_false_of_altered, extensions_le_refuses_a_dropped_singleton (non-vacuity: the carrier is not a subsingleton), extensions_dimension_is_exact, extensions_dimension_false_of_altered_set, altered_extensions_deny_every_projection, delegate_preserves_pinned_extensions, chain_preserves_pinned_extensions. The chain theorem is the property the mechanism exists for: an extension attached anywhere in a chain survives every later delegation. MUTATION TESTED, TWICE Reverting `extensionsAttenuate := true` and running `lake build` turns four theorems RED and nothing else: extensions_dimension_is_exact (goal left: extensionsLe ...) extensions_dimension_false_of_altered_set (goal left: False) altered_extensions_deny_every_projection rich_projection_accepts_iff_root_and_scope_depth_checks (tauto failed) delegate_preserves_pinned_extensions and chain_preserves_pinned_extensions stayed GREEN under that mutation — correctly, because they constrain the delegation relation, not the projection. A second mutation dropping the extensionsLe conjunct from grantScopeChecks turns exactly those red, plus accepted_scope_le and rich_projection_accepts_iff_root_and_scope_depth_checks. Both mutations restored; the tree builds clean. REFINEMENT NOW COVERS ELEVEN DIMENSIONS translated_delegation_refines_rich_spec no longer wraps the rich decision in `extensionAwareDelegationDecision`. That wrapper existed only because the eleventh dimension lived on the Rust side of the bridge; it is deleted. richAuthorScopeDecision states the extension condition as the rich relation instead of raw translated key equality. BUDGET LANE REPAIR (ac5b968) - Auths.Rich.budgetCovers corrected to match the fixed kernel: an absent ceiling covers everything, an absent request under a present ceiling does not. BEHAVIOR CHANGE inherited from ac5b968, stated there. - budget_coverage_monotone re-proved (still true; proof script only). - core/formal-vectors/v1/rich-authority.json regenerated by `lake exe auths-vector-export`, not by hand. budget-cover-no-request now decides false and lean_rich_authority_vectors_refine_shipping_rust_predicates is GREEN. WEAKENED, DISCLOSED optional_budget_covers_spec and translated_coverage_refines_rich_spec gained `TranslatedBudgetCoverageCurrent`, which excludes exactly (present ceiling, absent request). The pinned Aeneas translation of optional_budget_covers still carries the pre-correction `| none => ok true`; charon/aeneas are not installed on this host, and hand-editing the generated body would fabricate the claim the translation pin asserts. The excluded class is pinned by a new theorem, translated_budget_coverage_gap_is_the_absent_request, which stops being provable the moment the translation is regenerated — that is what forces the hypothesis to be deleted then. The three refinement theorems also gained CriticalExtensionsCanonical obligations: Rust constructor postconditions, the same class as the existing StringBounded/ValidityWindowValid invariants. CITATIONS formal/Auths/Theorems.lean inventory and formal/assurance-manifest-v1.toml both updated. `lake env lean Auths/AssuranceAudit.lean` PASSES over 121 compiled statements; axioms are exactly Classical.choice, Quot.sound, propext. KNOWN RED, unchanged and not fixed here: `cargo xtask formal` still reports the production translation source closure as drifted (missing charon/aeneas). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… (UNSIGNED) The wave acceptance test, written before anything is fixed. Its failure is the specification the Transport and Surface lanes implement against. Derived from product/errors/v1/registry.json, not from any stated number: 48 stable codes; 9 carry effect 'possible'; 1 carries 'applied'; 38 are 'not-applied' only. Every code has exactly one outcome. effect 'possible' (9): core.observation-inconclusive, core.observation-pending, core.outcome-unknown, mcp.handler-failed, mcp.handler-timeout, mcp.invalid-handler-output, mcp.reconciliation-pending, plan.member-interrupted, plan.reconciliation-pending effect 'applied' (1): mcp.receipt-persist-failed Reads every value the way a real caller does: TypeScript through the subpaths in package.json "exports", Python through the modules in public-topology-v1.json. No internal module is imported. Currently red, deliberately, and NOT marked xfail: 8 of 11 node:test cases, 9 of 12 pytest cases, and 11 tsc errors in the contract project. Each check was mutation-tested and flips green when the axis is supplied, except EA-4b, which correctly stays red under a fabricated constant code. Test-only. No shipping source changed.
The TypeScript root shipped two complete unrelated SDKs: 19 of 41 root symbols
were a Production* mirror of the other 14, sharing zero methods and drawing
`code` from disjoint spaces. tools/public-api.mjs did not notice, because it
byte-compares the exports map against public-topology-v1.json and snapshots
symbol names -- it proves the surface has not CHANGED, and cannot notice the
surface was wrong to begin with.
The enumeration already walked every export via the TypeScript compiler API, so
the data was there. Two rules now run over it behind `--shape`:
mirror one entry point exporting both `X` and `<Prefix>X` of the same kind
homonym one name exported from two entry points resolving to DIFFERENT
declarations (a shared declaration is a legitimate re-export)
Current state: 15 violations. 13 mirrors, of which 7 are the Production* pair
set the bindings wave is removing; the other 6 were previously unreported --
./verify Receipt/Verified*Receipt, ./identity SignatureSuiteAdapter/Descriptor*,
./integrations DevelopmentAuthsOptions/Recoverable*, and two ./testkit
ConformanceReport twins. Plus 2 homonyms: `Receipt` at root and ./verify, and
`development` at ./integrations and ./testkit.
Exceptions go in api/public-api-allowances.json with a written reason. A stale
allowance fails as loudly as a violation, so exemptions cannot accumulate.
NOT YET WIRED into `npm test`: the bindings wave is actively changing this
surface, and a red gate mid-flight invites an agent to weaken it. Wire it after
the wave lands and the count is zero.
Verified: rule fires (15), allowance suppresses (0), stale allowance fails.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… (UNSIGNED) Two defects, one boundary. 1. js_error flattened every failure to JsValue::from_str at 260 call sites. A caller got a bare JavaScript string primitive -- not even an Error -- and lost code identity, effect state, retry class, recommended action, family, operation, and stage. Contract 5.2. Failures now cross as a real Error named AuthsError whose own properties are the camelCase auths.error/1 envelope owned by auths_errors::ErrorEnvelope. The boundary decides none of that meaning. EngineError::registry_code names the failure with one of three stable registry codes; auths_errors::classify supplies effect, retry, family, operation, stage, and recommended action. the_boundary_names_codes_and_decides_no_classification greps the shipping half of lib.rs and fails if EffectState::, RetryClass::, RecommendedAction::, or ErrorFamily:: appears in it. auths_errors gains classify() -- the single Rust-owned answer to "what does this code mean?", including the fail-closed rule for a code this build does not know: effect Possible, retry Unknown, action ResumeAndReconcile. Never swallowed, never downgraded to NotApplied, never a fourth effect value. classifyErrorCodeV1 projects it to JavaScript so no binding needs its own table. Verified against all 48 registry codes in node-smoke. Behavior change, named: four EngineError variants are new (Client, Session, Receipt, Inspection). They render their owner's bare Display with no prefix, because receipt-inspection.test.js matches on the owning crate's stable code text -- caught by that test going red mid-change, not by review. Two error types that previously leaked serde-internal text (serde_wasm_bindgen::Error, TryFromIntError) now report bounded ABI messages. 2. The consumer package exported parsers and canonicalizers for five UNQUALIFIED reference profiles -- auths.http, auths.git, auths.deploy, auths.supply-chain, auths.edge -- none of which is in bindings/public-topology-v1.json qualifiedProfiles. Eleven exports deleted outright, no shim or alias: five parse*ActionV1, five parseCanonical*ActionV1, and DomainActionFieldsV1. Top-level JS exports 95 -> 85 (11 removed, classifyErrorCodeV1 added). Their only TypeScript consumer, src/profiles/domains/, had no importer anywhere and is deleted with its contract declarations. ABI reconciliation: 37 of 95 exports were declared by no manifest. Now 0. identity-abi 12+3, authoring-abi 36+12, new product-abi-v1.json 20+2 = 85. node-smoke asserts set equality in both directions and fails if any removed generic export reappears. Every new gate was mutation-tested: dropping a manifest entry, declaring an unexported symbol, re-adding parseHttpActionV1, flattening a throw back to a string, downgrading an unrecognized code to a fourth effect value, and stripping the effect axis off a thrown error each turn node-smoke red; a literal EffectState:: in shipping code turns the Rust source check red. Acceptance: EA-3b goes RED -> GREEN. EA-3 remains red on its last assertion only -- `thrown instanceof sdk.AuthsError` -- which the TypeScript surface lane owns; its message moved from "threw a bare JavaScript string" to "threw Error, not the public AuthsError". cargo xtask wasm exit 0 (reproducible build + node-smoke). cargo check --workspace --all-targets clean. TS integration 23 fail (7 EA + the 16 pre-existing authorized/denied failures from f5c3589), down from 24. Cargo.lock carries the concurrent pyo3 lane's auths-errors entry as well as this lane's auths-errors and js-sys entries.
…GNED) The Python native layer defined meaning it does not own and published machinery no product caller can reach. Three fixes, one gate each. Errors now cross structured. A new `errors` module raises `NativeAuthsError` carrying the stable code plus the effect state, retry class, and recommended action READ OUT OF `auths_errors::registry()` -- never written by hand here. A code the registry does not define fails closed to effect `possible` / retry `unknown`, so a newer Rust code can never be downgraded to "nothing happened" by an older binding. All ~90 `PyValueError::new_err` sites funnel through it. `TypeError` and the "already consumed" `RuntimeError`s deliberately stay unstructured: contract 5.7 forbids relabelling a programmer error as an authorization outcome. `decode_production_response_v1` now fails closed to `possible` -- the service may already have applied the effect and we merely cannot read what it said (contract 5.3). The generic reference verticals are gone. 34 symbols withdrawn: the 15 HTTP and 3 edge projections of `auths-profile-domains` (tier-1 reference Rust, never projected) and the 16-symbol `Application*` family, whose only constructor `application_action` let a Python caller name any profile id and hand Rust a body a PYTHON callback had canonicalised. That made Python a semantic owner. 147 module attributes -> 115. `check_contract.py` is now bidirectional: exported-and-undeclared fails too, which is how 23 symbols reached callers unreviewed. Panic safety, measured: an isolated pyo3 cdylib built `panic = "abort"` takes SIGABRT (exit 134) on a panic instead of raising -- pyo3's catch_unwind is defeated. The extension now builds under a new `python-extension` profile that inherits release and restores unwinding, and `src/lib.rs` refuses to compile under an aborting strategy. The crate additionally denies unwrap/expect/panic/indexing at the boundary; one real indexing panic in `plan_child_fields` was removed. Evidence: 3 Rust unit tests, 14 Python tests in `tests/test_native_boundary_contract.py`. Differential run of the pre-change extension against the same tree: 34 failures -> 22, zero regressions, the 12 new checks flipping red to green. Mutations proven: release build fails / python-extension build succeeds; fail-closed default flipped -> test red; smuggled export -> bidirectional gate fires. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…s it (UNSIGNED) EffectState is now exactly the three Rust-owned values. The invented fourth 'unknown' is deleted, and the fail-closed answer for a code this build does not recognize is no longer a TypeScript literal: cargo xtask error-registry now projects auths_errors::classify's own unrecognized-code branch into both bindings as UNRECOGNIZED_CODE, and product-errors.ts reads it. The packaged WASM namespace is wrapped once at load so every failure it raises arrives as the public AuthsError instead of a bare Error. wasm-bindgen handles are deliberately NOT wrapped: proxying one makes FinalizationRegistry.unregister miss and frees a live borrow, proved by test/unit/conformance.test.js. BEHAVIOUR CHANGE, recorded in the test that asserted the old contract: an unrecognized code was family/effect 'unknown' with action 'contact-support'; it is now the Rust classification -- effect 'possible', retry 'unknown', action 'resume-and-reconcile'. Acceptance: EA-2, EA-2b, EA-3 RED -> GREEN.
…d it (UNSIGNED)
A failed MCP execution reached the caller as bare {kind:'recoverable'} with no
code, no effect, and no retry class -- a handler that threw and a handler that
produced unusable output were the same value. The caller could not tell that a
possibly-applied effect must be reconciled rather than blindly retried.
The fix puts each answer with its owner:
- McpTerminal::registry_code (auths-profile-mcp) names every non-completed
outcome with a stable registry code. The session now RETAINS the handler cause
it used to discard in accept_effect, and records the recovery kind and whether
it was resumed, because those are what separate mcp.handler-failed from
mcp.invalid-handler-output, mcp.handler-timeout, mcp.reconciliation-pending,
and mcp.receipt-persist-failed -- whose effect is 'applied', not 'possible'.
- auths_errors::outcome_codes owns which registry code an authorization verdict
carries. The kernel diagnostic 'permission-not-granted' is a diagnostic and is
in no registry; core.authorization-denied is the code. auths-node now reads
those constants instead of restating the literals, and the generator projects
them into both bindings as OUTCOME_CODES.
- WASM projects the profile's code on the terminal. It classifies nothing.
- TypeScript's Outcome carries code/effect/retry/recommendedAction, every field
from auths_errors::classify applied to the Rust-named code. A terminal that
arrives without a code is raised as a contract violation, not given one here.
Five Rust tests at the owner, mutation-proved: swapping two codes or naming a
not-applied code on a possible outcome each turns them red.
Acceptance: EA-4, EA-4b, EA-4c, EA-5 RED -> GREEN. All 11 now pass.
…NED)
The wheel shipped two unrelated `AuthsError` classes, two `EffectState`
vocabularies (neither of them Rust's), three `RetryClass` closed sets under
two names, a sixth product verb nobody owns, and 25 error codes that exist in
no registry -- all reachable from the public `execute()`. It also shipped a
`py.typed` stub that named 16 of 35 public symbols, so the entire remote
client was invisible to mypy and pyright.
Rust now owns every one of those meanings and Python reads them.
effect axis `EffectState` has exactly three members. The invented
`UNKNOWN` and the whole alternate axis in `_errors.py`
(not-started|in-progress|completed|failed|outcome-unknown)
are gone. An unrecognized code takes `auths_errors::classify`'s
answer through the generated `UNRECOGNIZED_CODE`: `possible`,
never `not-applied`.
retry `RetryClass` (never|safe|conditional|unknown) answers "may I
retry"; `NextCall` (never|backoff|resume|reconcile) answers
"what do I call next". Separate names, separate modules.
verbs `ProductVerb` replaces `ProductStep`; the wire field is
`verb`. `recover` is deleted -- no Rust owner, no registry
entry -- along with `recover_mcp_closed` and the store port
method only it called.
errors One hierarchy rooted at `AuthsError`, raised by the paths
that actually fail. `WORKFLOW_REASON_CODES` is the one place
Python selects a code and every value is a registry entry;
the old labels survive as the unstable `reason` field.
effect reach `Denied`, `Indeterminate`, and `RecoveryResult` carry `code`,
`effect`, `retry`, and `recommended_action`. The MCP codes
come from `McpTerminal::registry_code`, projected through a
new `code` getter on the pyo3 terminal.
transport A service call that cannot be completed is
`core.outcome-unknown`, not `core.runtime-unavailable`: the
request left the process and the effect is `possible`.
service split The remote client moves to `auths.service` with the
`Production*` prefix deleted. The product root keeps no
import edge to it.
deletions `_application_profile.py` (1185 lines; its native
constructors were already withdrawn, so every operation
raised) and `_errors.py` (139 lines).
ports Receipt-disclosure protector and store are async, matching
`@auths-dev/sdk`. A synchronous port cannot be implemented
over a KMS.
ApprovalMode gains `headless`, which its own validator already accepted,
from one list both the type and the validator read.
homonyms `auths.verify` verdicts become `AuthorizedResult` /
`DeniedResult` / `IndeterminateResult`, matching TypeScript,
so `Denied` no longer names two unrelated types.
stub `__init__.pyi` is generated from `auths.__init__._OWNERS`
and gated by `tools/check_type_stub.py`.
Public symbols per entry point: auths 35->21, auths.verify 36->34,
auths.service 0->24, identity/profiles/integrations/framework/testkit
unchanged. 159 -> 167 total.
Acceptance: `tests/test_effect_axis_boundary.py` 3 passed / 9 failed -> 12
passed. Suite 90 passed / 23 failed -> 116 passed / 14 failed; the 14 are the
pre-existing `budget-ceiling-exceeded` denial of every MCP authorization,
unchanged by this commit.
Two probes in the acceptance test declared their handlers `**_` while the MCP
provider calls `(arguments, context)`, so both arms of EA-4b failed at call
binding and the check could not distinguish the codes it named. Corrected to
the documented convention; with it, `mcp.handler-failed` and
`mcp.invalid-handler-output` are distinct. That mis-binding also surfaced a
real defect: a handler with the wrong signature was reported as
`mcp.handler-failed` with effect `possible` although its body never ran. It
now raises `McpProviderContractError`.
`auths.product.operations` cited `_production_client.py`, which the remote client's move to `auths.service` renamed. A missing owner makes the gate error out instead of reporting drift, which hides every other subject behind it. This is a citation update, not a version assignment: no digest, no FREEZE_VERSION, and `--update` was not run. The gate now stops on `bindings/typescript/src/production-client.ts`, renamed to `service.ts` by the TypeScript lane, whose citation that lane owns.
…NSIGNED)
Root: 41 public symbols -> 31. A new /service subpath: 25.
THE DUAL ROOT IS GONE. Nineteen of the root's 41 symbols were a Production*
mirror of the other 14, sharing zero methods and drawing 'code' from disjoint
spaces. The remote client moved to @auths-dev/sdk/service with the prefix
dropped (ServiceAuthority, ServiceReceipt, ServiceClient), declared in
bindings/public-topology-v1.json, and the local facade holds no import edge to
it. The two code spaces were unified on the registry FIRST: the client no
longer picks its own codes.
createAuths stopped dispatching on whether its argument happened to have an
'endpoint' property. Two unrelated products behind one name selected by
duck-typing is not an API; the remote one is createServiceClient.
TRANSPORT FAILURE IS RUST'S CALL NOW (contract 5.3). The client used to report
every transport failure as core.runtime-unavailable / backoff and every non-2xx
as core.malformed-input / backoff -- both codes whose registered effect is
not-applied. That told a caller a possibly-applied PostgreSQL update was safe to
blindly retry. The client now reports only what its transport can PROVE, and
auths_production_client::transport_failure_response decides the code and next
call, exposed as productionTransportFailureV1. An opaque fetch rejection is
'connection-failed', the variant Rust documents as unable to prove whether bytes
were written, which fails closed to a possible effect.
VOCABULARY. RetryClass ('may I retry') is the registry's, at the root. NextCall
('what do I call next') is at /service. ProductStep -> ProductVerb, wire field
'verb'. workflow/errors.ts no longer defines a second RetryClass or the
none|possible|occurred axis.
HOMONYMS KILLED. The verifier engine class was also called Auths; it is
Verifier. Two structurally identical Receipt declarations became one, exported
once. The testkit's 'development' became 'fixtures' so it stops colliding with
the integrations 'development' that opens a real Auths.
CAPABILITIES REMOVED, both deliberate and both recorded in the tests that
covered them:
- Auths.recover and recoverMcpClosed (contract 4.2). A sixth operation with no
Rust owner and no registry entry, whose implementation re-ran authorization to
mint a throwaway decision receipt purely to re-derive an execution identifier.
- The identity DESCRIPTOR tier (contract 6.2/11.6, ruling 10A): a second
complete identity API with its own method and suite registries and no Python
counterpart.
TRUST REQUIREMENTS ENFORCED, NOT DOCUMENTED. test/unit/service-trust.test.js
drives the shipped client against every requirement
release/docs-bundle/runtime-facts.json declares. All ten pass; ST-5 is
mutation-proved -- claiming a non-effect the client cannot prove turns it red.
The public-API shape gate went 15 violations -> 0 and is now wired into
test:api, so it runs instead of merely existing.
Acceptance: all 11 effect-axis tests green. 16 integration failures remain and
are PRE-EXISTING, proved by a clean-baseline run at HEAD~2: they are the Rust
absent-budget denial convergence (f5c3589) reaching binding fixtures whose
grants carry a ceiling no action requests.
…(UNSIGNED) The previous commit claimed this and had not done it. src/workflow/errors.ts still declared its own RetryClass and its own effect axis spelled none|possible|occurred, so the SDK carried two types named RetryClass with different members and two words for 'the effect did not happen'. Both are now imported from product-errors.ts, which projects the Rust registry. 'none' was a second spelling of 'not-applied' -- same meaning, one word now -- and it is replaced at all four sites in the application profile and the two defaults in workflow/errors.ts. BEHAVIOUR CHANGE, recorded in test/unit/errors.test.js: ProviderOperationError for a non-timeout, non-cancelled failure reports effect 'not-applied' where it used to report 'none'. Same value, Rust's word. Verified: unit 32/32, package 10/10, contract green, effect-axis acceptance 11/11, public-API shape 0 violations, integration unchanged at the same 16 pre-existing absent-budget failures.
…t (UNSIGNED) bindings/typescript/src/production-client.ts is bindings/typescript/src/service.ts. The freeze gate was erroring on a missing file rather than reporting drift, which hid the drift it exists to report. This repoints the owner path only. Digests are NOT regenerated: version assignment happens at the end of the effort. The gate stays red by design.
…GNED)
UNSIGNED (auths-sign requires an interactive passphrase unavailable here).
Wave 2 verification found three different answers to "what does this code
mean?" shipping at once. All three agree on today's registry, because every
one of the 48 definitions declares exactly one outcome -- so no test could
see the disagreement, and a parity check over the registry is vacuous.
product/errors/auths-errors/src/lib.rs:308 the owner: DOMINANT outcome
(possible > applied > not-applied), and a fixed fail-closed answer for
an unrecognised code.
bindings/typescript/src/product-errors.ts:64 a faithful hand-copy of the
owner's rule. Driven against classifyErrorCodeV1 over all 48 codes plus
4 unknown codes: 0 disagreements. Left alone.
bindings/python/python/auths/_product_errors.py:488 outcomes[0] -- the
FIRST-DECLARED outcome.
bindings/python/src/errors.rs:93 a third rule: unanimity, else fail closed
to possible/unknown -- plus its own UNCLASSIFIED constant whose stage is
"unknown" where the owner's is "unrecognized-code".
Proven, not assumed. A scratchpad copy of the Python package with one
definition given two outcomes ordered [not-applied, possible] returned
not-applied/never where the owner returns possible/unknown: a
possibly-applied effect described to the caller as one that provably did not
happen.
- bindings/python/src/errors.rs: classify() now returns auths_errors::classify
verbatim. The local reduction, the local UNCLASSIFIED constant, and the
now-dead definition() helper are deleted.
- bindings/python/python/auths/_product_errors.py: the pure-Python projection
selects the dominant outcome. `max` keeps the first maximum, which is the
owner's tie behaviour.
Both repairs carry a check that bites:
- errors.rs the_boundary_reports_the_owner_classification_verbatim drives all
48 registry codes plus 4 unknown codes and compares every field. Mutating
stage back to "unknown" turns it red.
- test_vocabulary_parity.py test_classify_reports_the_dominant_outcome_the_way
_rust_does drives a synthetic two-outcome definition, and first asserts that
today's registry is all single-outcome so the synthetic case is still
needed. Reverting to outcomes[0] turns it red.
Separately, both lanes published a /service entry point that the SDK
vocabulary gate had never heard of, so it labelled all 49 of its symbols
"internal-leak: public mechanism without a final customer owner" -- in a
layer bindings/public-topology-v1.json declares by name.
- xtask/src/sdk_experience.rs: "./service" and "auths.service" own themselves.
- docs/product/sdk-glossary.json + xtask/src/sdk_vocabulary.rs: the "service"
owner and its concept.
- a new test asserts every layer the topology declares has an owner in both
languages, so publishing an entry point without one is a red test.
No fixture, protocol byte, registry code, or public binding symbol changed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
An absent `requested_budget` meant two different things and the kernel could
not tell them apart:
(i) the action's profile COULD have declared a budget and did not, so the
spend is unknown and a bounded ceiling cannot cover it; and
(ii) the profile's canonical body has no budget field at all, so the spend is
provably zero and every ceiling covers it.
`auths-verifier` applied (i) to everything. Composed with `auths.mcp/1`'s rule
that an MCP action may never declare a budget, every MCP grant chain with a
bounded terminal ceiling was unconditionally denied - and the same held for the
nine other shipping profiles that also cannot express a budget, including the
Stripe payout, connect-transfer, mandate, and subscription verticals.
PROTOCOL CHANGE (authorized under 10A). `AcceptedRegistries` gains
`budget_free_profiles`, encoded as key 13 of the verifier-context registries map
(now 14 entries). Every `.context.cbor` and `.result.cbor` golden vector is
regenerated. The list is empty by default, so an undeclared profile keeps the
denying reading: absence of a declaration never opens the gate.
- auths-model: `ProfileBudgetExpression` (default `Expressible`) and
`budget_ceiling_covers_action`, which is `optional_budget_covers` plus the
one fact the algebra cannot see. `optional_budget_covers` itself is
unchanged, so its Lean theorem and aeneas pin still hold.
- auths-profile-api: `ActionProfile::BUDGET_EXPRESSION`, no default, so every
profile must answer. All 22 implementations declare it; each value was read
off that profile's own canonicalizer, not assumed.
- Propagated to all four implementations: the Rust verifier, the Rust
authority kernel, the Go verifier, and the independent TypeScript verifier.
`cargo xtask cross-language` agrees at 104 fixtures.
New corpus fixture `action-budget-absent-budget-free-profile` is the authorizing
mirror of `action-budget-absent`: identical proof bytes, one differing context
declaration, opposite verdict.
Behavior changes named explicitly:
- `EffectiveAuthority::authorizes`, `evaluate_action_coverage`, and
`evaluate_action_coverage_view` take a `ProfileBudgetExpression`.
- The Go corpus digest pin moves from 103:6361... to 104:979e..., because the
corpus gained a fixture.
Verified: 16 TypeScript and 14 Python failures clear without deleting either
budget ceiling from the MCP node vectors.
The Wave 2 verify agent found the last two cross-language divergences. Every other operation and noun agreed; these did not: local factory TS createAuths (free fn) PY Auths.__init__ (constructor) service factory TS createServiceClient PY create_auths service client TS ServiceClient PY ServiceAuths The second row was the dangerous one: `create_auths` named the REMOTE client in Python while naming nothing in TypeScript, and Python's local factory was a constructor, so the same words meant different things in each language. TypeScript's spelling wins because it names the layer rather than the product, and Python conforms: local createAuths / create_auths service createServiceClient / create_service_client -> ServiceClient Superseded spellings are deleted outright, not aliased; prelaunch policy is direct cutover. TypeScript 147 tests pass across four suites; the public API shape gate stays at zero mirrored or homonymous exports. Python 133 tests pass. This lane was interrupted by ENOSPC mid-run and its Python half sat uncommitted; the work itself was complete and is verified above. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ted (UNSIGNED) semantic-freeze has been red since before this branch began: PR #109 changed auths.product.lifecycle under frozen identity v8 without assigning v9, and every wave since added more drift. It now passes. Computing the drift from owner paths rather than iterating the validator one error at a time found 26 of 63 identities drifted -- considerably more than the 6 the implementing agents self-reported, because each only knew its own lane. 20 frozen-meaning core.protocol 15->16, portable-abi-bindings 49->50, product.receipts 4->5, product.lifecycle 8->9, product.facade 9->10, public-sdk-contract 40->41, mcp-closed-execution 12->13, and 13 more 6 frozen-bytes dependency-graph 26->27, core fixtures manifest 3->4, identity-abi 3->4, assurance-manifest 3->4, errors manifest 3->4, bounded-policy manifest 1->2 FREEZE_VERSION 110 -> 111 assurance-manifest-v1.toml and qualification.toml shared one match arm; only the first drifted, so the arm is split rather than asserting a change to a file that did not change. Derived artifacts regenerated after review, not blindly: - architecture snapshot: 4 added edges, 0 removed. WASM and pyo3 now depend on auths-errors to carry the structured envelope, and WASM on js-sys to construct a real JS Error. bindings -> product is the correct direction. - sdk-experience baseline: TypeScript 193 -> 185 symbols across 7 -> 8 entry points (the dual-root collapse plus /service); Python 159 -> 168 across 7 -> 8 modules (the effect-axis vocabulary it previously could not name). - evolution lifecycle: the three codes auths-node's kernel rebuild registered (core.authorization-denied, core.authorization-indeterminate, core.unauthenticated-principal) gained active entries; registry is 48. - public-naming: two justified stale-name allowances for the audit document, which quotes public-naming.toml's own replace mappings. A third was REJECTED by the gate because auths-proof-algebra-contract/v1 is not a forbidden name -- an allowance without a violation is meaningless, and the gate said so. One genuine regression fixed, caught by the npm install smoke test rather than by any gate I was tracking: Wave 2 renamed ProductionProfile to ServiceProfile correctly but moved the factories with the type, so ./profiles lost githubIssueAddress, opentofuSavedPlanApply and postgresqlBoundedUpdate -- three of the four qualifiedProfiles -- while mcp, the fourth, stayed. A profile is a vertical, not a transport concept, and public-topology-v1.json maps the vertical layer to ./profiles. Restored by re-exporting the same declarations, so the shape gate still reports zero homonyms: one declaration, two paths, one meaning. Gates 17/17. Rust 776 tests, TypeScript 147, Python 133, all passing. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Source-SHA: 334e34c Workflow-Run: 31927345632
The aggregate 'cargo xtask ci authoritative' gate runs cargo fmt --all --check before anything else, so two unformatted files were masking the rest of the authoritative run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
1. cargo fmt --all --check — resolved upstream in c578427. 2. compliance / node-smoke: "exported but undeclared: productionTransportFailureV1" Wave 2 added the transport-failure classifier at bindings/wasm/auths-proof-wasm/src/lib.rs:156 — the function whose whole job is to stop a possibly-applied effect being reported as safe to retry — and wired it into bindings/typescript/src/service.ts:202,424 and verifier/wasm.ts:43, but never declared it in the ABI manifests. Declared in authoring-abi-v1.json; identity is the wrong home for a transport concern. 3. postgresql-live: "TLS PostgreSQL environment slots are required" Not an infrastructure problem, and not fixable with a fixture. The test was run from TWO workflows, correctly from one: - postgres-lifecycle.yml stands up the TLS fixture in tests/postgres_tls/compose.yaml and supplies all three slots (AUTHS_POSTGRES_URL, AUTHS_POSTGRES_CA_PEM, AUTHS_POSTGRES_SERVER_NAME). - ci.yml set AUTHS_LIFECYCLE_POSTGRES_URL, which configured() does not read, against the plain demo database on 54329 which has no TLS and no CA. It could never have satisfied the requirement, so it panicked on every run. Removed the ci.yml invocation. The duplication was the defect. On replacing it with a fixture: the test asserts multi-process capacity, restart replay, and transaction abort atomicity — properties only a real transactional engine exhibits. A fake would be a check that cannot fail in the way that matters. It already costs developers nothing: it is #[ignore]d, so it never runs in a normal `cargo test`, and its "real infra" is already a throwaway docker-compose fixture, not shared infrastructure. Freeze resynced for the ABI manifest and the formatting: portable-abi-bindings 50->51, evolution-contract 13->14, mcp-closed-execution 13->14, public-sdk-contract 41->42, release.public-surface 110->111, FREEZE_VERSION 111->112. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
… doc (UNSIGNED)
1. auths-node failed the Docker release build with
"`?` couldn't convert the error: `KeriError: std::error::Error` is not
satisfied" at main.rs:46, while `cargo check --workspace` passed.
FEATURE UNIFICATION MASKED IT. auths-did-key, auths-did-keri and
auths-registries all gate their Error impl:
#[cfg(feature = "std")]
impl std::error::Error for KeriError {}
and the workspace declares them `default-features = false` (Cargo.toml:150).
A whole-workspace build has some other crate turning on `.../std`, so the
impls exist and every local check passes. The Dockerfile runs
`cargo build --locked --release -p auths-node`, which resolves features for
ONE package with no unification, so std stays off and the impls vanish.
auths-node now requests `features = ["std"]` from all three rather than
relying on incidental unification. Only auths-did-keri had failed; the other
two were the same latent trap one build-order change away from firing.
Verified with the exact Docker command, not a workspace check:
cargo build --locked --release -p auths-node -> exit 0
2. docs/product/recipes/03_EXECUTE_ONE_ACTION.md was stale. The recipe source
bindings/recipes/python/03_execute_exact_action.py:6 was corrected to
`from auths.verify import verify_receipt` when the Python surface was
aligned, but bindings/recipes/tools/generate-docs.mjs was never re-run, so
the published recipe still told readers to import a symbol the root package
does not export. This is the broken recipe the adoption review reproduced.
Regenerated.
3. Freeze resynced: aeneas source-closure 12->13 (upstream c578427 regenerated
the qualification artifacts), product.vocabulary 8->9 (the recipe doc),
release.public-surface 111->112, FREEZE_VERSION 112->113.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The three-node reference job failed with:
Error: Process completed with exit code 35.
and nothing else. 35 is curl's CURLE_SSL_CONNECT_ERROR, so the TLS handshake
against the ingress on 8443 failed -- but the script reported no step name, no
container state, no ingress log, and no handshake detail. A reader cannot act
on that, and neither could I: with the stack unavailable locally there was no
way to tell a dead upstream from a bad certificate from an nginx that never
loaded its key.
This is the same shape as the rest of this branch: a check that runs, correctly
fails, and then declines to say why.
The script now names the step it was on and, on any failure, reports:
- the CA and ingress certificate subjects and validity windows
- whether the CA actually signs the ingress certificate
- `docker compose ps`
- the last 40 lines of the ingress log
- a verbose curl handshake
Behaviour on success is unchanged. Verified by running it with no stack up:
it correctly identifies `docker compose config` as the failing step and prints
the certificate chain state.
This does not fix the handshake. It makes the next run diagnosable rather than
a number, which is the honest next step -- the previous push was the first in
which auths-node compiled at all, so this job had never reached the smoke test
before and there is no prior evidence about why it fails.
Separately confirmed NOT causes: the certificate material is gitignored and
regenerated by the workflow before the stack starts, the generator writes to
the directories compose mounts, and nginx's SANs cover localhost and 127.0.0.1.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…NSIGNED) 697bd99 added `features = ["std"]` to auths-did-key, auths-did-keri and auths-registries so auths-node builds as a single package, but only the freeze was resynced -- not the dependency snapshot. The drift is exactly those three edges and nothing else: same source, same target, same layer, same kind, `features: []` -> `features: ["std"]`. Three added, three removed, no new dependency and no layer change. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…SIGNED) Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…IGNED)
The PR asserted one thing that was not true. `source-closure.json` attested
"this Lean was produced from this source" while the generated model still
answered `ok true` for a bounded ceiling with an absent request -- the vacuous
budget bug this branch fixed in Rust. The translation could not be regenerated,
so the gap was carried as hypotheses instead. It is regenerated now.
optional_budget_covers (some ceiling) none: ok true -> ok false
WHY IT COULD NOT REGENERATE. `formal qualify aeneas` ran `lake build` before it
reached `reproduce()`. Qualification REGENERATES the Lean a build compiles, so
the moment a translation referenced a symbol its upstream crate had not exported
yet, the build failed on the generated file, qualification aborted before
translating, and the upstream crate could never produce the symbol. Split into
`prepare_formal_translation` (no Lean) and `build_and_audit_formal`; ordinary
`cargo xtask formal` keeps build-first, only `qualify aeneas` inverts. The
compiled gate still decides success -- it runs after synchronization, before
evidence is written. Two tests lock the ordering structurally and were
mutation-proven: restoring `prepare_formal(` fails them.
THREE AENEAS BLOCKERS, one rule. Aeneas cannot translate a branching expression
in struct-field position. Ten of the twelve dimension fields were function
calls and all translated; the only two written inline were the only two that
failed. `depth_decreases` (`&&`) and `extensions_attenuate` (`match`) are now
named functions like their siblings. That `extensions_attenuate` was one of them
is not a coincidence: it is the eleventh dimension, the one that was vacuously
`:= true`, the newest, and the only one written unlike its neighbours.
`aeneas_version_matches` compared a hard 7-character truncation, so an Aeneas
built from exactly the pinned commit was rejected when git abbreviated to 8. It
tested formatting, not identity. Any genuine prefix >= 7 chars now passes.
DEPENDENCY CLOSURE, no axioms. `budget_ceiling_covers_action` and
`ProfileBudgetExpression` are translated in `auths_model`; `root_preserved` and
`RootLinkage` in `auths_algebra_kernel`. Generic `root_preserved<Identity:
PartialEq>` translates faithfully, trait bound intact. The authority bridge
reboxes its local carriers field by field and delegates -- 17 rfl proofs, four
linkage fields and eleven attenuation fields generated from the contract, so a
twelfth dimension regenerates the bridge rather than being dropped. It restates
no Boolean semantics. `required_compiled_external_axioms` stays 0.
The hand-rendered `attenuation_checks_accept` is deleted: it re-rendered the
contract in Lean beside the Rust the same contract generates, and two renderings
can disagree. The imported translation cannot -- it IS the shipped Rust.
BOTH CONDITIONAL PREMISES REMOVED, not renamed.
TranslatedBudgetCoverageCurrent excluded the one input class where the
translation was stale. The translation is current; the class is covered.
AuthorityStateAnchored assumed a root the translated state could not
express. `AuthorityStateView` now carries `root`, so `richAuthorityState`
reads it and rooting is structural. `root_preserved_rich_spec` proves the
translated dimension is exactly `rooted AND actor = subject`.
Both production refinement theorems are now unconditional over valid
representations.
`translated_budget_coverage_gap_is_the_absent_request` recorded the staleness as
checked evidence and stopped compiling on regeneration, exactly as its comment
promised. Replaced by four positive regressions. Profile expressibility is
modelled explicitly as trusted registry context an action cannot assert about
itself, with the complete truth table proved.
A qualification vector asserted that a bounded ceiling COVERS an undeclared
request -- the bug, written down as a passing test. Corrected, plus vectors for
both expressibility modes. Two declared-request vectors were removed rather than
closed with `native_decide`: comparing ceilings reaches opaque `as_bytes`, and
buying two vectors with a new axiom is the trade this branch exists to refuse.
`budgetCoversAction_declared` covers that case abstractly.
Verified: lake build 3286 jobs; assurance audit 124 compiled statements;
qualification cases 6/6; clean reproduction byte-identical; decision
GO-AENEAS-WITH-PRODUCTION-RESHAPE; no axiom, sorry, or admit in any compiled
artifact.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Source-SHA: 3d8338f Workflow-Run: 31956571432
…NED)
Reviewer item 4. `formal/refinement-mutations-v1.json` listed 23 ways an
attenuation dimension could be weakened, each with an `operator` describing the
mutation and a `witness` SENTENCE asserting it would be caught. The assurance
audit checked that the file EXISTED and read nothing inside it.
That is a claim recorded rather than enforced, sitting inside the evidence for
the claims -- the exact defect this branch exists to remove. The criticism lands
on my own work: I reported Kani mutation kills in commit messages, which is a
report, not a proof.
Auths/Rich/Mutations.lean adds 13 compiled counterexamples. Each exhibits a
concrete input on which the shipping semantics DENY and the described mutation
would accept, over a concrete Nat vocabulary, closing by `decide` -- so they are
computations rather than appeals to a tactic that could be silently weakened. A
harmless mutation would have no such witness and the theorem would not compile.
`optional_budget_no_request` is the vacuous-budget bug itself, now a theorem:
a bounded ceiling does NOT cover an undeclared request.
`validate_mutation_witnesses` in xtask requires every case naming a
`lean_declaration` to name one the assurance audit actually compiled. Deleting a
witness, renaming it, or pointing a case at nothing fails the build.
MUTATION-PROVEN, since asserting this one would repeat the error it fixes.
Pointing a case at `Auths.Rich.Mutations.this_theorem_does_not_exist` produced:
xtask: mutation case validity-start-direction names witness
Auths.Rich.Mutations.this_theorem_does_not_exist, which the
assurance audit did not compile
The check also rejected my own witnesses until they were added to the theorem
inventory, which is the useful signal: a theorem sitting in a file is not
evidence until it is part of the audited set.
10 OF 23 CASES REMAIN PROSE and are left visibly unbound. The set-valued
dimensions -- permissions, audiences, body digests, action constraints -- need
FiniteSet construction I have not written. Binding all 23 by asserting the rest
would be the same error at one remove.
Verified: lake build; assurance audit PASS at 137 compiled statements, up from
124; qualification cases 6/6; clean reproduction byte-identical; no axiom,
sorry, or admit.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…iant (UNSIGNED) Reviewer item 3, the half that was genuinely missing. `CriticalExtension::new` rejects a payload longer than `HARD_MAX_EXTENSION_BYTES` (auths-model/src/lib.rs:1080). Lean recorded distinctness and the 32-entry cap but not the byte bound, so a Lean inhabitant could exceed it. The claim that this type is exactly the Rust-constructible image was therefore too strong: the type admitted values Rust refuses. `Vocabulary` gains `extensionBodySize`, a measure the opaque carrier could not otherwise state; production supplies `List.length`. `CriticalExtensions` gains `bodiesBounded`, and `CriticalExtensionsCanonical` -- the predicate the production refinement quantifies over -- gains the same obligation. That second one is the substantive fix: the refinement theorems were universally quantified over a class strictly larger than the Rust constructor's image. The invariant paid for itself immediately. `CriticalExtensions.singleton` no longer compiles without a proof its payload is in bounds, and that obligation propagated to `empty_ne_singleton` and `extensions_le_refuses_a_dropped_singleton`. Before this, one could construct in Lean an extension set Rust would have rejected and prove theorems about it. SORTEDNESS IS DELIBERATELY NOT ADDED, and the reasoning is worth stating rather than leaving as a silent omission. Rust sorts during construction. An unsorted Lean value denotes the same map from identifier to payload, and `critical_extensions_equal` compares canonical vectors positionally either way, so no decision below depends on the order. Closing that last gap needs a total order on `ExtensionIdCarrier` threaded through every vocabulary; it would make the correspondence exact but changes no theorem. The byte bound was the half that actually admitted values Rust refuses, and that is the half fixed here. Verified: lake build; assurance audit PASS at 137 compiled statements; qualification cases 6/6; clean reproduction byte-identical. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…(UNSIGNED)
Reviewer item 2. `grantScopeChecks` was a nine-way anonymous conjunction, and
reaching a dimension meant counting:
((rich_projection_accepts_iff_root_and_scope_depth_checks
parent grant).1 accepted).2.2.2.2.2.2.2.2.2.2.2
Eleven projections whose meaning depended on position. That expression broke the
moment the structure landed, which is the evidence the refactor does what it is
for; it now reads `.2.2.2).extensions`.
`GrantScopeChecks` gives each dimension a name: profile, permissions, validity,
audiences, actionConstraint, budget, status, assurance, extensions.
`GrantScopeChecks.iff_conjunction` keeps the conjunctive spelling available for
rewriting, so existing tactic proofs are unchanged except where they addressed a
dimension by counting.
The property that matters is structural, not stylistic: adding a tenth scope
dimension now forces every constructor and every pattern match to mention it.
The eleventh attenuation dimension was once reported as
`extensionsAttenuate := true` and nobody noticed, because nothing in the shape
of a nested conjunction required it to be addressed. A structure requires it.
This is also the prerequisite for item 1: a certified projection needs a named
per-dimension carrier to attach exactness fields to.
Verified: lake build; assurance audit PASS at 137 compiled statements;
qualification cases 6/6; clean reproduction byte-identical.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…SIGNED)
Reviewer item 1, the change they called highest-value.
`Auths.Generated.AttenuationProjection` is eleven unconstrained `Bool`s, so
`extensionsAttenuate := true` remained EXPRESSIBLE. That is not hypothetical:
the eleventh dimension shipped as exactly that literal, and the exactness
theorems are what eventually caught it. They catch a bad projection after it
exists.
`CertifiedProjection parent grant` makes it unconstructible. Eleven obligations
pin each field to the `decide` of its rich relation, so a literal cannot be
supplied without a proof that the literal equals the semantic answer -- and for
a wrong literal no such proof exists.
PROVEN BY CONSTRUCTION, not asserted. A forged projection carrying
`extensionsAttenuate := true` was written and rejected:
error: Type mismatch
rfl has type ?m = ?m
but is expected to have type
{ ... extensionsAttenuate := true ... } = decide (extensionsLe ...)
`certifiedDelegationProjection` discharges all eleven obligations by `rfl`, and
that is itself the finding: `delegationProjection` was already honest and simply
had no way to say so in its type. The vacuous literal that shipped could not
have been written in this form.
Two theorems record the consequence: a certified projection cannot report
extensions or the trust root as attenuating when the semantics deny them.
Adding a twelfth dimension adds a twelfth obligation no existing constructor
satisfies, so the compiler demands it be addressed. Together with the named
`GrantScopeChecks` from the previous commit, another hidden `:= true` now has
to survive both a structure that requires the field and a type that requires a
proof of its value.
Verified: lake build; assurance audit PASS at 139 compiled statements, up from
137; qualification cases 6/6; clean reproduction byte-identical.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Reviewer item 5. Evidence was EXISTENCE-CHECKED only: the audit confirmed a file
was present at the cited path and read nothing. An artifact could be emptied,
rewritten, or replaced wholesale and every claim citing it still passed.
That is not hypothetical. `refinement-mutations-v1.json` was exactly this case --
23 prose entries standing in for checks, cited as evidence by three claims,
never read. The previous commit made its contents enforceable; this makes the
citation itself binding.
`FormalEvidence` gains `sha256`, verified whenever present. 155 evidence entries
across 11 distinct artifacts now carry one.
MUTATION-PROVEN. Corrupting a recorded digest reports the claim, the artifact,
and both hashes:
xtask: formal claim Auths.Rich.finiteSet_subset_refl cites evidence
formal/Auths/Rich/Theorems.lean with digest 0000...0000, but the
artifact hashes to 7dcf0fbc0904c1cc...
The check also fired on real input before any probe: `source-closure.json` is
regenerated by the same command that validates it, so its recorded digest went
stale mid-run and the audit refused. That is the binding behaving correctly --
regenerating an artifact now requires refreshing what cites it, which is the
point of citing a digest rather than a path.
The field is optional so an entry can be introduced before its digest is
recorded, but once present it is enforced.
Verified: lake build; assurance audit PASS at 139 compiled statements;
qualification cases 6/6; clean reproduction byte-identical; cargo xtask formal
passes with Kani, Lean theorems, and Rust refinement vectors all green.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…resh (UNSIGNED) Reviewer item 7, answered with evidence rather than churn, plus a real defect in what the previous commit shipped. THE SORRYS STAY, AND HERE IS WHY. The ask was to patch or locally prove the four `sorry`s in the vendored Aeneas runtime for a pristine artifact. Doing so means editing a dependency pinned by commit in translation-toolchain.lock: it breaks the pin, or requires re-pinning to a fork, and changes nothing about what is proved. Measured, not assumed -- all 139 audited declarations reduce to exactly three axioms: Classical.choice, Quot.sound, propext sorryAx: 0 So no audited theorem depends on any of them. The inventory already verified each RECORDED line still holds a `sorry`; what nothing checked was whether there were OTHERS. A new upstream `sorry` arriving with a toolchain bump would have been accepted silently while the inventory still read as a complete account. `validate_warning_inventory` now reports any unaccounted line by number. Trying to mutation-test that revealed the layering is already deeper than expected: injecting a `sorry` into vendored Aeneas was refused twice before reaching the new check -- first by the source-closure digest, then by the evidence digest added in 422d4ce. Three independent layers now catch it. A DEFECT IN 422d4ce, fixed here. The evidence digest binding was correct but unmaintainable: `source-closure.json` is regenerated by the same command that validates its digest, so every regeneration left a stale digest and a standing false alarm. It fired twice in normal operation before I noticed. `--update` now refreshes evidence digests before writing the manifest; the non-update path still verifies and refuses a mismatch. Update recomputes, check enforces, which is how the rest of the qualification already works. Verified: lake build; assurance audit PASS at 139 compiled statements; qualification cases 6/6; clean reproduction byte-identical. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The installed-client e2e calls `auths-sandbox-request`, which d82d57f deleted, and asserts `issuer.create(...)` returns an authority. The node refuses that permanently: kernel.rs returns UnauthenticatedPrincipal for both `create` and `delegate`, because ProductionRequest.identity is unauthenticated bytes and there is no client authentication at that call site to require instead. The old test asserted the fail-open this branch removed. Authority in V1 originates from a trust anchor's signature and arrives INSIDE the proof, so `auths-local-authority` authors one: it derives the same anchor `auths-local-context` put into the trusted context, signs a root grant to a per-label agent principal, signs the action that agent will present, assembles a canonical proof bundle, and prints the proof and action for the client to hand to `execute` -- the only verb the node answers. The grant terms and the trusted context come from ONE source, `reference_grant_terms`. Had they drifted, the node would deny every authored proof and the failure would read as a verifier bug rather than a fixture mismatch. Two things the model enforced while building this, worth recording because both are the protocol refusing to be shortcut: * a proof bundle with no signed action is rejected (`actions.is_empty()`), so a grant alone is not a proof of anything; * the trust anchor cannot sign the action -- the agent must -- which is the delegation the demo exists to show. LOCAL FIXTURE. The anchor key derives from AUTHS_LOCAL_SEED, so anyone with the seed can author against this stack. That is the point of a self-contained demo and disqualifying anywhere else. Verified: emits a proof and action for auths.opentofu.saved-plan-apply/1 from the CI seed. The e2e rewrites that consume it are the next step, and still need a way for the SDK to carry a caller-held proof: `serviceAuthority` is module-private, so today only create and delegate can produce a ServiceAuthority and both always fail. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The reference-stack e2e could not be rewritten without this, and the reason is worth stating plainly: a proof-carrying SDK had no way to carry a proof INWARD. `ServiceAuthority` is deliberately opaque -- bytes in a WeakMap, `toJSON()` returns never -- and `serviceAuthority()` was module-private. The only producers were `create` and `delegate`. A node that refuses to mint answers both with `core.unauthenticated-principal`, so on the reference stack NOTHING could produce a `ServiceAuthority`. A caller holding a valid, anchor-signed proof had no way to hand it over. That was coherent under the old model, where the service was the sole source of authority. Under the model this branch established -- authority originates from a trust anchor's signature and arrives inside the proof -- its absence is a leftover. `importAuthority` (TypeScript) and `import_authority` (Python) take canonical proof bytes and return the same opaque carrier the service would have. A way in and no way out: the bytes are copied, the value stays sealed, and neither language gained a reader. Both e2e tests are rewritten against it. They no longer call the deleted `auths-sandbox-request`, and no longer assert `create` returns an authority -- that assertion was the fail-open the kernel rebuild removed. They now author offline with `auths-local-authority`, import, and call `execute`, which is the only verb the node answers. Each also asserts the replay refusal, since the claim is keyed on (proof digest, action digest) and allows one effect. Surfaces updated from actual state: TypeScript 190 -> 191 symbols, the Python API snapshot regenerated, `auths-author` declared as a core API of auths-node, architecture snapshot and semantic freeze resynced. The TypeScript shape gate still reports zero mirrored or homonymous exports. Verified: TypeScript 147 tests, Python 133 tests, compliance PASS across 68 packages and 137 claims, sdk-experience, public-naming, arch, binding-semantics, sdk-vocabulary and cross-language all green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The rewritten e2e dropped `identity` from `createServiceClient`, which is
required, so both clients threw before reaching the node:
TypeError: Auths identity bytes are outside production bounds
at new ServiceClientValue
Each client now carries the agent label it authored under, so the identity the
transport sends matches the principal the proof delegates to.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The rewritten e2e reached the node and was DENIED. Three real defects behind that, each found by running the verifier rather than by reading code. 1. NO EVIDENCE, NO BINDINGS. The bundle carried a signed grant and nothing linking it to the key that signed it. Added raw-key evidence for the anchor and the agent, and control bindings tying the grant and the action to them. 2. THE NODE DECODES A CANONICAL ACTION, not the raw body. The tool emitted the file's bytes, so `decode_canonical_action` answered Malformed before any authorization decision was reached. 3. `Denied(BudgetCeilingExceeded)` -- and this one is this branch's own fix working. The grant carried a bounded ceiling while the action declared no budget, which is precisely the case changed from vacuously-covered to denied: an action that states no bound on what it may spend is the authority a ceiling exists to refuse. The demo now declares what it intends to spend. The third is worth keeping in mind. The fix denied my own proof, correctly, and the only way to discover that was to run it. `tests/local_fixture_authorizes.rs` closes the loop permanently: it authors a proof for each of the three reference profiles and requires the real verifier to return Authorized against the generated context. The context and the authoring tool are derived from one seed through `reference_grant_terms`, but that is a claim about the code, not a check on the result -- and every way the two can drift produces the same symptom, a node denying everything, which reads as a verifier bug rather than a fixture mismatch. Verified: VERIFY: Authorized for opentofu, postgresql and github; the test passes for all three. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…NED) `Denied(DelegationExpanded)` on every profile, and the validity dimension was right to refuse. The trusted context fixes the anchor's window when it is GENERATED, at stack start. The authoring tool runs later and was asking for `now + 3600` from its own clock, so the grant ended after the anchor it descends from. A child that outlives its parent expands the authority it was given, which is exactly what that dimension exists to catch. The grant now spans fifteen minutes, comfortably inside any lifetime the fixture generates. This also corrects something I reported an hour ago. I said the authored proof verified for all three profiles; it had been checked against a stale binary built before the canonical-action change. The test caught it the moment CI rebuilt, which is the argument for `local_fixture_authorizes.rs` existing rather than my having run the tool once by hand and believed the output. Both e2e tests now report the denial code on refusal instead of a bare `expected completed, got denied`, so a failure names the dimension instead of costing a CI round trip to diagnose. Verified: all three reference profiles return Authorized; auths-node's 25 tests pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The client reports `denied (core.authorization-denied)` and the node's own reasoning is not captured, so each diagnosis costs a five-minute round trip and ends in speculation. Receipt disclosure deliberately returns one failure for both unknown and unauthorized, so the client cannot be more specific -- but the node logs can. Captured on client failure only, so a passing run stays quiet. Locally the authored proof verifies against the generated context file through the node's own `for_request` path -- all three profiles Authorized -- so the remaining difference is inside the running node, not in the proof. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…(UNSIGNED) Reviewed work from a second agent, verified locally, and closed the two gaps it left. The verification matters more than the reading: 83 xtask tests, lake build over 3287 jobs, assurance audit at 158 compiled statements, qualification 6/6, reproduction byte-identical. WHAT THE REVIEW CORRECTLY CAUGHT IN MY EARLIER WORK. `validate_mutation_witnesses` accepted ANY compiled theorem as a witness and returned success for unreadable files, invalid JSON, and missing fields. It now deserializes a strict `MutationMatrix` with `deny_unknown_fields`, requires exactly 23 ordered unique ids, and derives the expected declaration from the case id rather than checking that something exists. Negative tests cover malformed JSON, wrong count, reordering, redirection, and a missing field. Several of my witnesses proved only `1 ≠ 0`. Those survive mutating the corresponding predicate to `True` -- they were decoration. All 23 now run through `evaluateGrant`, `evaluateAuthorScope` or `evaluateCoverage`, and all 23 are bound rather than the 13 I managed. `FormalEvidence.sha256` was optional, so deleting a digest disabled the check it was meant to enforce. Now required, 64 lowercase hex, with `is_file()` and symlink rejection instead of `exists()`. I declined sortedness on critical extensions, arguing no decision depended on ordering. Positional equality does. It is now recorded as `entries.Pairwise criticalExtensionLt`. `delegationProjection` returns `CertifiedProjection` rather than certification sitting beside it unused, which closes the real gap: my audited theorems were generic properties of the type, not a required connection to the projection the code actually builds. THE TWO GAPS I CLOSED. `profile_version_equality` proved its point through a different dimension. It is now stated against the TRANSLATED `profile_ref_equal`, which compares `version` before `id`, so a version-only difference decides without reaching the opaque `as_bytes` and closes by `rfl` -- no `native_decide`, no new axiom. `ReachableFromRoot` is the inductive ancestry predicate the review asked for: a state has it only by construction, as an origin or as an accepted extension of a reachable state. `rooted_of_reachable` proves the implication ONE WAY ONLY and says so. Every genuinely rooted chain passes `rooted`, so the kernel never rejects a real chain; a state carrying a present marker can pass without being reachable. That gap is closed by sealing the raw views, not by the predicate. Stating the direction that holds is more useful than implying `rooted` was fixed. It was not; it is an approximation, and the development now says so with a proof attached. ONE GATE WORTH NAMING. `statement_inventory_sha256` binds the manifest to the exact set of compiled statements, so adding even a true theorem halts qualification until the inventory is reviewed and the digest updated deliberately. It fired on my own three additions and made me check all 158 declarations and their axioms first: still exactly Classical.choice, Quot.sound and propext, still no sorryAx. My earlier work had no equivalent -- a theorem could appear and nothing would notice. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Source-SHA: 7d584b3 Workflow-Run: 31970247848
Break the semantic-freeze/formal-closure digest cycle and enforce the freeze in pre-commit. Make the installed reference validity tolerant of second-boundary clock skew, and make Windows checkpoint replacement retry transient destination locks without deleting durable state.
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.
Closes the safety gap between what Auths claims and what it checks. 25 commits, one story: every central claim is now enforced by something that can fail.
semantic-freezewas red onmainbefore this branch began. It passes now, along with 16 other gates.Fail-opens closed
PeerObservationwas a public enum with public variantsauths-nodemints root authoritiesparent: Nonefrom an unauthenticated self-asserted identity. Deleted withsandbox.rs.optional_budget_covers(Some(bounded), None) → true. The system only denied because a guard ran at line 2227 before the algebra at 2251 — correctness rested on statement order.The reference production runtime was a second authorization system
product/runtime/auths-nodeis whatdemos/open-production-reference/Dockerfilebuilds and runs. ItsCargo.tomldepended on no kernel crate. It hand-rolled narrowing over 4 dimensions where the kernel checks 11, and 8 of its 10 wire error codes were unregistered.A differential test against
auths-verifierover the canonical corpus, first run:Sharper than "checks 4 of 11" — it could not parse the protocol it claimed to enforce. Rebuilt on the kernel; the differential test is now its acceptance criterion, asserting exact
DenialReasonandRequirement.Two proofs that could not fail
root_preserved: truewas a literal.AuthorityStateViewcarried no root to compare against, so the Kani harness proved an identity over arbitrary booleans while presenting it as a security invariant. A red test showedevaluate_grant_viewaccepted a delegation descending from no root.extensionsAttenuate := truewas the same shape one level deeper:Rich.Granthad no extensions field, so the model could not express dimension 11. The eleven-dimension contract was proved over ten and reported eleven.Both are now computed, with theorems in Lean and Kani harnesses that were mutation-tested — reverted to the literal, confirmed red, restored.
31 proof harnesses no gate executed
xtask/src/formal.rsran Kani on 2 of 5 packages. Baseline: 31/31 passed. Four could not fail at all, proven by mutation using each harness as its own control:Rewritten to quantify over real domains and call production code rather than transcribe its arithmetic. A new
kani_harness_inventorycheck fails when any#[kani::proof]appears outside a gated root, so the class cannot silently return. Nine fixtures cited a harness symbol that does not exist; corrected through the generator.The signed receipt can now say "unknown"
ExecutionOutcome { Succeeded, Failed }— two variants. For a provider timeout the runtime signed a durable receipt asserting Failed for an effect that may have applied. GainedIndeterminate, mapping toEffectState::Possible. Protocol change, fixtures regenerated with per-fixture justification.Four implementations, one answer
EffectStatehad five incompatible value sets across three languages.RetryClassnamed three different closed sets, and both bindings exported two of them under one identifier.recoverwas a sixth product operation both bindings invented independently, with no Rust owner.The absent-budget case disagreed four ways — Rust verifier, Rust kernel, Go, independent TypeScript — invisible because all 102 canonical fixtures declared a
requested_budget. Adding one fixture madecargo xtask cross-languagefail; all four now agree, permanently.The bindings project rather than define
The TypeScript root shipped two complete unrelated SDKs: 19 of 41 root symbols were a
Production*mirror of the other 14, sharing zero methods, drawingcodefrom disjoint spaces.createAuthsdispatched local-vs-remote by sniffing for anendpointproperty.js_errorflattened every failure to a bare JS string at 262 call sites, destroying code identity, effect state and recommended action for all 48 registry codes. A panic underpanic = "abort"was proven to SIGABRT the interpreter (exit 134).Acceptance test written first, red: 8 of 11 TypeScript cases, 9 of 12 Python. Now 11/11 and 12/12 — the effect axis reaches a real caller in both languages, and an unrecognized code fails closed to
possible.New gates, so none of this returns
--shapeon the TypeScript public API: detects mirrored (X/PrefixX) and homonymous exports. Found 15, including six the audit missed. Now zero. A stale allowance fails as loudly as a violation.kani_harness_inventory: a harness outside a gated root fails the build.ProfileBudgetExpression: budget capability is a declared profile property, and an undeclared profile defaults to the denying reading.Verification
26 of 63 frozen identities drifted — four times what the implementing agents self-reported, since each knew only its own lane. Computed from owner paths, versions assigned individually,
FREEZE_VERSION110 → 111.Known red, deliberately
cargo xtask formalreports the translation source closure as drifted. Clearing it requires re-running charon and aeneas at the commits pinned informal/translation-toolchain.lock; neither is installed on the authoring host. That pin asserts "this Lean was produced from this source," so writing the digest without translating would fabricate exactly the class of claim this branch removes. It needs to go green in CI.The stale translation is recorded as a checked theorem —
translated_budget_coverage_gap_is_the_absent_request— naming precisely which input class the translated model and current Rust disagree on.Reviewer notes
auths-signrequires an interactive passphrase unavailable on the authoring host. Re-sign before merge.auths-deploymentdeleted — zero source consumers, recoverable frombbeb654.🤖 Generated with Claude Code