diff --git a/apps/approve-ios/Approve/AppState.swift b/apps/approve-ios/Approve/AppState.swift index 31ee54dfbaa..6d429909144 100644 --- a/apps/approve-ios/Approve/AppState.swift +++ b/apps/approve-ios/Approve/AppState.swift @@ -91,11 +91,12 @@ final class AppState: ObservableObject { let attempt = PushAttempt(enrollmentId: e.enrollment_id, attestKeyId: e.attest_key_id, token: desired) do { let client = try requireClient() - let body = WireEncode.pushUpdate(registration(client.config, desired)) + let push = registration(client.config, desired) + let body = WireEncode.pushUpdate(push) let requestedAt = Self.now() let auth = try await assertion(e, requestedAt: requestedAt, clientData: devicePushUpdateClientData(enrollmentId: e.enrollment_id, requestedAt: requestedAt, pushBodyJson: body)) - try await client.updatePush(bodyJson: body, auth) + try await client.updatePush(push, auth) // Record success only if the token is STILL desired and the enrolment the update // was made for is STILL the current one; otherwise loop and re-derive. guard apnsToken == desired, case .enrolled(var now) = state, now.enrollment_id == e.enrollment_id, diff --git a/apps/approve-ios/Approve/Wire.swift b/apps/approve-ios/Approve/Wire.swift index a15629297eb..c3bff6c7f76 100644 --- a/apps/approve-ios/Approve/Wire.swift +++ b/apps/approve-ios/Approve/Wire.swift @@ -181,6 +181,16 @@ enum WireEncode { } /// push_update_json static func pushUpdate(_ p: ApnsRegistration) -> String { push(p).serialized } + /// read_authentication_json_value + static func readAuthentication(_ a: ReadAuth) -> WireJson { + .object([("enrollment_id", .string(a.enrollmentId)), ("requested_at", .string(a.requestedAt)), ("assertion_b64", .string(a.assertionB64))]) + } + /// read_authentication_json: the body of the three authenticated reads + static func readRequest(_ a: ReadAuth) -> String { readAuthentication(a).serialized } + /// push_update_request_json: { auth, push } + static func pushUpdateRequest(_ a: ReadAuth, _ p: ApnsRegistration) -> String { + WireJson.object([("auth", readAuthentication(a)), ("push", push(p))]).serialized + } } enum WireDecode { @@ -393,14 +403,12 @@ enum OutcomeName { ] } -// ── Headers, paths ─────────────────────────────────────────────────────────────────────────── -enum ReadHeader { - static let enrollment = "X-Approval-Enrollment" - static let requestedAt = "X-Approval-Requested-At" - static let assertion = "X-Approval-Assertion" -} - -/// The credentials an authenticated GET or PUT carries; produced by the caller so this file signs nothing. +// ── Paths ──────────────────────────────────────────────────────────────────────────────────── +/// EVERY DEVICE OPERATION IS A POST WHOSE BODY CARRIES ITS AUTHENTICATION (gunbc.auth.approval_device_wire +/// ReadAuthentication): the server hands a route no request header but the tailnet login, so the +/// enrolment id, the claimed time and the assertion travel in the JSON body. The assertion's client +/// data (device_read_client_data) is unchanged by where the carrier rides. +/// The credentials an authenticated read or push update carries; produced by the caller so this file signs nothing. struct ReadAuth { var enrollmentId: String var requestedAt: String @@ -476,14 +484,9 @@ struct Client { let config: ServerConfig let session = URLSession(configuration: .ephemeral) - private func send(_ method: String, _ path: String, body: String? = nil, read: ReadAuth? = nil) async throws -> Data { + private func send(_ method: String, _ path: String, body: String? = nil) async throws -> Data { var req = URLRequest(url: try config.url(path)) req.httpMethod = method - if let read { - req.setValue(read.enrollmentId, forHTTPHeaderField: ReadHeader.enrollment) - req.setValue(read.requestedAt, forHTTPHeaderField: ReadHeader.requestedAt) - req.setValue(read.assertionB64, forHTTPHeaderField: ReadHeader.assertion) - } if let body { req.httpBody = Data(body.utf8) req.setValue("application/json", forHTTPHeaderField: "Content-Type") @@ -501,21 +504,24 @@ struct Client { func enrol(_ r: EnrolmentRequest) async throws -> EnrolmentGrant { try WireDecode.enrolmentGrant(await send("POST", Route.enrol, body: WireEncode.enrolmentRequest(r))) } + /// POST /approve/device/pending, body = read_authentication_json func pending(_ read: ReadAuth) async throws -> [PendingApproval] { - try WireDecode.pendingList(await send("GET", Route.pending, read: read)) + try WireDecode.pendingList(await send("POST", Route.pending, body: WireEncode.readRequest(read))) } + /// POST /approve/device/requests/, body = read_authentication_json func fetch(_ path: String, _ read: ReadAuth) async throws -> FetchedRequest { - try WireDecode.fetchedRequest(await send("GET", path, read: read)) + try WireDecode.fetchedRequest(await send("POST", path, body: WireEncode.readRequest(read))) } func redeem(_ r: SignedRedemption) async throws -> RedemptionOutcome { try WireDecode.redemptionResponse(await send("POST", Route.redeem, body: WireEncode.signedRedemption(r))) } - /// GET /approve/device/enrollments/, read-assertion authenticated. + /// POST /approve/device/enrollments/, body = read_authentication_json. func readback(_ path: String, _ read: ReadAuth) async throws -> EnrolmentReadback { - try WireDecode.enrolmentReadback(await send("GET", path, read: read)) + try WireDecode.enrolmentReadback(await send("POST", path, body: WireEncode.readRequest(read))) } - /// PUT /approve/device/push; the body is the exact JSON the assertion's client data framed. - func updatePush(bodyJson: String, _ read: ReadAuth) async throws { - _ = try await send("PUT", Route.push, body: bodyJson, read: read) + /// POST /approve/device/push, body = push_update_request_json { auth, push }; the assertion's + /// client data frames push_update_json(push) alone, exactly as the server re-renders it. + func updatePush(_ push: ApnsRegistration, _ read: ReadAuth) async throws { + _ = try await send("POST", Route.push, body: WireEncode.pushUpdateRequest(read, push)) } } diff --git a/apps/approve-ios/ApproveTests/ProtocolVectorTests.swift b/apps/approve-ios/ApproveTests/ProtocolVectorTests.swift index 25d9e745077..fb5503c942c 100644 --- a/apps/approve-ios/ApproveTests/ProtocolVectorTests.swift +++ b/apps/approve-ios/ApproveTests/ProtocolVectorTests.swift @@ -73,7 +73,7 @@ struct Vectors: Decodable { var envelope: [Envelope] /// path_segment: input -> encoded, emitted by the .dag path_segment fold. var path_segment: [PathSegment] - /// surface: the header names and route paths, by name. + /// surface: the one method, and the route paths, by name. var surface: [Surface] /// stored_request: the store's own rendering, so the detail screen's reader is joined to it. /// Optional in the Codable so that a fixture predating the section (it is emitted by @@ -178,6 +178,18 @@ final class ProtocolVectorTests: XCTestCase { XCTAssertEqual(WireEncode.pushUpdate(try WireDecode.pushUpdate(Data(body.utf8))), body) } + /// The read-authentication body and the push-update envelope { auth, push } are ENCODED only by + /// the app (the server decodes them), so they are checked against the fixture bytes directly + /// from the fixture's own field values. + func testReadAuthenticationEncodesToTheFixtureBytes() throws { + let body = try envelope("read_authentication") + let auth = ReadAuth(enrollmentId: "enr-482913", requestedAt: "2026-09-18T12:00:30Z", assertionB64: "omlzaWduYXR1cmU") + XCTAssertEqual(WireEncode.readRequest(auth), body) + let pushBody = try envelope("push_update") + let push = try WireDecode.pushUpdate(Data(pushBody.utf8)) + XCTAssertEqual(WireEncode.pushUpdateRequest(auth, push), try envelope("push_update_request")) + } + /// Every response body decodes strictly, with its declared members present and non-empty. func testResponsesDecode() throws { XCTAssertFalse(try WireDecode.enrolmentGrant(Data(try envelope("enrolment_grant").utf8)).enrollment_id.isEmpty) @@ -250,14 +262,12 @@ final class ProtocolVectorTests: XCTestCase { XCTAssertEqual(got, Data(try envelope("push_update_client_data").utf8)) } - /// Every header name and route the app spells is the fixture's; a missing surface row FAILS, so + /// The method and every route the app spells is the fixture's; a missing surface row FAILS, so /// a route the wire adds and the app does not spell is caught, not silently absent. func testSurfaceMatchesTheFixture() throws { let rows = Dictionary(uniqueKeysWithValues: try load().surface.map { ($0.name, $0.value) }) func surface(_ name: String) throws -> String { try XCTUnwrap(rows[name], "surface row \(name) missing") } - XCTAssertEqual(ReadHeader.enrollment, try surface("header_enrollment")) - XCTAssertEqual(ReadHeader.requestedAt, try surface("header_requested_at")) - XCTAssertEqual(ReadHeader.assertion, try surface("header_assertion")) + XCTAssertEqual("POST", try surface("method_every_device_operation")) XCTAssertEqual(Route.enrol, try surface("route_enrol")) XCTAssertEqual(Route.pending, try surface("route_pending")) XCTAssertEqual(Route.requestPrefix, try surface("route_request_prefix")) diff --git a/apps/approve-ios/project.yml b/apps/approve-ios/project.yml index dc72ee4ba95..50dea4393d3 100644 --- a/apps/approve-ios/project.yml +++ b/apps/approve-ios/project.yml @@ -23,6 +23,8 @@ targets: settings: base: PRODUCT_BUNDLE_IDENTIFIER: ai.gunb.approve + MARKETING_VERSION: "1" + CURRENT_PROJECT_VERSION: 1 INFOPLIST_KEY_UILaunchScreen_Generation: YES INFOPLIST_KEY_NSFaceIDUsageDescription: "Approving a request signs it with a key that only unlocks with Face ID." INFOPLIST_KEY_CFBundleDisplayName: Approve diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index 645669553f8..1ce06073810 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -411,6 +411,15 @@ type FilesystemDirectoryListing sole_constructor { entries: String } +// THE ENTRY NAMES OF AN ADMITTED LISTING, decoded once beside the encoding they come from: `List` +// joins names with newlines, so this is the split -- blank lines dropped, every other line one +// name as the host spelled it. A consumer that split `entries` itself would be the second +// decoder of one wire format (review 69704 of gunbc#12000 found one; extdeps.realization +// artifact_store_fs carries an older one under filesystem_absence_establishment_adoption_standing). +fn filesystem_listing_entry_names(listing: FilesystemDirectoryListing) -> List { + filter(listing.entries.split(delimiter: "\n"), n => n != "") +} + type FilesystemEstablishedAbsence sole_constructor { directory: FilePath name: String diff --git a/dag/gunbc/auth/approval_app_attest_config.dag b/dag/gunbc/auth/approval_app_attest_config.dag new file mode 100644 index 00000000000..f45e5f263d1 --- /dev/null +++ b/dag/gunbc/auth/approval_app_attest_config.dag @@ -0,0 +1,53 @@ +module gunbc.auth.approval_app_attest_config + +import std.types { NonEmptyStr, Int, List } +import extdeps.apple.app_attest { AppIdPrefix, AppAttestEnvironment, AppAttestDevelopment, app_attest_app_id } + +// THE FACTS THE APP ATTEST VERIFIER IS CONFIGURED WITH, and who owns each. The bundle identifier +// is the app's (apps/approve-ios/project.yml PRODUCT_BUNDLE_IDENTIFIER). The App ID prefix is +// read from the Identifier entry of the operator's Apple Developer account -- its own fact, not a +// second name for the team id (extdeps.apple.app_attest AppIdPrefix). The environment is decided +// by how the build reaches the phone: TestFlight and App Store builds attest in production. The +// admitted launch categories are Apple's validation categories for those distributions (2 = +// TestFlight, 4 = App Store; 3 = a development signing identity is admitted so the operator's +// own Xcode build can enrol during bring-up), and the bundle version is the one the operator +// distributed. +// +// THE OPERATOR SUPPLIED THE PREFIX (chat, 2026-09-22): the Team ID 72HGYAMBVQ shown under +// Membership details, which Apple uses as the App ID prefix for an account's own identifiers. The +// bring-up build reaches the phone from the operator's Xcode over a cable, so it attests in the +// development environment with a development signing identity (category 3); TestFlight (2) and +// App Store (4) stay admitted for the day the distribution changes, and the bundle version is the +// MARKETING_VERSION apps/approve-ios/project.yml sets. A wrong prefix does not fabricate: every +// attestation refuses AttestationAppIdMismatch by name. The row below is the one place that changes. +type AppAttestVerifierConfig + = AppAttestVerifierConfigured { + app_id_prefix: AppIdPrefix + bundle_id: NonEmptyStr + environment: AppAttestEnvironment + admitted_validation_categories: List + expected_bundle_version: NonEmptyStr + } + | AppAttestVerifierAwaitingOperator { missing: NonEmptyStr } + +data approval_app_bundle_id: NonEmptyStr = "ai.gunb.approve" + +data approval_app_attest_verifier: AppAttestVerifierConfig = AppAttestVerifierConfigured { + app_id_prefix: "72HGYAMBVQ" as AppIdPrefix, + bundle_id: approval_app_bundle_id, + environment: AppAttestDevelopment, + admitted_validation_categories: [2, 3, 4], + expected_bundle_version: approval_app_bundle_version, +} + +// CFBundleShortVersionString of the operator's build: the same literal apps/approve-ios/project.yml +// sets as MARKETING_VERSION, which is hand-authored Swift/XcodeGen seed and cannot read this row. +data approval_app_bundle_version: NonEmptyStr = "1" + +fn approval_app_attest_app_id(c: AppAttestVerifierConfig) -> NonEmptyStr? { + match c { + AppAttestVerifierAwaitingOperator { missing: _ } => none + AppAttestVerifierConfigured { app_id_prefix: p, bundle_id: b, environment: _, admitted_validation_categories: _, expected_bundle_version: _ } => + Present { value: app_attest_app_id(prefix: p, bundle_id: b) } + } +} diff --git a/dag/gunbc/auth/approval_assertion_counter.dag b/dag/gunbc/auth/approval_assertion_counter.dag new file mode 100644 index 00000000000..017f4119485 --- /dev/null +++ b/dag/gunbc/auth/approval_assertion_counter.dag @@ -0,0 +1,116 @@ +module gunbc.auth.approval_assertion_counter + +import std.types { NonEmptyStr, String, Int, HttpStatus } +import std.logic { Bool } +import gunbc.durable_cas_file_store { + OwnerOnlyCreateOnly, admit_cas_attempt_for_derived_payload, DerivedPayloadAdmitted, DerivedPayloadKeyNotSlotAddressable, + file_compare_and_set, observe_cas_slot_state, +} +import std.durable_compare_and_set { + cas_unreadable_slot_detail, CasCommitted, CasPreconditionFailed, CasStoreRefused, + CasObservedReadable, CasObservedUnreadable, CasReadableAbsent, CasReadablePresent, + CasGeneration, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, +} + +// ── THE APP ATTEST ASSERTION COUNTER, COMMITTED BY ITS CONSUMER ────────────────────────────── +// extdeps.apple.app_attest carries AuthenticAssertion.counter OUT of the verifier because Apple's +// step 5 -- the counter exceeds the one last stored for this key -- needs the consumer's state. This +// module is that consumer state for the device routes: one CAS slot per enrolment holding the last +// admitted counter, advanced by ONE compare-and-set whose expectation is the generation that was +// read. So "observed > stored, commit observed, then perform the operation" is atomic: two requests +// carrying the same captured assertion read the same generation, at most one commit lands, and the +// loser is refused before its operation runs. A timestamp window alone is not this wall -- a +// captured read replays inside it -- which is why the skew check in the routes is kept beside this +// standing rather than in place of it. +// +// WHICH ROUTES CONSULT IT is gunbc.auth.approval_device_routes' decision, stated there: the three +// reads and the push update do; the redemption POST does not, because its own replay wall is the +// server-minted expiring challenge and the one-decision CAS slot, and Apple's counter is monotonic +// across every assertion of the key, so a redemption that does not advance the standing leaves the +// reads' comparison sound. +// +// THE SLOT GROWS ONE GENERATION PER ADMITTED ASSERTION, AND THAT IS NO LONGER A LIVENESS BOUND. +// It was: gunbc.durable_cas_file_store walked a slot linearly from generation 1 and refused past 4096 +// generations, so an enrolment stopped being readable (a 503 here) after ~4096 admitted requests and +// only re-enrolment recovered it. The fact kept here is ONE value -- last_admitted_counter -- and no +// consumer reads a superseded generation, so the store now finds the head by galloping and bisecting +// over the contiguous chain, O(log n) reads, with its typed bound at the generation carrier's Int +// range rather than at a count a phone reaches. The chain itself stays because it is the store's +// O_EXCL exclusion mechanism, which is what makes the commit below atomic across racing requests. +// Storage still grows one small file per admitted assertion; that is disk, not a refusal. +// test.claim.approval_assertion_counter_wet_witness_test admits past the old bound to keep it so. + +data approval_assertion_counter_root: NonEmptyStr = "/var/lib/gunbc/approval-assertion-counters" + +type AssertionCounterStanding { + enrollment_id: NonEmptyStr + last_admitted_counter: Int + generation: CasGeneration +} + +type AssertionCounterObservation + = AssertionCounterNeverAdmitted + | AssertionCounterStood { standing: AssertionCounterStanding } + | AssertionCounterUnreadable { detail: NonEmptyStr } + +type AssertionCounterAdmission + = AssertionCounterAdmitted { enrollment_id: NonEmptyStr, counter: Int } + | AssertionCounterReplayed { observed: Int, last_admitted: Int } + | AssertionCounterRaced + | AssertionCounterStoreRefused { detail: NonEmptyStr } + +fn observe_assertion_counter(root: NonEmptyStr, enrollment_id: NonEmptyStr) -> AssertionCounterObservation { + match observe_cas_slot_state(root: root, key: enrollment_id) { + CasObservedUnreadable { cause: c } => AssertionCounterUnreadable { detail: concat("assertion counter slot unreadable: ", cas_unreadable_slot_detail(cause: c)) as NonEmptyStr } + CasObservedReadable { readable: r } => match r { + CasReadableAbsent => AssertionCounterNeverAdmitted + CasReadablePresent { version: v } => + match parse_int(s: v.value as String) { + Absent => AssertionCounterUnreadable { detail: "assertion counter slot holds no integer" } + Present { value: n } => AssertionCounterStood { standing: AssertionCounterStanding { enrollment_id: enrollment_id, last_admitted_counter: n, generation: v.generation } } + } + } + } +} + +fn assertion_counter_commit(root: NonEmptyStr, enrollment_id: NonEmptyStr, expected: CasExpectation, observed: Int) -> AssertionCounterAdmission { + match admit_cas_attempt_for_derived_payload(key: enrollment_id, expected: expected, proposed: to_string(observed) as NonEmptyStr) { + DerivedPayloadKeyNotSlotAddressable { key: _ } => AssertionCounterStoreRefused { detail: "enrolment id is not slot-addressable" } + DerivedPayloadAdmitted { verified: v } => + match file_compare_and_set(root: root, publication: OwnerOnlyCreateOnly, verified: v) { + CasCommitted { committed: _ } => AssertionCounterAdmitted { enrollment_id: enrollment_id, counter: observed } + CasPreconditionFailed { expected: _, observed: _ } => AssertionCounterRaced + CasStoreRefused { cause: _ } => AssertionCounterStoreRefused { detail: "assertion counter store refused the publication" } + } + } +} + +// THE ADMISSION: the observed counter strictly exceeds the standing, and the commit of it is the +// admission. Equal is a replay (the same assertion again), lower is a replay of an older one. +fn admit_assertion_counter(root: NonEmptyStr, enrollment_id: NonEmptyStr, observed: Int) -> AssertionCounterAdmission { + match observe_assertion_counter(root: root, enrollment_id: enrollment_id) { + AssertionCounterUnreadable { detail: d } => AssertionCounterStoreRefused { detail: d } + AssertionCounterNeverAdmitted => assertion_counter_commit(root: root, enrollment_id: enrollment_id, expected: ExpectSlotAbsent, observed: observed) + AssertionCounterStood { standing: s } => + if observed <= s.last_admitted_counter { AssertionCounterReplayed { observed: observed, last_admitted: s.last_admitted_counter } } + else { assertion_counter_commit(root: root, enrollment_id: enrollment_id, expected: ExpectSlotGeneration { generation: s.generation }, observed: observed) } + } +} + +fn assertion_counter_refusal_status(a: AssertionCounterAdmission) -> HttpStatus { + match a { + AssertionCounterAdmitted { enrollment_id: _, counter: _ } => 200 + AssertionCounterReplayed { observed: _, last_admitted: _ } => 403 + AssertionCounterRaced => 409 + AssertionCounterStoreRefused { detail: _ } => 503 + } +} + +fn assertion_counter_refusal_reason(a: AssertionCounterAdmission) -> String { + match a { + AssertionCounterAdmitted { enrollment_id: _, counter: _ } => "admitted" + AssertionCounterReplayed { observed: o, last_admitted: l } => "the assertion counter " + to_string(o) + " does not exceed the last admitted " + to_string(l) + ": a replay" + AssertionCounterRaced => "another assertion for this enrolment was admitted concurrently" + AssertionCounterStoreRefused { detail: d } => d as String + } +} diff --git a/dag/gunbc/auth/approval_broker_endpoint.dag b/dag/gunbc/auth/approval_broker_endpoint.dag index 2dde13d1a88..cfd2a2bf35b 100644 --- a/dag/gunbc/auth/approval_broker_endpoint.dag +++ b/dag/gunbc/auth/approval_broker_endpoint.dag @@ -8,6 +8,7 @@ import extdeps.external_authority { ExternalAuthority, CitedFigureStanding, Cite import gunbc.auth.approval_ntfy_deployment { srv1_tailnet_base_url_from } import gunbc.fleet_intent_network { fleet_intent_network } import gunbc.serve_liveness { serve_liveness_path } +import gunbc.auth.approval_device_wire { approval_device_request_path_prefix, approval_device_enrollment_path_prefix } // ── WHERE THE APPROVAL BROKER ANSWERS ──────────────────────────────────────────────────────── // ONE FACT, FOUR READERS. The four approval paths are read by the broker's route table @@ -35,6 +36,12 @@ data approval_broker_submit_path: NonEmptyStr = "/approvals" data approval_broker_status_path_template: NonEmptyStr = "/approvals/\{escalation_id\}" +// THE SIX DEVICE ROUTES' TEMPLATES, spelled from gunbc.auth.approval_device_wire's paths (the app's +// authority) rather than re-typed here: the two suffixed routes take one ParamToken segment, the +// four fixed routes are the wire's literals. Every device operation is a POST. +data approval_device_request_path_template: NonEmptyStr = join([approval_device_request_path_prefix as String, "\{segment\}"], "") as NonEmptyStr +data approval_device_enrollment_path_template: NonEmptyStr = join([approval_device_enrollment_path_prefix as String, "\{segment\}"], "") as NonEmptyStr + // ── The broker's own listener ──────────────────────────────────────────────────────────────── // A SEPARATE PORT IS WHAT MAKES THE SEPARATE PROCESS OBSERVABLE. Two units with two MainPIDs that // shared a socket would be a lie the first `ss` would expose; the broker binds its own loopback diff --git a/dag/gunbc/auth/approval_broker_marker.dag b/dag/gunbc/auth/approval_broker_marker.dag index f54604e7f8c..461a61c3cb9 100644 --- a/dag/gunbc/auth/approval_broker_marker.dag +++ b/dag/gunbc/auth/approval_broker_marker.dag @@ -57,6 +57,12 @@ type ApprovalBrokerMarker | DecisionHandlerObserved | SubmissionHandlerObserved | StatusHandlerObserved + | DeviceEnrolHandlerObserved + | DeviceRedeemHandlerObserved + | DevicePendingHandlerObserved + | DeviceRequestHandlerObserved + | DeviceEnrollmentReadbackHandlerObserved + | DevicePushUpdateHandlerObserved | BrokerNoRouteMatched | BrokerMethodNotAllowed | BrokerAdapterRefused @@ -102,6 +108,12 @@ fn approval_broker_marker_token(m: ApprovalBrokerMarker) -> NonEmptyStr { DecisionHandlerObserved => "decision" as NonEmptyStr SubmissionHandlerObserved => "submission" as NonEmptyStr StatusHandlerObserved => "status" as NonEmptyStr + DeviceEnrolHandlerObserved => "device-enrol" as NonEmptyStr + DeviceRedeemHandlerObserved => "device-redeem" as NonEmptyStr + DevicePendingHandlerObserved => "device-pending" as NonEmptyStr + DeviceRequestHandlerObserved => "device-request" as NonEmptyStr + DeviceEnrollmentReadbackHandlerObserved => "device-enrollment-readback" as NonEmptyStr + DevicePushUpdateHandlerObserved => "device-push-update" as NonEmptyStr BrokerNoRouteMatched => "no-route-matched" as NonEmptyStr BrokerMethodNotAllowed => "method-not-allowed" as NonEmptyStr BrokerAdapterRefused => "adapter-refused" as NonEmptyStr @@ -111,7 +123,10 @@ fn approval_broker_marker_token(m: ApprovalBrokerMarker) -> NonEmptyStr { data approval_broker_markers: List = [ ConfirmHandlerObserved, DecisionHandlerObserved, SubmissionHandlerObserved, - StatusHandlerObserved, BrokerNoRouteMatched, BrokerMethodNotAllowed, BrokerAdapterRefused, + StatusHandlerObserved, + DeviceEnrolHandlerObserved, DeviceRedeemHandlerObserved, DevicePendingHandlerObserved, + DeviceRequestHandlerObserved, DeviceEnrollmentReadbackHandlerObserved, DevicePushUpdateHandlerObserved, + BrokerNoRouteMatched, BrokerMethodNotAllowed, BrokerAdapterRefused, BrokerStaticRouteServed, ] diff --git a/dag/gunbc/auth/approval_broker_serve.dag b/dag/gunbc/auth/approval_broker_serve.dag index b374fa5886c..bf72d6740a2 100644 --- a/dag/gunbc/auth/approval_broker_serve.dag +++ b/dag/gunbc/auth/approval_broker_serve.dag @@ -26,6 +26,8 @@ import gunbc.auth.approval_writer_authority { import gunbc.auth.approval_broker_marker { ApprovalBrokerMarker, approval_broker_marked_body, ConfirmHandlerObserved, DecisionHandlerObserved, SubmissionHandlerObserved, StatusHandlerObserved, + DeviceEnrolHandlerObserved, DeviceRedeemHandlerObserved, DevicePendingHandlerObserved, + DeviceRequestHandlerObserved, DeviceEnrollmentReadbackHandlerObserved, DevicePushUpdateHandlerObserved, BrokerNoRouteMatched, BrokerMethodNotAllowed, BrokerAdapterRefused, BrokerStaticRouteServed, } import gunbc.auth.approval_broker_endpoint { @@ -34,7 +36,15 @@ import gunbc.auth.approval_broker_endpoint { approval_broker_submit_path, approval_broker_status_path_template, approval_broker_confirm_path_prefix, + approval_device_request_path_template, + approval_device_enrollment_path_template, } +import gunbc.auth.approval_device_wire { approval_device_enrol_path, approval_device_redeem_path, approval_device_pending_path, approval_device_push_path } +import gunbc.auth.approval_device_routes { + DeviceRouteResponse, + device_enrol_response, device_redeem_response, device_pending_response, device_request_response, device_enrollment_readback_response, device_push_update_response, +} +import extdeps.http.server { application_json_utf8 } import std.types { String, Int, Bool, List, NonEmptyStr, CommitSha, HttpStatus } import extdeps.uri_path { PathParamBinding, path_param_value } import std.markup { Fragment, attr } @@ -100,6 +110,12 @@ type ApprovalBrokerHandler | ApprovalDecideHandler | ApprovalSubmitHandler | ApprovalStatusHandler + | DeviceEnrolHandler + | DeviceRedeemHandler + | DevicePendingHandler + | DeviceRequestHandler + | DeviceEnrollmentReadbackHandler + | DevicePushUpdateHandler // THE APPROVAL PAIR IS TWO ROUTES ON PURPOSE. The operator's tap is a GET, and a GET must not // spend the decision -- link previews, mail scanners, chat unfurlers and browser prefetch all @@ -118,6 +134,12 @@ fn approval_broker_route_specs() -> List> ServedRouteSpec { method: POST, raw: approval_broker_decide_path_template as String, handler: ApprovalDecideHandler }, ServedRouteSpec { method: POST, raw: approval_broker_submit_path as String, handler: ApprovalSubmitHandler }, ServedRouteSpec { method: GET, raw: approval_broker_status_path_template as String, handler: ApprovalStatusHandler }, + ServedRouteSpec { method: POST, raw: approval_device_enrol_path as String, handler: DeviceEnrolHandler }, + ServedRouteSpec { method: POST, raw: approval_device_redeem_path as String, handler: DeviceRedeemHandler }, + ServedRouteSpec { method: POST, raw: approval_device_pending_path as String, handler: DevicePendingHandler }, + ServedRouteSpec { method: POST, raw: approval_device_request_path_template as String, handler: DeviceRequestHandler }, + ServedRouteSpec { method: POST, raw: approval_device_enrollment_path_template as String, handler: DeviceEnrollmentReadbackHandler }, + ServedRouteSpec { method: POST, raw: approval_device_push_path as String, handler: DevicePushUpdateHandler }, ] } @@ -125,6 +147,16 @@ fn approval_broker_route_table_build() -> ServedRouteTableBuild ServeHttpResponse { + broker_text_response(status: r.status, content_type: application_json_utf8, body: r.body, marker: marker, process: process) +} + // EVERY RESPONSE EITHER SERVING PROCESS EMITS FROM THESE FOLDS PASSES THROUGH HERE, which is why // the marker and the process are PARAMETERS of this fold rather than something each handler // remembers to append. A caller cannot construct a response without naming which fold produced it @@ -461,6 +493,12 @@ fn approval_broker_invoke( ApprovalDecideHandler => approval_decide_response(request: request, params: params, process: process) ApprovalSubmitHandler => approval_submit_response(request: request, process: process) ApprovalStatusHandler => approval_status_response(params: params, process: process) + DeviceEnrolHandler => device_route_response(marker: DeviceEnrolHandlerObserved, process: process, r: device_enrol_response(body: request.body, process: process)) + DeviceRedeemHandler => device_route_response(marker: DeviceRedeemHandlerObserved, process: process, r: device_redeem_response(body: request.body, process: process)) + DevicePendingHandler => device_route_response(marker: DevicePendingHandlerObserved, process: process, r: device_pending_response(body: request.body)) + DeviceRequestHandler => device_route_response(marker: DeviceRequestHandlerObserved, process: process, r: device_request_response(body: request.body, segment: path_param_value(params: params, name: "segment"))) + DeviceEnrollmentReadbackHandler => device_route_response(marker: DeviceEnrollmentReadbackHandlerObserved, process: process, r: device_enrollment_readback_response(body: request.body, segment: path_param_value(params: params, name: "segment"))) + DevicePushUpdateHandler => device_route_response(marker: DevicePushUpdateHandlerObserved, process: process, r: device_push_update_response(body: request.body, process: process)) } } diff --git a/dag/gunbc/auth/approval_capability.dag b/dag/gunbc/auth/approval_capability.dag index 29711cde0db..006438019f9 100644 --- a/dag/gunbc/auth/approval_capability.dag +++ b/dag/gunbc/auth/approval_capability.dag @@ -337,6 +337,28 @@ fn utc_instant_before(a: Timestamp, b: Timestamp) -> Bool { a < b } +// THE SIGNED DISTANCE IN SECONDS BETWEEN TWO CANONICAL INSTANTS, as a pure fold over the fields +// utc_instant_is_canonical already validates -- so a window around an instant is a comparison of +// two integers, not a clock call. Like utc_instant_before it is defined ONLY on canonical pairs; +// the caller establishes canonicity first. Days are counted from a proleptic Gregorian origin +// shifted by one 400-year cycle, which keeps every term non-negative (year 0000 included) without +// changing any leap year; the shift cancels in the difference. +data month_numbers: List = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12] + +fn utc_instant_seconds(t: Timestamp) -> Int { + let year = number_at(t: t, offsets: year_offsets) + let month = number_at(t: t, offsets: month_offsets) + let shifted = year + 399 + let days_before_year = 365 * shifted + shifted / 4 - shifted / 100 + shifted / 400 + let days_before_month = fold(filter(month_numbers, m => m < month), init: 0, f: (acc, m) => acc + days_in_month(y: year, m: m)) + let days = days_before_year + days_before_month + number_at(t: t, offsets: day_offsets) - 1 + days * 86400 + number_at(t: t, offsets: hour_offsets) * 3600 + number_at(t: t, offsets: minute_offsets) * 60 + number_at(t: t, offsets: second_offsets) +} + +fn utc_instant_seconds_after(later: Timestamp, earlier: Timestamp) -> Int { + utc_instant_seconds(t: later) - utc_instant_seconds(t: earlier) +} + // EXPIRY IS CHECKED WITH A STRICT COMPARISON AT THE BOUNDARY INSTANT. // // std.scoped_authorization grant_not_expired_at uses `<=`, which INCLUDES the expiry instant. That diff --git a/dag/gunbc/auth/approval_decision_store.dag b/dag/gunbc/auth/approval_decision_store.dag index b8603ff172c..ae8ed9a9d07 100644 --- a/dag/gunbc/auth/approval_decision_store.dag +++ b/dag/gunbc/auth/approval_decision_store.dag @@ -31,6 +31,7 @@ import gunbc.durable_cas_file_store { DerivedPayloadKeyNotSlotAddressable, file_compare_and_set, observe_cas_slot_state, + CasSlotKeys, CasSlotKeysListed, CasSlotKeysListingRefused, CasSlotKeysSubjectRefused, cas_slot_keys, } import std.durable_compare_and_set { cas_unreadable_slot_detail, @@ -799,3 +800,36 @@ data approval_keyring_materialization_frontier: DissolutionCondition = unbound_d description: "a fleet-converge step that reads approval_mac_key_secret_ref and approval_submission_mac_key_secret_ref through the WIF-backed convergence account and writes approval_mac_key_path and approval_submission_mac_key_path (0640 root:) on the host that serves /approve and /approvals, over the fleet SSH administrator edge rather than a job-user sudo -- SUFFICIENT FOR both keyrings to read ApprovalKeyLoaded on that host; lands as gunbc.auth.approval_keyring_converge (#11484)", ) + + +// ── The pending escalations ────────────────────────────────────────────────────────────────── +// WHAT THE PHONE LISTS ON OPEN: every filed escalation whose slot stands EscalationPending. The +// keys come from the store's own listing (gunbc.durable_cas_file_store cas_slot_keys, the inverse +// of the layout it writes), and each standing is read through observe_escalation exactly as a +// single read would be -- the listing decides which slots exist, never what they hold. A slot +// that cannot be read is carried as a refusal beside the rows, not dropped: a pending approval +// the phone cannot see is a decision that never happens. +type PendingEscalations + = PendingEscalationsListed { pending: List, unreadable: List } + | PendingEscalationsRefused { detail: String } + +type PendingFold { + pending: List + unreadable: List +} + +fn pending_escalations(root: NonEmptyStr) -> PendingEscalations { + match cas_slot_keys(root: root) { + CasSlotKeysListingRefused { root: _, detail: d } => PendingEscalationsRefused { detail: d } + CasSlotKeysSubjectRefused { root: r, cause: c } => PendingEscalationsRefused { detail: "store root " + (r as String) + " is not an admissible directory: " + c } + CasSlotKeysListed { keys: keys } => { + let f = fold(keys, init: PendingFold { pending: [], unreadable: [] }, f: (acc, k) => match observe_escalation(root: root, escalation_id: k) { + EscalationPending { request: r } => PendingFold { pending: acc.pending |> list_push(r), unreadable: acc.unreadable } + EscalationUnreadable { detail: _ } => PendingFold { pending: acc.pending, unreadable: acc.unreadable |> list_push(k) } + EscalationDecided { decision: _ } => acc + EscalationNotFiled => acc + }) + PendingEscalationsListed { pending: f.pending, unreadable: f.unreadable } + } + } +} diff --git a/dag/gunbc/auth/approval_device_crypto_realization.dag b/dag/gunbc/auth/approval_device_crypto_realization.dag new file mode 100644 index 00000000000..b01938e36a2 --- /dev/null +++ b/dag/gunbc/auth/approval_device_crypto_realization.dag @@ -0,0 +1,83 @@ +module gunbc.auth.approval_device_crypto_realization + +import std.types { NonEmptyStr, String, List, HttpStatus } +import std.logic { Bool } + +// ── WHICH REALIZATION RUNS THE DEVICE VERIFIERS IS PART OF ROUTE ADMISSION ─────────────────── +// extdeps.crypto.signature verify_signature and extdeps.apple.app_attest verify_attestation / +// verify_assertion are authored .dag folds. Called from an interpreted broker they ARE the +// interpreter -- the cost gunbc.auth.approval_device_redemption ecdsa_verification_realization_frontier +// names, per request, on the approval broker -- so a route that invoked them with nothing in front +// would realize that frontier as the evaluator. That frontier is therefore not an annotation beside +// the routes: every verifier-dependent route in gunbc.auth.approval_device_routes asks +// device_crypto_admission FIRST and refuses 503 with the typed cause before any decode, store read +// or verifier call when the native handler is not bound (DESIGN section 5: a frontier that is only +// an annotation is not a wall). +// +// Selecting the realization is itself realization (DESIGN section 3), so this module sits beside +// the routes, never inside the verifier interface. +// +// THE RECEIPT COVERS A NAMED POPULATION, NOT "THE VERIFIER RUNS NATIVELY". A bound handler is +// admitted only when its receipt lists every obligation below, and the P-256 base-point ORDER is its +// own obligation: a passing signature vector does not establish that the published base point has +// the declared order, so a receipt that covered only verification would admit the routes while the +// order fact the frontier names stayed dead. + +type DeviceCryptoObligation + = P256SignatureVerification + | AppAttestAttestationVerification + | AppAttestAssertionVerification + | P256BasePointOrder + +// The full population a bound handler must cover. +data device_crypto_obligations: List = [ + P256SignatureVerification, AppAttestAttestationVerification, AppAttestAssertionVerification, P256BasePointOrder, +] + +// What executing evidence discharges each obligation on the natively emitted route. +fn device_crypto_obligation_evidence(o: DeviceCryptoObligation) -> NonEmptyStr { + match o { + P256SignatureVerification => "extdeps.crypto.signature verify_signature (EcdsaP256Sha256) executing on the natively emitted handler" + AppAttestAttestationVerification => "extdeps.apple.app_attest verify_attestation executing on the natively emitted handler" + AppAttestAssertionVerification => "extdeps.apple.app_attest verify_assertion executing on the natively emitted handler" + P256BasePointOrder => "test.claim.p256_dag_ecdsa_witness_test the_base_point_has_order_n (n*G == infinity for the published base point) with its discriminating control (n-1)*G != infinity, executing natively" + } +} + +type DeviceCryptoHandlerReceipt { + handler_identity: NonEmptyStr + exact_revision: NonEmptyStr + covered: List +} + +type DeviceCryptoRealization + = NativeDeviceCryptoBound { receipt: DeviceCryptoHandlerReceipt } + | NativeDeviceCryptoUnavailable { cause: NonEmptyStr } + +// THE PRODUCTION BINDING. Unavailable until a natively emitted handler exists with a receipt over the +// whole population -- the capability ecdsa_verification_realization_frontier names; no PR in flight +// discharges it. Writing a Bound arm here is the whole cutover and it is admitted only with that +// handler's identity and exact revision, so the review of that one row is where the claim is made. +data approval_device_crypto_realization: DeviceCryptoRealization = NativeDeviceCryptoUnavailable { + cause: "no natively emitted realization handler of the device verifiers is bound (gunbc.auth.approval_device_redemption ecdsa_verification_realization_frontier); the interpreted verifiers are not admitted per request", +} + +type DeviceCryptoAdmission + = DeviceCryptoAdmitted { handler_identity: NonEmptyStr, exact_revision: NonEmptyStr } + | DeviceCryptoRefused { status: HttpStatus, reason: String } + +fn device_crypto_missing(receipt: DeviceCryptoHandlerReceipt) -> List { + filter(device_crypto_obligations, o => !any(receipt.covered, c => c == o)) +} + +fn device_crypto_admission(r: DeviceCryptoRealization) -> DeviceCryptoAdmission { + match r { + NativeDeviceCryptoUnavailable { cause: c } => DeviceCryptoRefused { status: 503, reason: "the native device-crypto realization is unavailable: " + (c as String) } + NativeDeviceCryptoBound { receipt: rc } => + if count(device_crypto_missing(receipt: rc)) > 0 { + DeviceCryptoRefused { status: 503, reason: "the native device-crypto handler receipt does not cover: " + join(map(device_crypto_missing(receipt: rc), o => device_crypto_obligation_evidence(o: o) as String), "; ") } + } else { + DeviceCryptoAdmitted { handler_identity: rc.handler_identity, exact_revision: rc.exact_revision } + } + } +} diff --git a/dag/gunbc/auth/approval_device_redemption.dag b/dag/gunbc/auth/approval_device_redemption.dag index 8f5cfeefbf9..55fb7007d1c 100644 --- a/dag/gunbc/auth/approval_device_redemption.dag +++ b/dag/gunbc/auth/approval_device_redemption.dag @@ -40,7 +40,7 @@ import gunbc.durable_cas_file_store { import std.durable_compare_and_set { cas_unreadable_slot_detail, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasObservedReadable, CasObservedUnreadable, CasReadableAbsent, CasReadablePresent, - CasGeneration, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, cas_generation_first, cas_generation_next, cas_generation_count, + CasGeneration, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, cas_generation_first, cas_generation_count, } import extdeps.languages.json.emit { JsonValue, JsonKeyValue, serialize_json, json_object, json_kv, json_string } import extdeps.languages.json.parse { JsonDocumentParsed, JsonDocumentUnreadable, parse_json_document } @@ -536,8 +536,8 @@ fn enrolment_record_kind_wire(k: EnrolmentRecordKind) -> NonEmptyStr { fn enrolment_record_kind_generation(k: EnrolmentRecordKind) -> CasGeneration { match k { IssuedCodeRecord => cas_generation_first() - EnrolledRecord => cas_generation_next(g: cas_generation_first()) - RevokedRecord => cas_generation_next(g: cas_generation_next(g: cas_generation_first())) + EnrolledRecord => 2 + RevokedRecord => 3 } } diff --git a/dag/gunbc/auth/approval_device_redemption_fixtures.dag b/dag/gunbc/auth/approval_device_redemption_fixtures.dag index a18c2ab0568..471694ae0d3 100644 --- a/dag/gunbc/auth/approval_device_redemption_fixtures.dag +++ b/dag/gunbc/auth/approval_device_redemption_fixtures.dag @@ -13,7 +13,7 @@ import gunbc.auth.approval_device_wire { enrolment_request_json, signed_redemption_json, push_update_json, enrolment_grant_json, pending_list_json, fetched_request_json, enrolment_readback_json, redemption_response_json, device_push_update_client_data, device_request_path, device_enrollment_path, enrollment_id_for_code, path_segment, - approval_device_enrollment_header, approval_device_requested_at_header, approval_device_assertion_header, + ReadAuthentication, read_authentication_json, PushUpdateRequest, push_update_request_json, approval_device_enrol_path, approval_device_redeem_path, approval_device_enrollment_path_prefix, approval_device_push_path, } import extdeps.crypto.signature { SignatureBytes, P1363FixedWidth } @@ -118,7 +118,7 @@ fn enrolment_vector_json(v: EnrolmentVector) -> JsonValue { ]) } -// The read transcript an App Attest assertion covers on the two authenticated GETs. +// The read transcript an App Attest assertion covers on the three authenticated reads (POSTs). type ReadVector { name: NonEmptyStr path: NonEmptyStr @@ -149,6 +149,7 @@ fn read_vector_json(v: ReadVector) -> JsonValue { // requests and must produce these bytes; it decodes the responses and must read these values. data fx_point: NonEmptyStr = "BHt2Zm9vYmFyYmF6cXV4" data fx_push: PushRegistration = ApnsRegistration { environment: ApnsProduction, topic: "ai.gunb.approve", token: "a1b2c3d4e5f6" } +data fx_read_auth: ReadAuthentication = ReadAuthentication { enrollment_id: "enr-482913", requested_at: "2026-09-18T12:00:30Z" as Timestamp, assertion_b64: "omlzaWduYXR1cmU" } fn fx_signing_input() -> DeviceRedemptionSigningInput { match first(redemption_vectors) { Present { value: v } => v.input Absent => redemption_vector(name: "approve-plain", decision: ProposeApprove, stored_request_text: "{}").input } @@ -172,6 +173,8 @@ data envelope_vectors: List = [ platform_proof: IosAppAttestAssertion { assertion_b64: "omlzaWduYXR1cmU" }, }) }, EnvelopeVector { name: "push_update", body: push_update_json(p: fx_push) }, + EnvelopeVector { name: "read_authentication", body: read_authentication_json(a: fx_read_auth) }, + EnvelopeVector { name: "push_update_request", body: push_update_request_json(r: PushUpdateRequest { auth: fx_read_auth, push: fx_push }) }, EnvelopeVector { name: "enrolment_grant", body: enrolment_grant_json(g: EnrolmentGrant { enrollment_id: "enr-482913" }) }, EnvelopeVector { name: "pending_list", body: pending_list_json(rows: [PendingApproval { escalation_id: "esc-mtc1-boot-1", request_revision: "sha256:abab" }]) }, EnvelopeVector { name: "fetched_request", body: fetched_request_json(f: FetchedRequest { @@ -192,6 +195,16 @@ data envelope_vectors: List = [ EnvelopeVector { name: "enrollment_path", body: device_enrollment_path(enrollment_id: enrollment_id_for_code(code: "482913")) as String }, ] +// The body of one named envelope vector, so a claim can drive a route with the same bytes the +// Swift mirror decodes (review 69752 of gunbc#12000: the writer-gate claim owes an execution on +// every mutating route). `none` when no vector carries the name. +fn envelope_vector_body(name: String) -> String? { + match first(filter(envelope_vectors, v => v.name == name)) { + Present { value: v } => Present { value: v.body } + Absent => none + } +} + fn envelope_vector_json(v: EnvelopeVector) -> JsonValue { json_object(members: [ json_kv(key: "name", value: json_string(s: v.name as String)), @@ -201,17 +214,16 @@ fn envelope_vector_json(v: EnvelopeVector) -> JsonValue { // ── The HTTP surface ───────────────────────────────────────────────────────────────────────── // EVERY NAME THE APP SENDS OR ADDRESSES, from the wire's own rows, so Wire.swift restates none of -// them: the three authenticated-request headers, every fixed route and route prefix, and the path -// segment encoding over specimens of each character class it must handle. +// them: the one method every device operation uses (authentication rides in the body, never in a +// header), every fixed route and route prefix, and the path segment encoding over specimens of +// each character class it must handle. type SurfaceVector { name: NonEmptyStr value: NonEmptyStr } data surface_vectors: List = [ - SurfaceVector { name: "header_enrollment", value: approval_device_enrollment_header }, - SurfaceVector { name: "header_requested_at", value: approval_device_requested_at_header }, - SurfaceVector { name: "header_assertion", value: approval_device_assertion_header }, + SurfaceVector { name: "method_every_device_operation", value: "POST" }, SurfaceVector { name: "route_enrol", value: approval_device_enrol_path }, SurfaceVector { name: "route_pending", value: approval_device_pending_path }, SurfaceVector { name: "route_request_prefix", value: approval_device_request_path_prefix }, diff --git a/dag/gunbc/auth/approval_device_routes.dag b/dag/gunbc/auth/approval_device_routes.dag new file mode 100644 index 00000000000..5c40515108d --- /dev/null +++ b/dag/gunbc/auth/approval_device_routes.dag @@ -0,0 +1,647 @@ +module gunbc.auth.approval_device_routes + +import std.types { NonEmptyStr, String, Int, List, Timestamp, HttpStatus } +import std.logic { Bool } +import std.integer { UInt8, QualifiedOctetsReady, QualifiedOctetsRefused } +import std.measure { Second, second, second_count, ByteSize, byte_size, byte_size_count } +import std.process { ProcessExit, ExitSuccess, exit_failure } +import std.dissolution { DissolutionCondition, unbound_dissolution } +import std.encoding { base64_decode, base64_octets, Standard, UrlSafe } +import std.algebra { trim } +import extdeps.clock { Clock } +import extdeps.entropy { Urandom } +import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.numeric.base16 { base16_encode_lower } +import extdeps.languages.json.emit { serialize_json, json_object, json_kv, json_string } +import extdeps.crypto.mac { MacKey, MacSigned, MacKeyMaterialNotHex, mac_sign } +import extdeps.crypto.signature { SignatureVerification, SignatureInvalid, EcdsaP256Sha256, verify_signature } +import extdeps.apple.app_attest { + AttestKeyId, AttestationVerification, AttestationRefused, AttestationRefusal, AttestationUndecodable, + AssertionVerification, AssertionRefused, AssertionUndecodable, AssertionAuthentic, + AttestationExpectation, verify_attestation, AssertionExpectation, verify_assertion, +} +import gunbc.cli_wire { CliWireResponse, CliWirePrintable, CliWireUnprintable } +import gunbc.clock_read { clock_now_probed_at } +import gunbc.auth.approval_capability { + ProposeApprove, ProposeDeny, utc_instant_is_canonical, utc_instant_before, utc_instant_seconds_after, + issue_capability, CapabilityIssued, CapabilityIssuanceRefused, approval_capability_signing_input, +} +import gunbc.auth.approval_app_attest_config { + AppAttestVerifierConfig, AppAttestVerifierConfigured, AppAttestVerifierAwaitingOperator, approval_app_attest_verifier, approval_app_attest_app_id, +} +import gunbc.auth.approval_device_crypto_realization { + DeviceCryptoRealization, DeviceCryptoAdmitted, DeviceCryptoRefused, device_crypto_admission, approval_device_crypto_realization, +} +import gunbc.auth.approval_assertion_counter { + AssertionCounterAdmitted, admit_assertion_counter, approval_assertion_counter_root, assertion_counter_refusal_status, assertion_counter_refusal_reason, +} +import gunbc.auth.approval_writer_authority { + ApprovalServingProcess, ApprovalWriteAdmitted, ApprovalWriteRefused, approval_write_admission, approval_write_refusal_reason, +} +import gunbc.auth.approval_decision_store { + approval_decision_store_root, read_approval_keyring, ApprovalKeyringRead, ApprovalKeyLoaded, ApprovalKeyringRefused, + StoredApprovalRequest, stored_request_json, observe_escalation, EscalationPending, EscalationDecided, EscalationNotFiled, EscalationUnreadable, + claims_for, pending_escalations, PendingEscalationsListed, PendingEscalationsRefused, +} +import gunbc.auth.approval_device_wire { + MobileIos, MobileAndroid, enrolment_transcript, device_read_client_data, device_push_update_client_data, approval_device_read_skew, + ReadAuthentication, decode_read_request, PushUpdateRequest, decode_push_update_request, push_update_json, + EnrolmentRequest, decode_enrolment_request, IosAppAttestAttestation, AndroidKeyAttestationChain, + SignedRedemption, decode_signed_redemption, IosAppAttestAssertion, AndroidDecisionKeyOnly, device_redemption_signing_input, + WireDecoded, WireRefused, + EnrolmentGrant, enrolment_grant_json, PendingApproval, pending_list_json, VerbCapability, FetchedRequest, fetched_request_json, + RedemptionChallenge, redemption_challenge_message, enrolment_readback_json, redemption_response_json, + approval_device_pending_path, device_request_path, device_enrollment_path, approval_device_push_path, + decode_path_segment, PathSegmentDecoded, PathSegmentMalformed, PathSegmentNonCanonical, +} +import gunbc.auth.approval_device_redemption { + approval_device_store_root, EnrolmentSlotStanding, EnrolmentCodeConsumed, EnrolmentRevoked, EnrolmentCodeUnspent, EnrolmentCodeUnknown, EnrolmentSlotUnreadable, + VerifiedDeviceEnrollment, IosAttestedAppInstance, AndroidAttestedDecisionKey, + observe_enrolment_slot, observe_enrollment, enrolment_readback_of, issue_enrolment_code, commit_enrolment, + enrolment_admission, EnrolmentAdmitted, EnrolmentRefused, EnrolmentRefusal, + EnrolmentCodeNotIssued, EnrolmentCodeAlreadyUsed, EnrolmentCodeExpired, EnrolmentStoreUnreadable, EnrolmentAttestationRefused, EnrolmentAttestationForOtherBytes, EnrolmentAndroidUnrealized, + DeviceStoreWrite, DeviceStoreWritten, DeviceStoreSlotOccupied, DeviceStoreRefused, + redeem_device_over_store, DeviceRedemptionOutcome, redemption_response_of, DeviceRedeemed, DeviceAlreadyDecided, DeviceLostTheRace, + DeviceEnrollmentUnknown, DeviceEnrollmentRevoked, DeviceEscalationNotFiled, DeviceStoreUnreadable, DeviceKeyringUnavailable, DeviceCommitRefused, + DeviceEnrollmentForAnotherOperator, DeviceSignedForAnotherRequest, DeviceChallengeExpired, DeviceChallengeNotIssuedHere, DeviceCapabilityTagMalformed, + DeviceCapabilityRefused, DeviceSignatureRefused, DevicePlatformProofRefused, DevicePlatformProofForOtherBytes, DevicePlatformProofWrongKey, DevicePlatformUnrealized, +} + +// ── THE SIX DEVICE ROUTES, as folds the broker mounts ──────────────────────────────────────── +// Each fold takes what the serve entry hands a route -- the body, the path suffix where there is +// one, the serving process and the observed instant -- and returns the status and JSON body the +// wire spells. The broker (gunbc.auth.approval_broker_serve) owns routing, markers and the writer +// gate's placement; the redemption and wire modules own every decision; this module is the +// adapter between them and it decides nothing an authority module has not already decided. +// +// EVERY OPERATION IS A POST AND ITS AUTHENTICATION RIDES IN THE BODY (decision msg_5b415336): the +// enrolment POST consumes a code; the redeem POST carries a signature and a platform proof; the +// three reads and the push update carry a ReadAuthentication -- an App Attest assertion over the +// route's framed client data -- and are admitted only for an ACTIVE enrolment inside the skew +// window around the observed instant. +// +// WHAT NO ROUTE HERE DOES: issue an enrolment code (issue_device_enrolment_code below is the +// operator's verb over the SSH edge, never a route), and mint a verified value -- SignatureVerified, +// AttestationVerified, AssertionAuthentic and the admitted enrolment/redemption are minted by the +// seams and folds they belong to, and this module only carries them from the verifier to the +// admission. + +type DeviceRouteResponse { + status: HttpStatus + body: String +} + +fn device_refusal_json(reason: String) -> String { + serialize_json(v: json_object(members: [json_kv(key: "refused", value: json_string(s: reason))])) +} + +fn device_refused(status: HttpStatus, reason: String) -> DeviceRouteResponse { + DeviceRouteResponse { status: status, body: device_refusal_json(reason: reason) } +} + +// The instant every route decides at: the clock probe admitted only as a canonical UTC instant. +fn device_observed_at() -> Timestamp? { + match clock_now_probed_at() { + Absent => none + Present { value: t } => if utc_instant_is_canonical(t: t as Timestamp) { Present { value: t as Timestamp } } else { none } + } +} + +// THE INSTANT IS PROBED ONCE PER REQUEST, and a probe that is not a canonical UTC instant refuses +// the request rather than deciding under an unknown time. +fn device_clock_refused() -> DeviceRouteResponse { + device_refused(status: 503, reason: "the clock did not answer a canonical UTC instant") +} + +fn device_instant_plus(t: Timestamp, s: Second) -> Timestamp { + Clock.TimestampAdd(timestamp: t, offset: second_count(s: s)).result +} + +// ── The verifier's expectations, from the configuration ────────────────────────────────────── +type VerifierExpectations + = VerifierReady { app_id: NonEmptyStr, config: AppAttestVerifierConfig } + | VerifierUnconfigured { missing: NonEmptyStr } + +fn verifier_expectations() -> VerifierExpectations { + match approval_app_attest_verifier { + AppAttestVerifierAwaitingOperator { missing: m } => VerifierUnconfigured { missing: m } + AppAttestVerifierConfigured { app_id_prefix: _, bundle_id: _, environment: _, admitted_validation_categories: _, expected_bundle_version: _ } => + match approval_app_attest_app_id(c: approval_app_attest_verifier) { + Absent => VerifierUnconfigured { missing: "app id" } + Present { value: app_id } => VerifierReady { app_id: app_id, config: approval_app_attest_verifier } + } + } +} + +fn attestation_expectation_for(app_id: NonEmptyStr, config: AppAttestVerifierConfig, key_id: AttestKeyId, client_data: NonEmptyStr, observed_at: Timestamp) -> AttestationExpectation? { + match config { + AppAttestVerifierAwaitingOperator { missing: _ } => none + AppAttestVerifierConfigured { app_id_prefix: _, bundle_id: _, environment: env, admitted_validation_categories: cats, expected_bundle_version: ver } => + Present { value: AttestationExpectation { key_id: key_id, client_data: client_data, app_id: app_id, environment: env, observed_at: observed_at, admitted_validation_categories: cats, expected_bundle_version: ver } } + } +} + +fn assertion_expectation_for(app_id: NonEmptyStr, config: AppAttestVerifierConfig, key_id: AttestKeyId, public_key_point_b64url: NonEmptyStr, client_data: NonEmptyStr) -> AssertionExpectation? { + match config { + AppAttestVerifierAwaitingOperator { missing: _ } => none + AppAttestVerifierConfigured { app_id_prefix: _, bundle_id: _, environment: _, admitted_validation_categories: cats, expected_bundle_version: ver } => + Present { value: AssertionExpectation { key_id: key_id, public_key_point_b64url: public_key_point_b64url, client_data: client_data, app_id: app_id, admitted_validation_categories: cats, expected_bundle_version: ver } } + } +} + +// The App Attest assertion for an enrolment's evidence over given client data: the verifier's +// verdict, or a refusal minted through the seam when the object does not decode as base64 or the +// enrolment is not an iOS one. +fn assertion_for_enrollment(enrollment: VerifiedDeviceEnrollment, assertion_b64: NonEmptyStr, client_data: NonEmptyStr, app_id: NonEmptyStr, config: AppAttestVerifierConfig) -> AssertionVerification { + match enrollment.evidence { + AndroidAttestedDecisionKey => AssertionRefused { cause: AssertionUndecodable { cause: "no assertion verifier for an Android enrolment" } } + IosAttestedAppInstance { attest_key_id: k, attest_public_key_b64url: pk, receipt_b64: _ } => + match base64_decode(s: assertion_b64 as String, variant: Standard) { + Absent => AssertionRefused { cause: AssertionUndecodable { cause: "assertion_b64 is not base64" } } + Present { value: object } => + match assertion_expectation_for(app_id: app_id, config: config, key_id: k, public_key_point_b64url: pk, client_data: client_data) { + Absent => AssertionRefused { cause: AssertionUndecodable { cause: "verifier unconfigured" } } + Present { value: e } => verify_assertion(object: object, e: e) + } + } + } +} + +// ── Authenticated reads ────────────────────────────────────────────────────────────────────── +type DeviceReadAdmission + = DeviceReadAdmitted { enrollment: VerifiedDeviceEnrollment } + | DeviceReadRefused { status: HttpStatus, reason: String } + +// The window is closed below and open above, in whole seconds from the observed instant: a pure +// comparison over gunbc.auth.approval_capability utc_instant_seconds_after, so no clock call and no +// negative offset handed to a Nat carrier. Both instants must be canonical; either one failing is +// outside the window. +fn requested_at_within_skew(requested_at: Timestamp, observed_at: Timestamp) -> Bool { + utc_instant_is_canonical(t: requested_at) && utc_instant_is_canonical(t: observed_at) + && seconds_within_half_open_window(d: utc_instant_seconds_after(later: requested_at, earlier: observed_at), w: second_count(s: approval_device_read_skew) as Int) +} + +fn seconds_within_half_open_window(d: Int, w: Int) -> Bool { + d >= 0 - w && d < w +} + +// ADMISSION OF A READ: a bound native verifier realization, an ACTIVE enrolment named by the body, a +// claimed time inside the skew window, an assertion under that enrolment's App Attest key over +// exactly this route's client data, and that assertion's counter committed past the enrolment's +// standing (gunbc.auth.approval_assertion_counter) BEFORE the operation runs. A revoked or unknown +// enrolment is refused before any verification runs; an unbound realization before anything is read. +// +// THE COUNTER IS WHAT MAKES A CAPTURED ASSERTION SINGLE-USE here: the skew window bounds when a +// read may be presented, not how often, so without the standing a captured authenticated read +// replays inside it -- recovering the fetch response, or, on the push update, rolling the APNs +// registration back to an older token. The redemption POST does NOT consult the standing: its +// replay wall is the server-minted expiring challenge and the one-decision CAS slot of +// redeem_device_over_store, and because Apple's counter is monotonic across the key, a redemption +// that does not advance the standing leaves the reads' strict comparison sound. +fn admit_device_read(realization: DeviceCryptoRealization, auth: ReadAuthentication, client_data: NonEmptyStr, observed_at: Timestamp) -> DeviceReadAdmission { + match device_crypto_admission(r: realization) { + DeviceCryptoRefused { status: st, reason: why } => DeviceReadRefused { status: st, reason: why } + DeviceCryptoAdmitted { handler_identity: _, exact_revision: _ } => admit_device_read_realized(auth: auth, client_data: client_data, observed_at: observed_at) + } +} + +fn admit_device_read_realized(auth: ReadAuthentication, client_data: NonEmptyStr, observed_at: Timestamp) -> DeviceReadAdmission { + match verifier_expectations() { + VerifierUnconfigured { missing: m } => DeviceReadRefused { status: 503, reason: "the App Attest verifier is not configured: " + (m as String) } + VerifierReady { app_id: app_id, config: config } => + match observe_enrollment(root: approval_device_store_root, enrollment_id: auth.enrollment_id) { + EnrolmentCodeUnknown => DeviceReadRefused { status: 404, reason: "no such enrolment" } + EnrolmentCodeUnspent { challenge: _ } => DeviceReadRefused { status: 404, reason: "no such enrolment" } + EnrolmentRevoked { enrollment: _, revoked_at: _, reason: _ } => DeviceReadRefused { status: 403, reason: "the enrolment is revoked" } + EnrolmentSlotUnreadable { detail: d } => DeviceReadRefused { status: 503, reason: d as String } + EnrolmentCodeConsumed { enrollment: e } => + if !requested_at_within_skew(requested_at: auth.requested_at, observed_at: observed_at) { + DeviceReadRefused { status: 403, reason: "requested_at is outside the read skew window" } + } else { + match assertion_for_enrollment(enrollment: e, assertion_b64: auth.assertion_b64, client_data: client_data, app_id: app_id, config: config) { + AssertionRefused { cause: _ } => DeviceReadRefused { status: 403, reason: "the read assertion did not verify" } + AssertionAuthentic { authentic: a } => + if a.client_data != client_data { DeviceReadRefused { status: 403, reason: "the read assertion covers other bytes" } } + else { + match admit_assertion_counter(root: approval_assertion_counter_root, enrollment_id: e.enrollment_id, observed: a.counter) { + AssertionCounterAdmitted { enrollment_id: _, counter: _ } => DeviceReadAdmitted { enrollment: e } + refused => DeviceReadRefused { status: assertion_counter_refusal_status(a: refused), reason: assertion_counter_refusal_reason(a: refused) } + } + } + } + } + } + } +} + +// ── POST /approve/device/enrol ─────────────────────────────────────────────────────────────── +fn enrolment_refusal_status(r: EnrolmentRefusal) -> HttpStatus { + match r { + EnrolmentCodeNotIssued => 403 + EnrolmentCodeAlreadyUsed => 409 + EnrolmentCodeExpired { expires_at: _, observed_at: _ } => 403 + EnrolmentStoreUnreadable { detail: _ } => 503 + EnrolmentAttestationRefused { cause: _ } => 403 + EnrolmentAttestationForOtherBytes => 403 + EnrolmentAndroidUnrealized => 501 + } +} + +fn enrolment_refusal_reason(r: EnrolmentRefusal) -> String { + match r { + EnrolmentCodeNotIssued => "the code was not issued" + EnrolmentCodeAlreadyUsed => "the code was already consumed" + EnrolmentCodeExpired { expires_at: x, observed_at: _ } => "the code expired at " + x + EnrolmentStoreUnreadable { detail: d } => d as String + EnrolmentAttestationRefused { cause: _ } => "the attestation did not verify" + EnrolmentAttestationForOtherBytes => "the attestation covers other bytes" + EnrolmentAndroidUnrealized => "Android enrolment is not realized" + } +} + +fn attestation_for_request(r: EnrolmentRequest, app_id: NonEmptyStr, config: AppAttestVerifierConfig, observed_at: Timestamp) -> AttestationVerification { + match r.evidence { + AndroidKeyAttestationChain { chain: _ } => AttestationRefused { cause: AttestationUndecodable { cause: "no attestation verifier for Android" } } + IosAppAttestAttestation { attest_key_id: k, attestation_b64: b } => + match base64_decode(s: b as String, variant: Standard) { + Absent => AttestationRefused { cause: AttestationUndecodable { cause: "attestation_b64 is not base64" } } + Present { value: object } => + match attestation_expectation_for(app_id: app_id, config: config, key_id: k, client_data: enrolment_transcript(code: r.code, decision_key: r.decision_key, platform: r.platform), observed_at: observed_at) { + Absent => AttestationRefused { cause: AttestationUndecodable { cause: "verifier unconfigured" } } + Present { value: e } => verify_attestation(object: object, e: e) + } + } + } +} + +// THE PUSH REGISTRATION HAS ITS OWN ROOT. gunbc.durable_cas_file_store owns both directions of the +// layout under approval_device_store_root (review 69827 of gunbc#12000), so a record that is not a +// CAS generation does not live there: it is a last-write-wins owner-only file under a sibling root +// this module owns, keyed by the server-derived enrolment id (never a request-supplied string -- +// both writers pass the verified enrolment's id). +data approval_device_push_root: NonEmptyStr = "/var/lib/gunbc/approval-device-push" + +fn push_registration_path(enrollment_id: NonEmptyStr) -> String { + (approval_device_push_root as String) + "/" + (enrollment_id as String) + ".json" +} + +// WRITTEN BY TWO ROUTES, READ BY A CONSUMER THAT DOES NOT EXIST YET, and the frontier is declared +// beside the write rather than left for the reader to infer (DESIGN section 3c). Nothing in this +// corpus sends an APNs push: the consumer is the push sender that wakes the phone when a request is +// filed (gunbc.auth.approval_request_submission notify_filed is where it attaches), loading this +// record by the pending request's operator enrolment. It cannot land before the operator creates an +// APNs authentication key (Apple Developer > Keys) and it reaches srv1 as a secret; until then the +// app polls its pending list on the authenticated read route, which needs no registration. +data approval_device_push_sender_frontier: DissolutionCondition = unbound_dissolution( + description: "an APNs push sender bound at notify_filed that loads the operator's push registration from approval_device_push_root by enrolment id and sends the wakeup with the operator-created APNs key held on srv1 -- SUFFICIENT FOR a filed request to wake the enrolled phone without polling; until it lands the registration is stored and unread, and the app polls", +) + +fn store_push_registration(enrollment_id: NonEmptyStr, push_json: String) -> DeviceRouteResponse? { + let w = Filesystem.WriteOwnerOnly(path: push_registration_path(enrollment_id: enrollment_id), content: push_json) + if w.success { none } else { Present { value: device_refused(status: 503, reason: "push registration not stored: " + w.error) } } +} + +fn device_enrol_response(body: String, process: ApprovalServingProcess) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_enrol_response_at(realization: approval_device_crypto_realization, body: body, process: process, observed_at: now) + } +} + +fn device_enrol_response_at(realization: DeviceCryptoRealization, body: String, process: ApprovalServingProcess, observed_at: Timestamp) -> DeviceRouteResponse { + match approval_write_admission(asker: process) { + ApprovalWriteRefused { holder: h, asker: a } => device_refused(status: 503, reason: approval_write_refusal_reason(holder: h, asker: a) as String) + ApprovalWriteAdmitted { writer: _ } => + match decode_enrolment_request(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "enrolment request refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: r } => + match device_crypto_admission(r: realization) { + DeviceCryptoRefused { status: st, reason: why } => device_refused(status: st, reason: why) + DeviceCryptoAdmitted { handler_identity: _, exact_revision: _ } => + match verifier_expectations() { + VerifierUnconfigured { missing: m } => device_refused(status: 503, reason: "the App Attest verifier is not configured: " + (m as String)) + VerifierReady { app_id: app_id, config: config } => { + let slot = observe_enrolment_slot(root: approval_device_store_root, code: r.code) + let attestation = attestation_for_request(r: r, app_id: app_id, config: config, observed_at: observed_at) + match enrolment_admission(slot: slot, platform: r.platform, decision_key: r.decision_key, attestation: attestation, observed_at: observed_at) { + EnrolmentRefused { cause: c } => device_refused(status: enrolment_refusal_status(r: c), reason: enrolment_refusal_reason(r: c)) + EnrolmentAdmitted { enrollment: e } => + match commit_enrolment(root: approval_device_store_root, admitted: EnrolmentAdmitted { enrollment: e }) { + DeviceStoreSlotOccupied => device_refused(status: 409, reason: "the code was consumed concurrently") + DeviceStoreRefused { detail: d } => device_refused(status: 503, reason: d as String) + DeviceStoreWritten => + match store_push_registration(enrollment_id: e.enrollment_id, push_json: push_update_json(p: r.push)) { + Present { value: refused } => refused + Absent => DeviceRouteResponse { status: 200, body: enrolment_grant_json(g: EnrolmentGrant { enrollment_id: e.enrollment_id }) } + } + } + } + } + } + } + } + } +} + +// ── POST /approve/device/redeem ────────────────────────────────────────────────────────────── +// EXHAUSTIVE over the closed outcome (review 69672 of gunbc#12000: a wildcard let a new arm inherit +// 403 silently and made the claim over this map non-discriminating). A new outcome is a compile +// refusal here until someone says what it answers. +fn redemption_status(o: DeviceRedemptionOutcome) -> HttpStatus { + match o { + DeviceRedeemed { decision: _ } => 200 + DeviceAlreadyDecided { decision: _ } => 200 + DeviceEnrollmentUnknown => 404 + DeviceEnrollmentRevoked { enrollment_id: _ } => 403 + DeviceEnrollmentForAnotherOperator { enrolled: _, expected: _ } => 403 + DeviceEscalationNotFiled { escalation_id: _ } => 404 + DeviceStoreUnreadable { detail: _ } => 503 + DeviceKeyringUnavailable { cause: _ } => 503 + DeviceSignedForAnotherRequest { field: _ } => 403 + DeviceChallengeExpired { expires_at: _, observed_at: _ } => 403 + DeviceChallengeNotIssuedHere => 403 + DeviceCapabilityTagMalformed => 400 + DeviceCapabilityRefused { cause: _ } => 403 + DeviceSignatureRefused { verification: _ } => 403 + DevicePlatformProofRefused { cause: _ } => 403 + DevicePlatformProofForOtherBytes => 403 + DevicePlatformProofWrongKey => 403 + DevicePlatformUnrealized => 501 + DeviceLostTheRace => 409 + DeviceCommitRefused { detail: _ } => 503 + } +} + +// The signature verdict for a redemption: the seam's verdict under the enrolment's decision key +// over exactly the signing input's framed bytes. With no active enrolment there is no key to +// verify under, and the fold refuses on the slot before it reads this value; SignatureInvalid is +// the honest carrier for "not verified", never a success. +fn redemption_signature(slot: EnrolmentSlotStanding, r: SignedRedemption) -> SignatureVerification { + match slot { + EnrolmentCodeConsumed { enrollment: e } => verify_signature(key: e.decision_key, signature: r.signature, message: device_redemption_signing_input(i: r.signing_input)) + _ => SignatureInvalid { suite: EcdsaP256Sha256 } + } +} + +fn redemption_assertion(slot: EnrolmentSlotStanding, r: SignedRedemption, app_id: NonEmptyStr, config: AppAttestVerifierConfig) -> AssertionVerification { + match slot { + EnrolmentCodeConsumed { enrollment: e } => + match r.platform_proof { + AndroidDecisionKeyOnly => AssertionRefused { cause: AssertionUndecodable { cause: "no platform proof verifier for Android" } } + IosAppAttestAssertion { assertion_b64: b } => assertion_for_enrollment(enrollment: e, assertion_b64: b, client_data: device_redemption_signing_input(i: r.signing_input), app_id: app_id, config: config) + } + _ => AssertionRefused { cause: AssertionUndecodable { cause: "no active enrolment" } } + } +} + +fn device_redeem_response(body: String, process: ApprovalServingProcess) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_redeem_response_at(realization: approval_device_crypto_realization, body: body, process: process, observed_at: now) + } +} + +fn device_redeem_response_at(realization: DeviceCryptoRealization, body: String, process: ApprovalServingProcess, observed_at: Timestamp) -> DeviceRouteResponse { + match approval_write_admission(asker: process) { + ApprovalWriteRefused { holder: h, asker: a } => device_refused(status: 503, reason: approval_write_refusal_reason(holder: h, asker: a) as String) + ApprovalWriteAdmitted { writer: _ } => + match decode_signed_redemption(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "redemption refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: r } => + match device_crypto_admission(r: realization) { + DeviceCryptoRefused { status: st, reason: why } => device_refused(status: st, reason: why) + DeviceCryptoAdmitted { handler_identity: _, exact_revision: _ } => + match verifier_expectations() { + VerifierUnconfigured { missing: m } => device_refused(status: 503, reason: "the App Attest verifier is not configured: " + (m as String)) + VerifierReady { app_id: app_id, config: config } => { + let slot = observe_enrollment(root: approval_device_store_root, enrollment_id: r.signing_input.enrollment_id) + let outcome = redeem_device_over_store( + root: approval_decision_store_root, + keyring: read_approval_keyring(), + enrolment: slot, + signed: r.signing_input, + signature: redemption_signature(slot: slot, r: r), + assertion: redemption_assertion(slot: slot, r: r, app_id: app_id, config: config), + observed_at: observed_at, + ) + DeviceRouteResponse { status: redemption_status(o: outcome), body: redemption_response_json(r: redemption_response_of(o: outcome)) } + } + } + } + } + } +} + +// ── POST /approve/device/pending ───────────────────────────────────────────────────────────── +fn device_pending_response(body: String) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_pending_response_at(realization: approval_device_crypto_realization, body: body, observed_at: now) + } +} + +fn device_pending_response_at(realization: DeviceCryptoRealization, body: String, observed_at: Timestamp) -> DeviceRouteResponse { + match decode_read_request(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "read refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: auth } => + match admit_device_read(realization: realization, auth: auth, client_data: device_read_client_data(path: approval_device_pending_path, enrollment_id: auth.enrollment_id, requested_at: auth.requested_at), observed_at: observed_at) { + DeviceReadRefused { status: s, reason: r } => device_refused(status: s, reason: r) + DeviceReadAdmitted { enrollment: _ } => + match pending_escalations(root: approval_decision_store_root) { + PendingEscalationsRefused { detail: d } => device_refused(status: 503, reason: d) + PendingEscalationsListed { pending: rows, unreadable: u } => + if count(u) > 0 { device_refused(status: 503, reason: "an escalation slot could not be read: " + join(map(u, x => x as String), ", ")) } + else { DeviceRouteResponse { status: 200, body: pending_list_json(rows: map(rows, r => PendingApproval { escalation_id: r.escalation_id, request_revision: r.request_revision })) } } + } + } + } +} + +// ── POST /approve/device/requests/ ────────────────────────────────────────────────── +data approval_redemption_challenge_window: Second = second(count: 300) + +type ChallengeIssuance + = ChallengeIssued { challenge: RedemptionChallenge } + | ChallengeIssuanceRefused { detail: String } + +// The stateless challenge: the MAC under the capability key over redemption_challenge_message, +// exactly what device_redemption_admission recomputes to check it. +fn issue_redemption_challenge(key: MacKey, request: StoredApprovalRequest, enrollment_id: NonEmptyStr, observed_at: Timestamp) -> ChallengeIssuance { + let expires_at = device_instant_plus(t: observed_at, s: approval_redemption_challenge_window) + match mac_sign(key: key, message: redemption_challenge_message(escalation_id: request.escalation_id, request_revision: request.request_revision, enrollment_id: enrollment_id, expires_at: expires_at)) { + MacKeyMaterialNotHex { key_id: _ } => ChallengeIssuanceRefused { detail: "the capability key material is not hex" } + MacSigned { tag: t } => ChallengeIssued { challenge: RedemptionChallenge { expires_at: expires_at, nonce_hex: t.hex } } + } +} + +fn verb_capability_for(key: MacKey, request: StoredApprovalRequest, approve: Bool) -> VerbCapability? { + let claims = claims_for(request: request, decision: if approve { ProposeApprove } else { ProposeDeny }) + match issue_capability(claims: claims, key: key) { + CapabilityIssuanceRefused { cause: _ } => none + CapabilityIssued { capability: c } => Present { value: VerbCapability { capability_text: approval_capability_signing_input(c: claims), capability_tag_b64url: c.tag_b64url } } + } +} + +fn device_request_response(body: String, segment: String) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_request_response_at(realization: approval_device_crypto_realization, body: body, segment: segment, observed_at: now) + } +} + +fn device_request_response_at(realization: DeviceCryptoRealization, body: String, segment: String, observed_at: Timestamp) -> DeviceRouteResponse { + match decode_path_segment(presented: segment) { + PathSegmentMalformed { cause: c } => device_refused(status: 400, reason: "request path: " + (c as String)) + PathSegmentNonCanonical { presented: _, canonical: _ } => device_refused(status: 400, reason: "request path segment is not canonical") + PathSegmentDecoded { identity: escalation_id } => + match decode_read_request(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "read refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: auth } => + match admit_device_read(realization: realization, auth: auth, client_data: device_read_client_data(path: device_request_path(escalation_id: escalation_id), enrollment_id: auth.enrollment_id, requested_at: auth.requested_at), observed_at: observed_at) { + DeviceReadRefused { status: s, reason: r } => device_refused(status: s, reason: r) + DeviceReadAdmitted { enrollment: e } => + match observe_escalation(root: approval_decision_store_root, escalation_id: escalation_id) { + EscalationNotFiled => device_refused(status: 404, reason: "no such escalation") + EscalationDecided { decision: _ } => device_refused(status: 409, reason: "the escalation is already decided") + EscalationUnreadable { detail: d } => device_refused(status: 503, reason: d as String) + EscalationPending { request: req } => + match read_approval_keyring() { + ApprovalKeyringRefused { cause: _ } => device_refused(status: 503, reason: "the capability keyring is unavailable") + ApprovalKeyLoaded { key: key } => + match issue_redemption_challenge(key: key, request: req, enrollment_id: e.enrollment_id, observed_at: observed_at) { + ChallengeIssuanceRefused { detail: d } => device_refused(status: 503, reason: d) + ChallengeIssued { challenge: ch } => + match verb_capability_for(key: key, request: req, approve: true) { + Absent => device_refused(status: 503, reason: "the approve capability could not be issued") + Present { value: approve } => + match verb_capability_for(key: key, request: req, approve: false) { + Absent => device_refused(status: 503, reason: "the deny capability could not be issued") + Present { value: deny } => + DeviceRouteResponse { status: 200, body: fetched_request_json(f: FetchedRequest { + escalation_id: req.escalation_id, request_revision: req.request_revision, + stored_request_text: stored_request_json(r: req) as NonEmptyStr, + challenge: ch, approve: approve, deny: deny, + }) } + } + } + } + } + } + } + } + } +} + +// ── POST /approve/device/enrollments/ ─────────────────────────────────────────────── +// The readback authenticates under the enrolment it asks about, so a revoked enrolment answers +// through the read admission's refusal, and an unknown one is 404 before any verification. +fn device_enrollment_readback_response(body: String, segment: String) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_enrollment_readback_response_at(realization: approval_device_crypto_realization, body: body, segment: segment, observed_at: now) + } +} + +fn device_enrollment_readback_response_at(realization: DeviceCryptoRealization, body: String, segment: String, observed_at: Timestamp) -> DeviceRouteResponse { + match decode_path_segment(presented: segment) { + PathSegmentMalformed { cause: c } => device_refused(status: 400, reason: "enrollment path: " + (c as String)) + PathSegmentNonCanonical { presented: _, canonical: _ } => device_refused(status: 400, reason: "enrollment path segment is not canonical") + PathSegmentDecoded { identity: enrollment_id } => + match decode_read_request(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "read refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: auth } => + if auth.enrollment_id != enrollment_id { device_refused(status: 403, reason: "the read speaks for another enrolment") } + else { + match admit_device_read(realization: realization, auth: auth, client_data: device_read_client_data(path: device_enrollment_path(enrollment_id: enrollment_id), enrollment_id: auth.enrollment_id, requested_at: auth.requested_at), observed_at: observed_at) { + DeviceReadRefused { status: s, reason: r } => device_refused(status: s, reason: r) + DeviceReadAdmitted { enrollment: _ } => + match enrolment_readback_of(standing: observe_enrollment(root: approval_device_store_root, enrollment_id: enrollment_id)) { + Absent => device_refused(status: 404, reason: "no such enrolment") + Present { value: rb } => DeviceRouteResponse { status: 200, body: enrolment_readback_json(r: rb) } + } + } + } + } + } +} + +// ── POST /approve/device/push ──────────────────────────────────────────────────────────────── +fn device_push_update_response(body: String, process: ApprovalServingProcess) -> DeviceRouteResponse { + match device_observed_at() { + Absent => device_clock_refused() + Present { value: now } => device_push_update_response_at(realization: approval_device_crypto_realization, body: body, process: process, observed_at: now) + } +} + +fn device_push_update_response_at(realization: DeviceCryptoRealization, body: String, process: ApprovalServingProcess, observed_at: Timestamp) -> DeviceRouteResponse { + match approval_write_admission(asker: process) { + ApprovalWriteRefused { holder: h, asker: a } => device_refused(status: 503, reason: approval_write_refusal_reason(holder: h, asker: a) as String) + ApprovalWriteAdmitted { writer: _ } => + match decode_push_update_request(text: body) { + WireRefused { at: a, cause: c } => device_refused(status: 400, reason: "push update refused at " + (a as String) + ": " + (c as String)) + WireDecoded { value: r } => + match admit_device_read(realization: realization, auth: r.auth, client_data: device_push_update_client_data(enrollment_id: r.auth.enrollment_id, requested_at: r.auth.requested_at, push: r.push), observed_at: observed_at) { + DeviceReadRefused { status: s, reason: rr } => device_refused(status: s, reason: rr) + DeviceReadAdmitted { enrollment: e } => + match store_push_registration(enrollment_id: e.enrollment_id, push_json: push_update_json(p: r.push)) { + Present { value: refused } => refused + Absent => DeviceRouteResponse { status: 200, body: serialize_json(v: json_object(members: [json_kv(key: "stored", value: json_string(s: e.enrollment_id as String))])) } + } + } + } + } +} + +// ── The operator's verb: issue an enrolment code ───────────────────────────────────────────── +// Run over the fleet SSH administrator edge as the owner of approval_device_store_root, never +// served over HTTP (gunbc.auth.approval_device_redemption: the operator's SSH key is the +// attribution). Eight hex characters of entropy, ten minutes to spend it, printed once. +// +// ITS CONSUMER IS A DECLARED FRONTIER (DESIGN section 3c, with the trigger beside it): in this +// corpus the SSH administrator edge is realized by a FleetConvergeWorkflowMode running on the host +// (gunbc.auth.approval_keyring_converge lands that way), and a mode's step output is a workflow +// log readable by every principal with read access to the repository -- which is the exact +// property the redemption module refuses for an HTTP issuer, since a readable code lets another +// principal enrol its own key under the operator's login inside the window. So the verb is not +// bound to a mode that prints it. TRIGGER: the operator's decision on how the code reaches them +// and no one else (approval_device_enrolment_code_delivery_frontier below) -- the existing private +// operator notification channel, or an SSH session of the operator's own -- after which one +// FleetConvergeWorkflowMode or one documented operator invocation binds this function and +// the routes gain their admitted entry. +data approval_enrolment_code_window: Second = second(count: 600) +data approval_enrolment_code_entropy: ByteSize = byte_size(count: 4) + +fn mint_enrolment_code() -> NonEmptyStr? { + match base64_decode(s: trim(s: Urandom.ReadBytes(count: byte_size_count(b: approval_enrolment_code_entropy)).octets_b64), variant: Standard) { + Absent => none + Present { value: octets } => + if count(octets) != byte_size_count(b: approval_enrolment_code_entropy) { + none + } else { + match base64_octets(values: octets) { + QualifiedOctetsRefused { observed: _ } => none + QualifiedOctetsReady { value: qualified } => Present { value: base16_encode_lower(octets: qualified) as NonEmptyStr } + } + } + } +} + +data approval_device_enrolment_code_delivery_frontier: DissolutionCondition = unbound_dissolution( + description: "an operator-decided delivery of the enrolment code that only the operator can read -- the private operator notification channel gunbc.auth.approval_notification publishes to, or an operator-run SSH invocation -- binding issue_device_enrolment_code as one FleetConvergeWorkflowMode step or one documented operator verb, never a workflow log line -- SUFFICIENT FOR the operator to obtain a code that device_enrol_response will consume, with no other principal able to read it", +) + +fn issue_device_enrolment_code() -> CliWireResponse { + match device_observed_at() { + Absent => CliWireUnprintable { cause: "the clock did not answer a canonical UTC instant" } + Present { value: now } => + match mint_enrolment_code() { + Absent => CliWireUnprintable { cause: "the entropy read did not yield the requested octets" } + Present { value: code } => + match issue_enrolment_code(root: approval_device_store_root, code: code, issued_at: now, expires_at: device_instant_plus(t: now, s: approval_enrolment_code_window)) { + DeviceStoreWritten => CliWirePrintable { bytes: "enrolment code " + (code as String) + " (expires " + device_instant_plus(t: now, s: approval_enrolment_code_window) + ")\n", exit: ExitSuccess } + DeviceStoreSlotOccupied => CliWireUnprintable { cause: "the minted code's slot is already occupied; run again" } + DeviceStoreRefused { detail: d } => CliWireUnprintable { cause: d } + } + } + } +} diff --git a/dag/gunbc/auth/approval_device_wire.dag b/dag/gunbc/auth/approval_device_wire.dag index 8085b746fdc..f4b0c2da6b9 100644 --- a/dag/gunbc/auth/approval_device_wire.dag +++ b/dag/gunbc/auth/approval_device_wire.dag @@ -88,10 +88,11 @@ fn approval_push_custom_keys(h: ApprovalPushHint) -> List { // THE FETCH RETURNS BEARER CAPABILITIES, so it is authenticated, not merely hidden behind an opaque // push. The app proves it is the enrolled app instance with an App Attest assertion (no Face ID -- // reading is not deciding) over a framed read request naming the path, the enrolment and the app's -// claimed time; the server admits it only inside a short skew window and only for an ACTIVE iOS -// enrolment. Residual, stated: the counter is not stored (see PlatformRedemptionProof), so a -// captured read request replays inside its window -- over the tailnet's TLS -- and would disclose a -// capability that, until cutover, the legacy bearer route still honours. Cutover closes it. +// claimed time, carried in the POST body as ReadAuthentication; the server admits it only inside a short skew window and only for an ACTIVE iOS +// enrolment. The skew window bounds WHEN a read may be presented, not how often: a captured read is +// made single-use by the assertion counter, committed per enrolment before the read runs +// (gunbc.auth.approval_assertion_counter; which routes consult it is decided in +// gunbc.auth.approval_device_routes admit_device_read). data approval_device_read_protocol: NonEmptyStr = "gunbc.approval-device-read.v1" as NonEmptyStr data approval_device_read_skew: Second = second(count: 60) @@ -191,12 +192,12 @@ type EnrolmentRequest { } // Per-redemption platform proof. iOS: an App Attest assertion whose client data is EXACTLY the -// signing input. THE ASSERTION COUNTER IS NOT STORED, a stated departure from Apple's recommended -// flow: Apple uses it to refuse replay, and a redemption replay is already refused twice -- the -// challenge is server-minted, expiring and bound to one escalation revision, and the decision slot -// admits one decision per escalation. Storing it would add one CAS generation per approval against -// the store's generation probe bound, for no refusal the route lacks. (Reads are the exception, and -// their residual is stated at device_read_client_data.) +// signing input. The REDEMPTION does not consult the stored assertion counter, deliberately: its replay +// wall is the server-minted, expiring challenge bound to one escalation revision and the one-decision +// slot, and because Apple's counter is monotonic across the key, a redemption that does not advance +// the standing leaves the reads' comparison sound. The counter IS stored and IS the replay wall for +// the reads and the push update (gunbc.auth.approval_assertion_counter, consulted by +// gunbc.auth.approval_device_routes admit_device_read), where that decision is stated. type PlatformRedemptionProof = IosAppAttestAssertion { assertion_b64: NonEmptyStr } | AndroidDecisionKeyOnly @@ -789,12 +790,59 @@ fn redemption_response_json(r: RedemptionResponse) -> String { ])) } -// ── Headers, paths and the two further routes ──────────────────────────────────────────────── -// The three headers an authenticated GET or PUT carries: the enrolment it speaks for, the app's -// claimed time, and the App Attest assertion over the route's framed client data. -data approval_device_enrollment_header: NonEmptyStr = "X-Approval-Enrollment" as NonEmptyStr -data approval_device_requested_at_header: NonEmptyStr = "X-Approval-Requested-At" as NonEmptyStr -data approval_device_assertion_header: NonEmptyStr = "X-Approval-Assertion" as NonEmptyStr +// ── Read authentication, paths and the two further routes ──────────────────────────────────── +// EVERY DEVICE OPERATION IS A POST WHOSE BODY CARRIES ITS AUTHENTICATION (decision msg_5b415336, +// 2026-09-21). An earlier cut carried the enrolment id, the app's claimed time and the App Attest +// assertion as three request headers; `gunbc serve` hands a route exactly one header +// (Tailscale-User-Login) and the v1 seed's purpose standing refuses growing it for the approval +// product, so a header the handler cannot read is a wall that does not exist. The body carrier is +// the SAME framing the assertion covers -- device_read_client_data over the route's path, the +// enrolment and the time -- so moving it off the headers changed no signed byte. +type ReadAuthentication { + enrollment_id: NonEmptyStr + requested_at: Timestamp + assertion_b64: NonEmptyStr +} + +fn read_authentication_json_value(a: ReadAuthentication) -> JsonValue { + json_object(members: [ + json_kv(key: "enrollment_id", value: json_string(s: a.enrollment_id as String)), + json_kv(key: "requested_at", value: json_string(s: a.requested_at)), + json_kv(key: "assertion_b64", value: json_string(s: a.assertion_b64 as String)), + ]) +} + +fn read_authentication_json(a: ReadAuthentication) -> String { + serialize_json(v: read_authentication_json_value(a: a)) +} + +fn decode_read_authentication(v: JsonValue) -> WireDecode { + match wire_object(v: v, at: "auth", allowed: ["enrollment_id", "requested_at", "assertion_b64"]) { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: o } => + match wire_string(obj: o, key: "enrollment_id") { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: enrollment_id } => + match wire_string(obj: o, key: "requested_at") { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: requested_at } => + match wire_string(obj: o, key: "assertion_b64") { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: assertion_b64 } => + WireDecoded { value: ReadAuthentication { enrollment_id: enrollment_id, requested_at: requested_at as Timestamp, assertion_b64: assertion_b64 } } + } + } + } + } +} + +// The body of the three authenticated reads (pending, one request, enrolment readback). +fn decode_read_request(text: String) -> WireDecode { + match parse_json_document(s: text) { + JsonDocumentUnreadable { gap: g } => WireRefused { at: "$", cause: json_document_gap_text(gap: g) as NonEmptyStr } + JsonDocumentParsed { value: v } => decode_read_authentication(v: v) + } +} // THE ENROLMENT ID IS DERIVED FROM THE CODE, so the app knows the id of the enrolment its code // produced even when the POST's answer was lost -- the readback needs nothing the operator must type. @@ -807,9 +855,10 @@ fn enrollment_id_for_code(code: NonEmptyStr) -> NonEmptyStr { // key it just attested, which the server holds only if the enrolment committed. data approval_device_enrollment_path_prefix: NonEmptyStr = "/approve/device/enrollments/" as NonEmptyStr -// PUSH UPDATE: APNs rotates tokens; the app re-registers on every launch and PUTs the token here, +// PUSH UPDATE: APNs rotates tokens; the app re-registers on every launch and POSTs the token here, // without a new enrolment. The token is inside the assertion's client data, so an assertion made -// for one token cannot carry another. +// for one token cannot carry another. The body is { auth, push }: the same read authentication +// beside the registration the client data framed. data approval_device_push_path: NonEmptyStr = "/approve/device/push" as NonEmptyStr data approval_device_push_protocol: NonEmptyStr = "gunbc.approval-device-push.v1" as NonEmptyStr @@ -817,6 +866,41 @@ fn device_push_update_client_data(enrollment_id: NonEmptyStr, requested_at: Time framed(fields: [approval_device_push_protocol as String, approval_device_push_path as String, enrollment_id as String, requested_at, push_update_json(p: push)]) } +type PushUpdateRequest { + auth: ReadAuthentication + push: PushRegistration +} + +fn push_update_request_json(r: PushUpdateRequest) -> String { + serialize_json(v: json_object(members: [ + json_kv(key: "auth", value: read_authentication_json_value(a: r.auth)), + json_kv(key: "push", value: push_registration_json(p: r.push)), + ])) +} + +fn decode_push_update_request(text: String) -> WireDecode { + match parse_json_document(s: text) { + JsonDocumentUnreadable { gap: g } => WireRefused { at: "$", cause: json_document_gap_text(gap: g) as NonEmptyStr } + JsonDocumentParsed { value: v } => + match wire_object(v: v, at: "$", allowed: ["auth", "push"]) { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: o } => + match wire_member(obj: o, key: "auth") { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: av } => + match decode_read_authentication(v: av) { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: auth } => + match decode_push_registration_in(o: o, key: "push") { + WireRefused { at: a, cause: c } => WireRefused { at: a, cause: c } + WireDecoded { value: push } => WireDecoded { value: PushUpdateRequest { auth: auth, push: push } } + } + } + } + } + } +} + // A PATH SEGMENT IS "id-" + base64url(UTF-8(identity)), TOTAL AND INJECTIVE, and never refused: every // identity the store admits has a route. The output is drawn only from the base64url alphabet, "=" // padding and the "id-" prefix, so it carries no percent escape for any layer to decode, cannot be a diff --git a/dag/gunbc/ci/ci_layer_roots.dag b/dag/gunbc/ci/ci_layer_roots.dag index 455da3b2905..2865c7c96af 100644 --- a/dag/gunbc/ci/ci_layer_roots.dag +++ b/dag/gunbc/ci/ci_layer_roots.dag @@ -390,6 +390,10 @@ data excl_local_repo_wet_host_probe_reason: String = "real host-effect execution data excl_local_repo_wet_host_probe_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for shell.PosixCommandV.Check, so observe_host_cli_dependency can be asserted under a fixed mock; then these fns re-enroll as ordinary hermetic discovery rows, drop off local_repo_wet_schedule, and this row deletes") +data excl_local_repo_wet_device_route_store_read_reason: String = "real host-effect execution witness over the App Attest device routes whose one claim is the gate's discriminating control: under a bound realization the read proceeds past device_crypto_admission into the enrolment store's Filesystem.Read (gunbc.auth.approval_device_redemption observe_enrollment over approval_device_store_root), which has no mock_response. The route takes no store as a parameter, so the store cannot be supplied at the claim's interface. The effect is READ-ONLY: nothing is written, no network is reached, and the claim asserts only that the answer is not the realization reason, which holds whether the slot is absent, unreadable or present. So excluded from the discovery corpus and executed by the required floor's local-repo wet lane." + +data excl_local_repo_wet_device_route_store_read_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for Filesystem.Read sufficient for observe_enrollment to be driven under a fixed store, OR the device read routes take their store observation as a supplied value; then the control re-enrolls as an ordinary hermetic discovery row in test.claim.approval_device_routes_witness_test, drops off local_repo_wet_schedule, and this row deletes") + data excl_local_repo_wet_tempdir_write_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for shell.Mktemp.Dir and Filesystem.Write, sufficient for sha256sum_verify_via_shell to be asserted under a fixed mock; then these fns re-enroll as ordinary hermetic discovery rows, drop off local_repo_wet_schedule, and this row deletes") data excl_local_repo_wet_dissolve: DissolutionCondition = unbound_dissolution(description: "mock_response coverage lands for the git plumbing these witnesses reach and the assertions are re-checked under a fixed mock; then the fns re-enroll as ordinary hermetic discovery rows, drop off local_repo_wet_schedule, and this row deletes") @@ -1060,6 +1064,16 @@ data witness_exclusion_frontier: List = [ classification: LocalRepoWetLane, reason: excl_local_repo_wet_tempdir_write_reason, dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "approval_assertion_counter_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_tempdir_write_reason, + dissolution: excl_local_repo_wet_dissolve}, + WitnessExclusionRow { + pattern: "approval_device_routes_wet_witness_test.dag", + classification: LocalRepoWetLane, + reason: excl_local_repo_wet_device_route_store_read_reason, + dissolution: excl_local_repo_wet_device_route_store_read_dissolve}, WitnessExclusionRow { pattern: "durable_exclusive_hold_file_store_wet_witness_test.dag", classification: LocalRepoWetLane, diff --git a/dag/gunbc/compute/attempt_lifecycle.dag b/dag/gunbc/compute/attempt_lifecycle.dag index d26355f3574..f1874880447 100644 --- a/dag/gunbc/compute/attempt_lifecycle.dag +++ b/dag/gunbc/compute/attempt_lifecycle.dag @@ -9,7 +9,7 @@ import std.durable_compare_and_set { CasSlotObservation, CasObservedReadable, CasObservedUnreadable, CasReadableSlot, CasReadableAbsent, CasReadablePresent, CasGeneration, cas_generation_count, cas_unreadable_slot_detail, - CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, + CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, CasGenerationSpaceExhausted, } import gunbc.durable_cas_file_store { CasAttemptAdmission, CasAttemptAdmitted, CasAttemptDigestMismatch, CasAttemptDigestIncomparable, @@ -345,6 +345,7 @@ fn attempt_commit(root: NonEmptyStr, record: AttemptRecord, expected: CasExpecta detail: match c { CasSlotObservationRefused { cause: u } => join(["the attempt store refused the read: ", cas_unreadable_slot_detail(cause: u)], "") CasGenerationPublicationRefused { detail: d } => join(["the attempt store refused the write: ", d as String], "") + CasGenerationSpaceExhausted { head: h } => join(["the attempt store's generation space is exhausted at head ", to_string(value: cas_generation_count(g: h))], "") }, } } diff --git a/dag/gunbc/durable_cas_file_store.dag b/dag/gunbc/durable_cas_file_store.dag index 35268c917ee..a062ad0804a 100644 --- a/dag/gunbc/durable_cas_file_store.dag +++ b/dag/gunbc/durable_cas_file_store.dag @@ -1,15 +1,20 @@ module gunbc.durable_cas_file_store -import std.types { NonEmptyStr, String, Int, Bool } +import std.types { NonEmptyStr, String, Int, Bool, List } +import std.algebra { trim } +import std.decimal { decimal_digits_only } +import std.list { distinct_by_key } import std.content_hash { ContentHash, content_hash_of_value, compare_content_hash, ContentHashEqual, ContentHashDifferent, ContentHashCrossFamilyIncomparable } -import std.durable_compare_and_set { CasAttempt, cas_attempt, CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, CasGeneration, CasSlotVersion, CasReadableAbsent, CasReadablePresent, CasSlotObservation, CasObservedReadable, CasObservedUnreadable, CasUnreadableMalformed, CasUnreadableReadRefused, CasUnreadableObservationBoundExceeded, CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, cas_generation_first, cas_generation_next, cas_generation_count } +import std.durable_compare_and_set { CasAttempt, cas_attempt, CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasExpectation, ExpectSlotAbsent, ExpectSlotGeneration, CasGeneration, CasSlotVersion, CasReadableAbsent, CasReadablePresent, CasSlotObservation, CasObservedReadable, CasObservedUnreadable, CasUnreadableMalformed, CasUnreadableReadRefused, CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, cas_generation_exhausted, cas_generation_first, cas_generation_count, cas_generation_successor, CasSuccessorGeneration, CasSuccessorExhausted } +import std.checked_arithmetic { int_inclusive_max } import extdeps.filesystem.filesystem_io { Filesystem, FilesystemCreateNew, FilesystemCreated, FilesystemCreateTargetOccupied, FilesystemCreateRefused, FilesystemCreateKindUnrecognized, FilesystemExactRead, FilesystemExactPathRead, FilesystemExactPathAbsent, FilesystemExactPathUnreadable, FilesystemExactPathKindUnrecognized, FilesystemFailureKind, filesystem_create_new, filesystem_exact_read, filesystem_failure_kind_name, + filesystem_listing_observation, FilesystemDirectoryListed, FilesystemDirectoryListingRefused, FilesystemDirectorySubjectRefused, filesystem_listing_entry_names, FilesystemEntryAbsent, FilesystemEntryListed, FilesystemEntryPresenceIndeterminate, FilesystemEntrySubjectRefused, - filesystem_entry_presence, filesystem_listing_observation, + filesystem_entry_presence, } data authorization_claim_store_root: NonEmptyStr = "/var/lib/gunbc/authorization-claims" as NonEmptyStr @@ -226,17 +231,66 @@ fn cas_file_slot_path(root: NonEmptyStr, key: NonEmptyStr, generation: CasGenera // HOW THE SLOT IS OBSERVED, AND THE BOUND IS PART OF THE CONTRACT. // -// Generations are contiguous and append-only, so the head is found by probing -// upward from 1 until a generation is absent. That needs only Read, no -// directory listing and no parsing of names back into numbers -- a filesystem -// layout that had to be re-parsed to be understood would be a second identity -// authority beside the key. -// -// THE PROBE IS BOUNDED AND THE BOUND REFUSES RATHER THAN TRUNCATING. Running off -// the end returns a typed refusal, not "the head is wherever I stopped looking": -// a walk that silently reported its own patience as the answer would be the -// bound-shaped closure DESIGN names, where a real number satisfies a question it -// never measured. +// Generations are contiguous and append-only -- a generation N+1 is published only by a writer that +// observed head N, and this store offers no delete -- so presence is a PREFIX of the generation line: +// every generation at or below the head exists and none above it does. The head is therefore the +// boundary of a monotone predicate, and it is found by GALLOPING (read 1, 2, 4, 8 ... until one is +// absent) and then BISECTING between the last present and the first absent generation. The head +// search needs only Read and no parsing of names back into numbers -- a filesystem layout that had to +// be re-parsed to be understood would be a second identity authority beside the key. The one listing +// this store takes is cas_first_generation_absent's, on the single arm where generation 1 reads absent, +// to tell an EMPTY slot from an UNINITIALIZED store; it establishes absence, it never finds a head. +// +// WHY NOT A LINEAR WALK FROM 1, which is what this was. The walk read every superseded generation on +// every observation, so its cost grew with the slot's whole history, and its bound was denominated in +// GENERATIONS: past 4096 of them every observation of the slot refused, permanently, for a slot whose +// head was perfectly well formed. The first consumer that advances a slot once per request -- +// gunbc.auth.approval_assertion_counter, one generation per admitted App Attest assertion -- turned +// that into an availability cliff: an operator phone stopped being able to read after ~4096 admitted +// requests, and only re-enrolment recovered it. Raising the bound would have moved that cliff and +// kept it. Nothing reads a superseded generation -- the interface's fact is the HEAD, and +// std.durable_compare_and_set promises a monotone version, not a history -- so the walk was paying, +// per observation, for information no consumer demands. +// +// WHY THE CHAIN ITSELF STAYS. The chain is not an obligation of the interface; it is THIS +// realization's exclusion mechanism. An in-place conditional overwrite is not honestly available on a +// plain filesystem: rename replaces unconditionally, so a compare-then-rename is a check-then-act race +// that only a lock closes, and flock is exactly the single-host exclusion the interface module exists +// to replace. O_EXCL on a DISTINCT name per generation is what lets the OS decide the race, so the +// generations are the price of the exclusion and are kept. What was an artifact is only the READ. +// +// THE SEARCH IS TOTAL OVER THE WHOLE GENERATION LINE, SO IT HAS NO OBSERVATION BOUND. CasGeneration is +// realized as a machine Int, so the line is 1 ..= int_inclusive_max. The gallop doubles while doubling +// stays inside that range; past half of it, it probes the maximum itself instead of doubling. Every +// step is overflow-free: the doubling is taken only at or below max / 2, and the bisection midpoint +// is lo + (hi - lo) / 2. So an observation reads at most ~2 x 63 generations and ALWAYS answers -- +// absent, a head, or a typed read refusal -- and there is no ProbedBeyondBound arm left to produce. +// The end of the line is a WRITE fact, not a read fact: a head at the maximum is readable, and the +// write that would follow it refuses with CasGenerationSpaceExhausted (std.durable_compare_and_set +// cas_generation_successor), because that head has no successor to publish. +// +// THE CONTRACT IS LINEARIZABILITY: an observation returns the head the slot held AT SOME INSTANT +// DURING THE INVOCATION, not merely some generation that was once committed. It follows from two +// facts this store guarantees. Presence is a prefix (a generation is published only after its +// predecessor was observed, and nothing is deleted), and presence is never retracted. So the head, +// as a function of time, is non-decreasing and moves in steps of exactly one generation. +// +// The search ends with generation h read present at some instant t1 and h+1 read absent at some +// instant t2, both inside the invocation. At t1 the head is at least h. At t2 the head is at most h, +// because h+1 is absent and presence is a prefix. Whichever read came first, the head moves through +// every integer between those two values, so there is an instant between t1 and t2 at which the head +// is exactly h. An empty answer is one read of generation 1 absent, which is the head at that +// instant. The value reported is generation h's content, which is written once and never rewritten. +// test.claim.approval_assertion_counter_wet_witness_test places an append between the search's reads +// and shows the reported head is a real generation and the stale writer is refused by the exclusive +// create. +// +// WHAT THE SEARCH NO LONGER OBSERVES: superseded generations it does not land on. The linear walk +// read every one and would refuse on an unreadable generation below the head; this reads O(log n) of +// them. No consumer reads a superseded generation, so none of this store's answers depends on them. +// A HISTORY-INTEGRITY instrument -- every generation present, readable and well formed -- is +// therefore a separate concern with its own subject, not a side effect of reading the head, and this +// store does not claim to provide it. // // READ CLASSIFICATION IS THE HOST KIND CHANNEL, NEVER THE ERROR TEXT. // filesystem_exact_read already partitions NotFound from PermissionDenied / @@ -248,48 +302,69 @@ type CasSlotProbe = ProbedAbsent | ProbedAbsenceUnestablished { cause: String } | ProbedHead { generation: CasGeneration, value: NonEmptyStr } - | ProbedBeyondBound { bound: Int } | ProbedUnreadable { generation: CasGeneration, kind: FilesystemFailureKind } | ProbedReadKindUnrecognized { generation: CasGeneration, observed: String } -data cas_max_generation_probe: Int = 4096 - -fn cas_probe_from(root: NonEmptyStr, key: NonEmptyStr, generation: CasGeneration, previous: NonEmptyStr) -> CasSlotProbe { - if cas_generation_count(g: generation) > cas_max_generation_probe { - ProbedBeyondBound { bound: cas_max_generation_probe } - } else { - let path = cas_file_slot_path(root: root, key: key, generation: generation) - let read = Filesystem.Read(path: path) - cas_probe_from_exact( - root: root, - key: key, - generation: generation, - previous: previous, - exact: filesystem_exact_read(path: path, content: read.content, success: read.success, error: read.error, error_kind: read.error_kind), - ) - } +// One generation read, classified: present with its content, absent, or a typed refusal. +type CasGenerationRead + = GenerationPresent { content: NonEmptyStr } + | GenerationAbsent + | GenerationRefused { probe: CasSlotProbe } + +fn cas_read_generation(root: NonEmptyStr, key: NonEmptyStr, generation: CasGeneration) -> CasGenerationRead { + let path = cas_file_slot_path(root: root, key: key, generation: generation) + let read = Filesystem.Read(path: path) + cas_classify_generation_read( + generation: generation, + exact: filesystem_exact_read(path: path, content: read.content, success: read.success, error: read.error, error_kind: read.error_kind), + ) } -fn cas_probe_from_exact( - root: NonEmptyStr, - key: NonEmptyStr, - generation: CasGeneration, - previous: NonEmptyStr, - exact: FilesystemExactRead, -) -> CasSlotProbe { +fn cas_classify_generation_read(generation: CasGeneration, exact: FilesystemExactRead) -> CasGenerationRead { match exact { - FilesystemExactPathRead { path: _, content: c } => - cas_probe_from(root: root, key: key, generation: cas_generation_next(g: generation), previous: c as NonEmptyStr) - FilesystemExactPathAbsent { path: _ } => - if cas_generation_count(g: generation) == 1 { - cas_first_generation_absent(root: root, key: key) - } else { - ProbedHead { generation: cas_generation_count(g: generation) - 1, value: previous } - } + FilesystemExactPathRead { path: _, content: c } => GenerationPresent { content: c as NonEmptyStr } + FilesystemExactPathAbsent { path: _ } => GenerationAbsent FilesystemExactPathUnreadable { path: _, kind: k, error: _ } => - ProbedUnreadable { generation: generation, kind: k } + GenerationRefused { probe: ProbedUnreadable { generation: generation, kind: k } } FilesystemExactPathKindUnrecognized { path: _, observed: o, error: _ } => - ProbedReadKindUnrecognized { generation: generation, observed: o } + GenerationRefused { probe: ProbedReadKindUnrecognized { generation: generation, observed: o } } + } +} + +// INVARIANT: `present` was read present. Double until a generation reads absent; past half of the +// Int range, probe the maximum instead of doubling, so no step overflows. +fn cas_probe_gallop(root: NonEmptyStr, key: NonEmptyStr, present: CasGeneration, present_value: NonEmptyStr) -> CasSlotProbe { + let p = cas_generation_count(g: present) + if p >= int_inclusive_max() { + ProbedHead { generation: present, value: present_value } + } else { + let next = if p <= int_inclusive_max() / 2 { p * 2 } else { int_inclusive_max() } + match cas_read_generation(root: root, key: key, generation: next) { + GenerationRefused { probe: r } => r + GenerationPresent { content: c } => + cas_probe_gallop(root: root, key: key, present: next, present_value: c) + GenerationAbsent => + cas_probe_bisect(root: root, key: key, present: present, present_value: present_value, absent: next) + } + } +} + +// INVARIANT: `present` read present, `absent` read absent, present < absent. The head is the last +// present generation, reached when the two are adjacent. +fn cas_probe_bisect(root: NonEmptyStr, key: NonEmptyStr, present: CasGeneration, present_value: NonEmptyStr, absent: CasGeneration) -> CasSlotProbe { + let lo = cas_generation_count(g: present) + let hi = cas_generation_count(g: absent) + if hi - lo <= 1 { + ProbedHead { generation: present, value: present_value } + } else { + let mid = lo + (hi - lo) / 2 + match cas_read_generation(root: root, key: key, generation: mid) { + GenerationRefused { probe: p } => p + GenerationPresent { content: c } => + cas_probe_bisect(root: root, key: key, present: mid, present_value: c, absent: absent) + GenerationAbsent => + cas_probe_bisect(root: root, key: key, present: present, present_value: present_value, absent: mid) + } } } @@ -326,7 +401,13 @@ fn cas_absence_unestablished(cause: String) -> CasUnreadableSlot { } fn cas_observe_slot(root: NonEmptyStr, key: NonEmptyStr) -> CasSlotProbe { - cas_probe_from(root: root, key: key, generation: cas_generation_first(), previous: "unread" as NonEmptyStr) + let first = cas_generation_first() + match cas_read_generation(root: root, key: key, generation: first) { + GenerationRefused { probe: p } => p + GenerationAbsent => cas_first_generation_absent(root: root, key: key) + GenerationPresent { content: c } => + cas_probe_gallop(root: root, key: key, present: first, present_value: c) + } } // THE PROJECTION TAKES A HEAD, NOT A PROBE, AND THE DELETED ARM IS THE REPAIR. @@ -352,12 +433,6 @@ fn cas_head_as_readable(generation: CasGeneration, value: NonEmptyStr) -> CasRea } } -// ONE AUTHORITY FOR WHAT BOUND EXHAUSTION IS. Three sites spelled it independently, twice as a -// malformed head, and a fourth spelling would have arrived with the next caller. -fn cas_slot_observation_bound_exceeded(bound: Int) -> CasUnreadableSlot { - CasUnreadableObservationBoundExceeded { bound: bound } -} - // AN UNREADABLE GENERATION IS A SLOT-OBSERVATION REFUSAL, NEVER AN ABSENT SLOT. // // gunbc#11335 made the probe read through the host's failure kind, so a generation that exists and @@ -386,8 +461,6 @@ fn cas_generation_read_kind_unrecognized(generation: CasGeneration, observed: St fn cas_probe_as_observation(probe: CasSlotProbe) -> CasSlotObservation { match probe { - ProbedBeyondBound { bound: b } => - CasObservedUnreadable { cause: cas_slot_observation_bound_exceeded(bound: b) } ProbedUnreadable { generation: g, kind: k } => CasObservedUnreadable { cause: cas_generation_unreadable(generation: g, kind: k) } ProbedReadKindUnrecognized { generation: g, observed: o } => @@ -413,10 +486,24 @@ fn cas_probe_as_observation(probe: CasSlotProbe) -> CasSlotObservation CasSlotObservation { - cas_probe_as_observation(probe: cas_observe_slot(root: root, key: key)) + if !cas_key_is_slot_addressable(key: key) { + CasObservedUnreadable { cause: CasUnreadableReadRefused { detail: cas_key_not_slot_addressable_detail } } + } else { + cas_probe_as_observation(probe: cas_observe_slot(root: root, key: key)) + } } +data cas_key_not_slot_addressable_detail: NonEmptyStr = "key is not slot-addressable: it carries a path separator" + + // ACCESS MODE AND CONDITIONAL PUBLICATION ARE TWO FACTS, AND THIS STORE HELD THEM AS ONE. // // Every generation was published with `Filesystem.WriteOwnerOnly`, so one operation decided both @@ -630,7 +717,6 @@ fn cas_owner_only_failed_publication( } ProbedAbsent => cas_publication_refused(detail: detail) ProbedAbsenceUnestablished { cause: c } => CasStoreRefused { cause: CasSlotObservationRefused { cause: cas_absence_unestablished(cause: c) } } - ProbedBeyondBound { bound: b } => cas_publication_beyond_bound(bound: b) ProbedUnreadable { generation: g, kind: k } => CasStoreRefused { cause: CasSlotObservationRefused { cause: cas_generation_unreadable(generation: g, kind: k) } } ProbedReadKindUnrecognized { generation: g, observed: o } => @@ -640,36 +726,6 @@ fn cas_owner_only_failed_publication( } } -// THE BOUND ARM CANNOT SAY THE STORE REFUSED TO PUBLISH, AND A FIRST CUT SAID IT ANYWAY. -// -// It routed `ProbedBeyondBound` to the publication refusal along with the other two, on the reasoning -// that the write had failed and the target had not appeared. The second half does not follow. Consider -// a slot whose head is 4095 and two writers targeting 4096: -// -// the other writer wins 4096; this writer's create fails -// the re-observation reads 4096 successfully and probes 4097 -// 4097 exceeds the bound, so the probe answers ProbedBeyondBound -// -// Another writer DID publish. Reporting a publication refusal there invents the wrong cause -- the -// same fabrication the lost-race repair one screen up exists to remove, reappearing in the arm that -// repair did not consider. Found by external review. -// -// SO THIS ANSWERS WHAT IS ACTUALLY KNOWN: the slot could not be observed. It is a slot-observation -// refusal, not a publication refusal and not a precondition failure, because the probe no longer holds -// a readable head to report as the winner. The ordinary two-writer control runs far below the bound -// and cannot discriminate this arm, so it has its own control. -// -// AND THE CAUSE IS BOUND EXHAUSTION, NOT A MALFORMED HEAD, which the first version of this repair got -// wrong in the other direction: it stopped claiming the publication failed and then said the slot's -// contents were garbage. A slot holding 4096 contiguous, perfectly well formed generations is not -// malformed, and telling an operator it is sends them to repair bytes that are fine. Found by external -// review, on this function's own repair. -fn cas_publication_beyond_bound(bound: Int) -> CasOutcome { - CasStoreRefused { - cause: CasSlotObservationRefused { cause: cas_slot_observation_bound_exceeded(bound: bound) } - } -} - fn cas_publication_refused(detail: String) -> CasOutcome { CasStoreRefused { cause: CasGenerationPublicationRefused { detail: detail as NonEmptyStr } @@ -691,10 +747,6 @@ fn file_compare_and_set( let attempt = verified.attempt let probe = cas_observe_slot(root: root, key: attempt.key) match probe { - ProbedBeyondBound { bound: b } => - CasStoreRefused { - cause: CasSlotObservationRefused { cause: cas_slot_observation_bound_exceeded(bound: b) } - } ProbedUnreadable { generation: g, kind: k } => CasStoreRefused { cause: CasSlotObservationRefused { cause: cas_generation_unreadable(generation: g, kind: k) } } ProbedReadKindUnrecognized { generation: g, observed: o } => @@ -721,15 +773,66 @@ fn file_compare_and_set( CasPreconditionFailed { expected: attempt.expected, observed: cas_head_as_readable(generation: h, value: v) } ExpectSlotGeneration { generation: g } => if cas_generation_count(g: g) == cas_generation_count(g: h) { - cas_commit_at( - admitted: AdmittedCasPublication { - root: root, publication: publication, attempt: attempt, - target: cas_generation_next(g: h), - } - ) + match cas_generation_successor(g: h) { + CasSuccessorExhausted { head: last } => cas_generation_exhausted(head: last) + CasSuccessorGeneration { generation: next } => + cas_commit_at( + admitted: AdmittedCasPublication { + root: root, publication: publication, attempt: attempt, + target: next, + } + ) + } } else { CasPreconditionFailed { expected: attempt.expected, observed: cas_head_as_readable(generation: h, value: v) } } } } } + +// ── Which slots exist ──────────────────────────────────────────────────────────────────────── +// THE STORE OWNS BOTH DIRECTIONS OF ITS LAYOUT. cas_file_slot_path renders "/.", so +// the inverse over a directory listing strips exactly one trailing "." -- the generation +// is always the LAST dotted component and always numeric, so a key that itself contains "." reads +// back unchanged. This is the one place a name is parsed back into a key, beside the function +// that made the name; a consumer that split file names itself would be the second identity +// authority the head-probe note above refuses. The listing answers WHICH keys have a slot; each +// key's standing is still read through observe_cas_slot_state. +type CasSlotKeys + = CasSlotKeysListed { keys: List } + | CasSlotKeysListingRefused { root: NonEmptyStr, detail: String } + | CasSlotKeysSubjectRefused { root: NonEmptyStr, cause: String } + +fn cas_name_is_digits(s: String) -> Bool { + s != "" && decimal_digits_only(s: s) +} + +// "." -> key, or none for a name that is not a slot file. +fn cas_key_of_slot_name(name: String) -> NonEmptyStr? { + let parts = name.split(delimiter: ".") + if count(parts) < 2 { none } else { + let last = match parts |> get(count(parts) - 1) { + null => "" + p => p + } + if !cas_name_is_digits(s: last) { none } else { + let key = join(parts |> take(count(parts) - 1), ".") + if key == "" { none } else { Present { value: key as NonEmptyStr } } + } + } +} + +fn cas_slot_keys(root: NonEmptyStr) -> CasSlotKeys { + let listing = Filesystem.List(path: root as String) + match filesystem_listing_observation(directory: root as String, success: listing.success, entries: listing.entries, error: listing.error) { + FilesystemDirectorySubjectRefused { directory: _, cause: c } => CasSlotKeysSubjectRefused { root: root, cause: c } + FilesystemDirectoryListingRefused { directory: _, error: e } => CasSlotKeysListingRefused { root: root, detail: e } + FilesystemDirectoryListed(listed) => { + let keys = fold(filesystem_listing_entry_names(listing: listed), init: [], f: (acc, n) => match cas_key_of_slot_name(name: trim(s: n)) { + Absent => acc + Present { value: k } => acc |> list_push(k) + }) + CasSlotKeysListed { keys: distinct_by_key(xs: keys, key: fn(k) { k as String }) } + } + } +} diff --git a/dag/gunbc/explicit_witness_admission.dag b/dag/gunbc/explicit_witness_admission.dag index 443f016f859..320ad0ea142 100644 --- a/dag/gunbc/explicit_witness_admission.dag +++ b/dag/gunbc/explicit_witness_admission.dag @@ -473,6 +473,14 @@ data explicit_witness_admissions: List = [ reason: "Admitted RED whose cited boundary NO LONGER EXISTS: gunbc#10245 replaced the witness entry import closure with a caller-declared pool, so the population is exactly origin_probe_subject_files, and run_direct_rust_door_emit_write_compile_smoke lives in dag/test/claim/direct_rust_door_write_compile_witness_test.dag, which that subject does not name. The cause is the declared subject and is decidable by reading it; it is neither the marshal nor the reachability horizon. Owner: witness-evidence-lifecycle lane.", dissolution: unbound_dissolution(description: "a population authority enumerates fn-arrow declarations repository-wide within this lane's budget, so the direct-door smoke declaration is in the probe's subject without the witness naming its file one by one; this witness greens and this row deletes. Naming that one file in origin_probe_subject_files would also green it and is NOT the trigger: it would green the row without the capability the row stands for") ), + known_red_probe( + entry: "dag/test/claim/file_hold_plan_refusal_probe_witness_test.dag", + f: "the_harness_runs_and_a_clean_source_over_the_hold_store_is_clean", + kind: CorpusWitnessKind, + budget: FastLaneEvalBudget, + reason: "RED ON THIS STACK FOR A MAIN-WIDE COMPILER DEFECT, NOT FOR THE HOLD STORE. The claim asserts a census of the hold-store harness has zero blocking rows. Bisected to 9945e9268f1 (its parent is clean): cas_slot_keys began importing std.decimal, whose closure reaches std.measure through std.bytes and std.integer, and the census's measured compile (gunbc.type_ref_hit_ne_bind_measure) charges std.measure's own unit variants, passed as phantom type arguments in Measure, as missing imports -- 38 blocking UnresolvedType rows here, and 147 for a source importing std.measure alone on plain main. The unmeasured resolve admits the same leaves, so the two routes of one compiler disagree; the measure is the wrong side. Kept enrolled rather than deleted or loosened: it is the discriminating red that shows the census is not yet fit for any closure reaching std.measure.", + dissolution: unbound_dissolution(description: "the measured compile's binding authority (v1.compiler.infer_env type_ref_measure_binding_authority) treats a zero-payload variant as bound exactly when the observed unit_variant_index keys it, and its regenerated stage0 mirror is what claim_batch executes -- SUFFICIENT FOR a census whose closure reaches std.measure to report zero blocking UnresolvedType rows for std.measure's own unit variants. Delivered by gunbc#12132; this row deletes when #12132 is merged into this branch and the claim reads green."), + ), source_root_ingest_gate_admitted_witness( entry: "src/v2/test/claim/self_host/compiler_closure_emit_from_ingest_test.dag", f: "compiler_closure_scoped_ingest_module_count_ok_holds", diff --git a/dag/gunbc/fabric/durable_cas_fabric_storage.dag b/dag/gunbc/fabric/durable_cas_fabric_storage.dag index d66425f817e..8d7762f2f6b 100644 --- a/dag/gunbc/fabric/durable_cas_fabric_storage.dag +++ b/dag/gunbc/fabric/durable_cas_fabric_storage.dag @@ -11,7 +11,7 @@ import std.durable_compare_and_set { CasUnreadableSlot, CasUnreadableMalformed, CasUnreadableReadRefused, CasUnreadableObservationBoundExceeded, CasOutcome, CasCommitted, CasPreconditionFailed, CasStoreRefused, CasSlotObservationRefused, CasGenerationPublicationRefused, - cas_generation_count, cas_generation_next, cas_generation_first, + cas_generation_count, cas_generation_successor, CasSuccessorGeneration, CasSuccessorExhausted, cas_generation_exhausted, cas_generation_first, } import gunbc.durable_cas_file_store { VerifiedCasAttempt } import extdeps.languages.json.emit { JsonValue, json_kv, json_string, json_int, json_object, serialize_json } @@ -160,7 +160,11 @@ fn fabric_storage_compare_and_set(store: FabricStorageBinding, verified: Verifie ExpectSlotAbsent => CasPreconditionFailed { expected: attempt.expected, observed: CasReadablePresent { version: v } } ExpectSlotGeneration { generation: g } => if cas_generation_count(g: g) == cas_generation_count(g: v.generation) { - cas_slot_advance(store: store, verified: verified, expected: ExpectHeadAt { object: o }, target: cas_generation_next(g: v.generation)) + match cas_generation_successor(g: v.generation) { + CasSuccessorExhausted { head: h } => cas_generation_exhausted(head: h) + CasSuccessorGeneration { generation: next } => + cas_slot_advance(store: store, verified: verified, expected: ExpectHeadAt { object: o }, target: next) + } } else { CasPreconditionFailed { expected: attempt.expected, observed: CasReadablePresent { version: v } } } diff --git a/dag/gunbc/fabric/fabric_storage_wire.dag b/dag/gunbc/fabric/fabric_storage_wire.dag index a5dc83c81e0..17430857bb8 100644 --- a/dag/gunbc/fabric/fabric_storage_wire.dag +++ b/dag/gunbc/fabric/fabric_storage_wire.dag @@ -2,7 +2,7 @@ module gunbc.fabric_storage_wire import std.types { String, NonEmptyStr, Int, List } import std.durable_compare_and_set { - CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, CasUnreadableSlot, + CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, CasGenerationSpaceExhausted, CasUnreadableSlot, CasUnreadableMalformed, CasUnreadableContentMissing, CasUnreadableReadRefused, CasUnreadableObservationBoundExceeded, cas_generation_count, } @@ -68,6 +68,7 @@ fn fault_words(fault: FabricStorageFault) -> List { FabricStoreRefused { cause: c } => match c { CasGenerationPublicationRefused { detail: d } => ["store-publish", d as String] + CasGenerationSpaceExhausted { head: h } => ["store-exhausted", to_string(h)] CasSlotObservationRefused { cause: u } => match u { CasUnreadableMalformed { detail: d } => ["store-malformed", d as String] @@ -193,6 +194,7 @@ fn decode_fault(ws: List, i: Int, line: String) -> FabricStorageFault { "store-malformed" => FabricStoreRefused { cause: CasSlotObservationRefused { cause: CasUnreadableMalformed { detail: nonempty_or(text: detail, fallback: "unspecified") } } } "store-read-refused" => FabricStoreRefused { cause: CasSlotObservationRefused { cause: CasUnreadableReadRefused { detail: nonempty_or(text: detail, fallback: "unspecified") } } } "store-content-missing" => match content_hash_from_structural_digest(digest: detail) { Present { value: h } => FabricStoreRefused { cause: CasSlotObservationRefused { cause: CasUnreadableContentMissing { referenced: h } } } Absent => undecodable(line: line) } + "store-exhausted" => match parse_int(s: detail) { Present { value: h } => FabricStoreRefused { cause: CasGenerationSpaceExhausted { head: h } } Absent => undecodable(line: line) } "store-bound" => match parse_int(s: detail) { Present { value: b } => FabricStoreRefused { cause: CasSlotObservationRefused { cause: CasUnreadableObservationBoundExceeded { bound: b } } } Absent => undecodable(line: line) } _ => undecodable(line: line) } diff --git a/dag/gunbc/fleet_observation/capture_chunk.dag b/dag/gunbc/fleet_observation/capture_chunk.dag index 30695efad99..dd7bda02b7c 100644 --- a/dag/gunbc/fleet_observation/capture_chunk.dag +++ b/dag/gunbc/fleet_observation/capture_chunk.dag @@ -29,6 +29,7 @@ import std.durable_compare_and_set { CasUnreadableObservationBoundExceeded, CasSlotObservationRefused, CasGenerationPublicationRefused, + CasGenerationSpaceExhausted, } import gunbc.fleet_observation_collector_ownership { CollectorSessionId } @@ -333,6 +334,8 @@ fn local_commit_from_cas(outcome: CasOutcome) -> LocalCommitStanding { } CasGenerationPublicationRefused { detail: detail } => LocalCommitFailed { cause: ChunkCommitRefused { detail: detail } } + CasGenerationSpaceExhausted { head: h } => + LocalCommitFailed { cause: ChunkCommitRefused { detail: join(["slot generation space exhausted at head ", to_string(h)], "") as NonEmptyStr } } } } } diff --git a/dag/gunbc/instruments/fabric_control_plane_live_probe.dag b/dag/gunbc/instruments/fabric_control_plane_live_probe.dag index 034a6126325..5960574b515 100644 --- a/dag/gunbc/instruments/fabric_control_plane_live_probe.dag +++ b/dag/gunbc/instruments/fabric_control_plane_live_probe.dag @@ -33,7 +33,7 @@ import std.durable_compare_and_set { CasObservedReadable, CasObservedUnreadable, CasReadableAbsent, CasReadablePresent, CasUnreadableSlot, CasUnreadableMalformed, CasUnreadableContentMissing, CasUnreadableReadRefused, CasUnreadableObservationBoundExceeded, - CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, + CasStoreFailure, CasSlotObservationRefused, CasGenerationPublicationRefused, CasGenerationSpaceExhausted, } import product.fabric.identity { FabricIdentity, OfferKey, DemandKey, WorkKey } import product.fabric.demand { Demand } @@ -616,6 +616,7 @@ fn fci1_cas_store_failure_wire(cause: CasStoreFailure) -> NonEmptyStr { match cause { CasSlotObservationRefused { cause: c } => fci1_cas_unreadable_wire(cause: c) CasGenerationPublicationRefused { detail: _ } => "cas-publication-refused" + CasGenerationSpaceExhausted { head: _ } => "cas-generation-space-exhausted" } } diff --git a/dag/gunbc/instruments/scm_write_spine_canary.dag b/dag/gunbc/instruments/scm_write_spine_canary.dag index 6f5e5fd6c73..2e5e7d12826 100644 --- a/dag/gunbc/instruments/scm_write_spine_canary.dag +++ b/dag/gunbc/instruments/scm_write_spine_canary.dag @@ -25,7 +25,6 @@ module gunbc.instruments.scm_write_spine_canary import std.types { String, NonEmptyStr, Int, Bool } import std.process { ProcessExit, ExitSuccess, exit_failure } import std.durable_compare_and_set { CasGeneration, cas_generation_count, CasUnreadableObservationBoundExceeded } -import gunbc.durable_cas_file_store { cas_max_generation_probe } import gunbc.scm.repository_slot { RepositorySlot, LoadedRepositoryGeneration, RepositoryPublication, RepositoryPublished, diff --git a/dag/gunbc/recurring_failure_mode/store_refusal_reported_as_contention.dag b/dag/gunbc/recurring_failure_mode/store_refusal_reported_as_contention.dag index 4d05d4ed014..9521b854585 100644 --- a/dag/gunbc/recurring_failure_mode/store_refusal_reported_as_contention.dag +++ b/dag/gunbc/recurring_failure_mode/store_refusal_reported_as_contention.dag @@ -13,7 +13,7 @@ data store_refusal_reported_as_contention: RecurringFailureMode = RecurringFailu "SPECIMEN, REPAIRED (silent-stag-307): cas_commit_at previously mapped every unsuccessful WriteOwnerOnly to CasPreconditionFailed via cas_probe_as_readable, including ProbedBeyondBound-as-absent. Publication now folds Filesystem.WriteCreateNew through filesystem_create_new. CasPreconditionFailed is emitted only for FilesystemCreateTargetOccupied together with a readable winner. Permission, other, unrecognized kinds, and occupied-with-no-readable-winner are CasStoreRefused. No error string is parsed. Observe uses cas_probe_as_observation, which preserves unreadability.", "EXECUTED, hermetic classification fold (floor run 34797864081): test.claim.durable_cas_file_store_witness a_permission_refused_create_is_store_refused_not_contention, occupied_create_with_no_readable_winner_is_store_refused_not_contention, and occupied_create_with_a_readable_winner_is_precondition_failed. Those three mock the filesystem; they are not the composed path. A fourth row on the same run compared the production fold against a deliberately widening fold shipped as an importable production declaration in the same module; the program-author ruling on gunbc#11335 struck that fold (DESIGN 4b(4) keeps the RED against the real fold enrolled, never a second, intentionally false decision authority beside it), and a branch-local mutation of cas_outcome_from_create is how discrimination is demonstrated.", - "SIBLING ARM, same class, found by the same ruling: cas_probe_from_exact reclassified FilesystemExactPathKindUnrecognized as ProbedUnreadable { kind: FilesystemOtherFailure }, reporting a vocabulary mismatch between realization and interface as an ordinary recognized host failure -- the catch-all the filesystem authority says an unrecognized kind name must never map to. It now carries ProbedReadKindUnrecognized { generation, observed } and projects to CasStoreRefused / CasObservedUnreadable with CasUnreadableMalformed; the hermetic control is test.claim.durable_cas_file_store_witness an_unrecognized_read_kind_is_refused_as_unrecognized_not_as_other.", + "SIBLING ARM, same class, found by the same ruling: the probe's read classifier (now cas_classify_generation_read, which every generation read of cas_observe_slot routes through) reclassified FilesystemExactPathKindUnrecognized as ProbedUnreadable { kind: FilesystemOtherFailure }, reporting a vocabulary mismatch between realization and interface as an ordinary recognized host failure -- the catch-all the filesystem authority says an unrecognized kind name must never map to. It now carries ProbedReadKindUnrecognized { generation, observed } and projects to CasStoreRefused / CasObservedUnreadable with CasUnreadableMalformed; the hermetic control is test.claim.durable_cas_file_store_witness an_unrecognized_read_kind_is_refused_as_unrecognized_not_as_other.", "EXECUTED, filesystem publication layer (BuildBuddy amd64): cargo test --release -p v1-compiler --lib write_file_create_new (11 tests), including a_write_failure_after_creation_leaves_no_target_behind (post-staging RLIMIT_FSIZE) and direct_final_path_open_then_write_leaves_a_target_when_the_write_fails. Publication, not classification.", @@ -32,7 +32,7 @@ data store_refusal_reported_as_contention: RecurringFailureMode = RecurringFailu evidence: [ decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_outcome_from_create"), - decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_probe_from_exact"), + decl_ref(module_path: "gunbc.durable_cas_file_store", decl_name: "cas_classify_generation_read"), decl_ref(module_path: "test.claim.durable_cas_file_store_witness", decl_name: "a_permission_refused_create_is_store_refused_not_contention"), decl_ref(module_path: "test.claim.durable_cas_file_store_witness", decl_name: "an_unrecognized_read_kind_is_refused_as_unrecognized_not_as_other"), decl_ref(module_path: "test.claim.durable_cas_file_store_wet_witness", decl_name: "a_non_contention_store_refusal_is_not_precondition_failed_by_real_execution"), diff --git a/dag/gunbc/roadmap/roadmap_serve.dag b/dag/gunbc/roadmap/roadmap_serve.dag index e20232dc3ce..460e5c7c977 100644 --- a/dag/gunbc/roadmap/roadmap_serve.dag +++ b/dag/gunbc/roadmap/roadmap_serve.dag @@ -515,6 +515,12 @@ fn roadmap_mounts_during_cutover(h: ApprovalBrokerHandler) -> Bool { ApprovalDecideHandler => true ApprovalSubmitHandler => true ApprovalStatusHandler => true + DeviceEnrolHandler => false + DeviceRedeemHandler => false + DevicePendingHandler => false + DeviceRequestHandler => false + DeviceEnrollmentReadbackHandler => false + DevicePushUpdateHandler => false } } diff --git a/dag/std/durable_compare_and_set.dag b/dag/std/durable_compare_and_set.dag index 3026427b971..04e02b7ca70 100644 --- a/dag/std/durable_compare_and_set.dag +++ b/dag/std/durable_compare_and_set.dag @@ -18,6 +18,7 @@ module std.durable_compare_and_set import std.types { NonEmptyStr, Int, String } import std.content_hash { ContentHash, serialize_content_hash } +import std.checked_arithmetic { int_inclusive_max } type CasGeneration = @@ -128,8 +129,9 @@ type CasSlotObservation // // THE PLACEMENT WAS PUT TO REVIEW AND RULED ON, and the ruling also corrected the NAME, which is the // part worth keeping. The arm stays here: an interface outcome need not be producible by every -// realization, it needs a real producer and a stable caller-visible meaning, and the file store -// supplies both. Moving it into the realization would either erase the typed remedy or force the whole +// realization, it needs a real producer and a stable caller-visible meaning, and a realization that +// must discover its head under a budget supplies both (gunbc.fabric.durable_cas_fabric_storage does; the +// file store no longer does, because its head search is total over the generation line). Moving it into the realization would either erase the typed remedy or force the whole // store-failure carrier to become realization-specific. // // But the first spelling was `CasUnreadableBeyondProbeBound`, and PROBE IS THE FILE REALIZATION'S @@ -176,9 +178,16 @@ fn cas_unreadable_slot_detail(cause: CasUnreadableSlot) -> String { // only the DETAIL of the third. So the three-way outcome stands and its payload gains the // distinction. A caller with no use for it matches `CasStoreRefused` and carries the value on, which // is honest; a caller that needs to tell a corrupt head from a failed write can now do so. +// THE THIRD WAY IS THAT THE GENERATION LINE HAS ENDED. CasGeneration is realized as a machine Int +// (std.checked_arithmetic int_inclusive_max), so a slot whose head IS that maximum has no successor to +// publish. That is neither an unreadable head nor a publication the store refused for a host reason: +// the head is well formed and the store is healthy, and the only honest answer is that this slot can +// never advance again. It is unreachable by any consumer at a physical rate, and it is still typed, +// because the alternative is a successor computed by an overflowing addition. type CasStoreFailure = CasSlotObservationRefused { cause: CasUnreadableSlot } | CasGenerationPublicationRefused { detail: NonEmptyStr } + | CasGenerationSpaceExhausted { head: CasGeneration } // The outcome of one attempt. // @@ -252,8 +261,23 @@ fn cas_generation_count(g: CasGeneration) -> Int { g } -fn cas_generation_next(g: CasGeneration) -> CasGeneration { - cas_generation_count(g: g) + 1 +// THE SUCCESSOR IS TOTAL, AND THE LAST GENERATION HAS NONE. This replaces `cas_generation_next`, +// which added 1 unconditionally, so a head at the Int maximum had a successor only an overflowing +// addition could name. The check precedes the addition (std.checked_arithmetic: pre-check, never +// post-check). +type CasGenerationSuccessor + = CasSuccessorGeneration { generation: CasGeneration } + | CasSuccessorExhausted { head: CasGeneration } + +fn cas_generation_successor(g: CasGeneration) -> CasGenerationSuccessor { + if cas_generation_count(g: g) >= int_inclusive_max() { CasSuccessorExhausted { head: g } } + else { CasSuccessorGeneration { generation: cas_generation_count(g: g) + 1 } } +} + +// ONE AUTHORITY FOR THE EXHAUSTED OUTCOME, so every realization that finds a head with no successor +// answers with the same refusal rather than re-spelling it. +fn cas_generation_exhausted(head: CasGeneration) -> CasOutcome { + CasStoreRefused { cause: CasGenerationSpaceExhausted { head: head } } } fn cas_generation_first() -> CasGeneration { @@ -263,10 +287,10 @@ fn cas_generation_first() -> CasGeneration { // The generation a successful commit lands on, derived from the observation // rather than from the caller's expectation — a caller cannot name the // generation it is about to occupy. -fn cas_committed_generation(readable: CasReadableSlot) -> CasGeneration { +fn cas_committed_generation(readable: CasReadableSlot) -> CasGenerationSuccessor { match readable { - CasReadableAbsent => cas_generation_first() - CasReadablePresent { version: v } => cas_generation_next(g: v.generation) + CasReadableAbsent => CasSuccessorGeneration { generation: cas_generation_first() } + CasReadablePresent { version: v } => cas_generation_successor(g: v.generation) } } @@ -335,12 +359,16 @@ fn cas_decide_readable( readable: CasReadableSlot ) -> CasOutcome { if cas_expectation_admits(expected: attempt.expected, readable: readable) { - CasCommitted { - committed: CasSlotVersion { - generation: cas_committed_generation(readable: readable), - content: attempt.proposed_content, - value: attempt.proposed - } + match cas_committed_generation(readable: readable) { + CasSuccessorExhausted { head: h } => cas_generation_exhausted(head: h) + CasSuccessorGeneration { generation: g } => + CasCommitted { + committed: CasSlotVersion { + generation: g, + content: attempt.proposed_content, + value: attempt.proposed + } + } } } else { CasPreconditionFailed { expected: attempt.expected, observed: readable } diff --git a/dag/std/fabric_storage.dag b/dag/std/fabric_storage.dag index 9cec51f1595..902b045b354 100644 --- a/dag/std/fabric_storage.dag +++ b/dag/std/fabric_storage.dag @@ -244,6 +244,7 @@ fn fabric_storage_fault_wire(fault: FabricStorageFault) -> String { FabricStoreRefused { cause: c } => match c { CasSlotObservationRefused { cause: u } => join(["store could not read the head: ", cas_unreadable_slot_detail(cause: u)], "") CasGenerationPublicationRefused { detail: d } => join(["store refused publication: ", d as String], "") + CasGenerationSpaceExhausted { head: h } => join(["store generation space exhausted at head ", to_string(h)], "") } FabricObjectMissing { object: o } => join(["object missing: ", fabric_object_ref_wire(object: o) as String], "") FabricObjectCorrupt { object: o, detail: d } => join(["object corrupt: ", fabric_object_ref_wire(object: o) as String, " ", d as String], "") diff --git a/dag/test/claim/approval_assertion_counter_wet_witness_test.dag b/dag/test/claim/approval_assertion_counter_wet_witness_test.dag new file mode 100644 index 00000000000..9ed5b3791c8 --- /dev/null +++ b/dag/test/claim/approval_assertion_counter_wet_witness_test.dag @@ -0,0 +1,173 @@ +module test.claim.approval_assertion_counter_wet_witness_test + +import extdeps.shell +import std.logic { Bool } +import std.types { String, NonEmptyStr, Int } +import std.durable_compare_and_set { ExpectSlotGeneration, cas_attempt, CasPreconditionFailed, CasReadablePresent } +import std.content_hash { content_hash_of_value } +import extdeps.filesystem.filesystem_io { Filesystem, filesystem_create_new } +import gunbc.durable_cas_file_store { + CasSlotProbe, ProbedHead, cas_probe_bisect, cas_outcome_from_create, observe_cas_slot_state, cas_file_slot_path, + CasGenerationRead, GenerationPresent, GenerationAbsent, cas_read_generation, +} +import gunbc.auth.approval_assertion_counter { + AssertionCounterAdmission, AssertionCounterAdmitted, AssertionCounterReplayed, AssertionCounterRaced, AssertionCounterStoreRefused, + admit_assertion_counter, assertion_counter_commit, assertion_counter_refusal_status, +} + +// THE ASSERTION COUNTER STANDING, EXECUTED AGAINST A REAL FILESYSTEM through +// gunbc.durable_cas_file_store: each claim owns a fresh store under a throwaway /tmp directory and +// removes it before returning. Effects: shell.Mktemp.DirWithTemplate, the CAS store's Filesystem +// reads and create-new writes, shell.Remove.RecursiveForce. The route wiring that hands +// AuthenticAssertion.counter to this admission is not executed here: minting AssertionAuthentic +// needs a real verification, which the device routes refuse to run on the interpreter +// (gunbc.auth.approval_device_crypto_realization). + +fn fresh_counter_root() -> String { + shell.Mktemp.DirWithTemplate(template: "/tmp/gunbc_assertion_counter.XXXXXX").path +} + +fn admitted_at(a: AssertionCounterAdmission, counter: Int) -> Bool { + match a { + AssertionCounterAdmitted { enrollment_id: _, counter: c } => c == counter + _ => false + } +} + +fn replayed(a: AssertionCounterAdmission) -> Bool { + match a { + AssertionCounterReplayed { observed: _, last_admitted: _ } => assertion_counter_refusal_status(a: a) == 403 + _ => false + } +} + +// A REPLAY AT AN ALREADY-ADMITTED COUNTER IS REFUSED, and so is an older one; the positive control +// at a higher counter is admitted after both refusals, so the refusals did not wedge the slot. +test fn a_replayed_assertion_counter_is_refused_and_a_higher_one_admitted() -> Bool { + let root = fresh_counter_root() + let first = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-482913", observed: 5) + let same = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-482913", observed: 5) + let older = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-482913", observed: 4) + let higher = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-482913", observed: 6) + let replay_of_higher = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-482913", observed: 6) + let removed = shell.Remove.RecursiveForce(path: root) + admitted_at(a: first, counter: 5) && replayed(a: same) && replayed(a: older) && admitted_at(a: higher, counter: 6) && replayed(a: replay_of_higher) && removed.success +} + +// THE STANDING IS PER ENROLMENT: one enrolment's admitted counter does not refuse another's. +test fn the_counter_standing_is_per_enrolment() -> Bool { + let root = fresh_counter_root() + let a = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-aaaa", observed: 9) + let b = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-bbbb", observed: 1) + let removed = shell.Remove.RecursiveForce(path: root) + admitted_at(a: a, counter: 9) && admitted_at(a: b, counter: 1) && removed.success +} + +// A LOST COMPARE-AND-SET RACE IS REFUSED, NOT ADMITTED. Two requests that read the same standing +// commit against the same generation; the second commit arrives after the first has advanced the +// slot, so its expectation names a superseded generation and the store's exclusive create decides +// against it. The positive control is the first commit itself. +test fn a_lost_counter_race_is_refused_not_admitted() -> Bool { + let root = fresh_counter_root() + let first = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-race", observed: 5) + let winner = assertion_counter_commit(root: root as NonEmptyStr, enrollment_id: "enr-race", expected: ExpectSlotGeneration { generation: 1 }, observed: 6) + let loser = assertion_counter_commit(root: root as NonEmptyStr, enrollment_id: "enr-race", expected: ExpectSlotGeneration { generation: 1 }, observed: 7) + let after = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-race", observed: 6) + let removed = shell.Remove.RecursiveForce(path: root) + let raced = match loser { + AssertionCounterRaced => assertion_counter_refusal_status(a: loser) == 409 + _ => false + } + admitted_at(a: first, counter: 5) && admitted_at(a: winner, counter: 6) && raced && replayed(a: after) && removed.success +} + +fn admit_sequentially(root: NonEmptyStr, enrollment_id: NonEmptyStr, next: Int, last: Int) -> Bool { + if next > last { true } + else { + match admit_assertion_counter(root: root, enrollment_id: enrollment_id, observed: next) { + AssertionCounterAdmitted { enrollment_id: _, counter: c } => + if c == next { admit_sequentially(root: root, enrollment_id: enrollment_id, next: next + 1, last: last) } else { false } + _ => false + } + } +} + +// THE CLAIM THAT WOULD HAVE CAUGHT THE CLIFF, AT ONE INTERFACE (DESIGN section 3). Its subject is +// head discovery and the next admission past generation 4096 -- not 4200 admissions each run end to +// end, which cost ~22 s and re-executed a path the claims above already execute for real. So the +// history is SUPPLIED: 4200 contiguous generations are written into the slot through the store's own +// slot-path authority (cas_file_slot_path), each holding the counter an admission would have written, +// so the layout cannot drift from production. Then ONE real admission runs against it: the last counter +// again and an older one are replays, and the next is admitted. Restoring the old 4096 bound or the +// linear walk reds it. +fn seed_contiguous_generations(root: NonEmptyStr, key: NonEmptyStr, next: Int, last: Int) -> Bool { + if next > last { true } + else { + let w = Filesystem.WriteCreateNew(path: cas_file_slot_path(root: root, key: key, generation: next), content: to_string(next)) + if w.success { seed_contiguous_generations(root: root, key: key, next: next + 1, last: last) } else { false } + } +} + +test fn an_enrolment_keeps_admitting_past_four_thousand_ninety_six_assertions() -> Bool { + let root = fresh_counter_root() + let seeded = seed_contiguous_generations(root: root as NonEmptyStr, key: "enr-long-lived", next: 1, last: 4200) + let again = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-long-lived", observed: 4200) + let older = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-long-lived", observed: 17) + let next = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: "enr-long-lived", observed: 4201) + let removed = shell.Remove.RecursiveForce(path: root) + seeded && replayed(a: again) && replayed(a: older) && admitted_at(a: next, counter: 4201) && removed.success +} + +// AN APPEND THAT LANDS MID-SEARCH YIELDS A STALE HEAD, NEVER A FABRICATED ONE, AND A WRITER ACTING ON +// THE STALE HEAD IS REFUSED BY THE EXCLUSIVE CREATE ITSELF. Five counters are admitted (generations +// 1..5). The search's boundary is OBSERVED, not supplied: generation 4 is READ present and generation 6 +// is READ absent through the store's own classified read (cas_read_generation), which is the state a +// real search holds after its gallop and one bisection step. Only THEN does a concurrent writer publish +// generation 6, and the bisection resumes from exactly those two observed facts -- the absent bound it +// carries was true when it was read and is stale when it is used, which is the interleaving. It must +// report generation 5 holding counter 5, a generation that really was committed, one behind the real +// head. A writer acting on that stale head then attempts the real exclusive create of generation 6: the +// OS reports occupancy, the create never overwrites (generation 6 still holds counter 6), and the store +// classifies it as a lost race. +test fn an_append_landing_mid_search_yields_a_stale_real_head_and_the_stale_writer_is_refused_by_the_create() -> Bool { + let root = fresh_counter_root() + let key: NonEmptyStr = "enr-interleave" + let seeded = admit_sequentially(root: root as NonEmptyStr, enrollment_id: key, next: 1, last: 5) + let observed_present = cas_read_generation(root: root as NonEmptyStr, key: key, generation: 4) + let observed_absent = cas_read_generation(root: root as NonEmptyStr, key: key, generation: 6) + let appended = admit_assertion_counter(root: root as NonEmptyStr, enrollment_id: key, observed: 6) + let resumed = match observed_present { + GenerationPresent { content: v4 } => match observed_absent { + GenerationAbsent => Present { value: cas_probe_bisect(root: root as NonEmptyStr, key: key, present: 4, present_value: v4, absent: 6) } + _ => Absent + } + _ => Absent + } + let stale_real = match resumed { + Present { value: probe } => match probe { + ProbedHead { generation: g, value: v } => + g == 5 && (v as String) == "5" && (v as String) == Filesystem.Read(path: cas_file_slot_path(root: root as NonEmptyStr, key: key, generation: g)).content + _ => false + } + Absent => false + } + let target_path = cas_file_slot_path(root: root as NonEmptyStr, key: key, generation: 6) + let stale_write = Filesystem.WriteCreateNew(path: target_path, content: "7") + let stale_attempt = cas_attempt(key: key, expected: ExpectSlotGeneration { generation: 5 }, proposed: "7" as NonEmptyStr, proposed_content: content_hash_of_value(value: "7")) + let classified = cas_outcome_from_create( + attempt: stale_attempt, + target: 6, + created: filesystem_create_new(path: stale_write.path, success: stale_write.success, error: stale_write.error, error_kind: stale_write.error_kind), + post: observe_cas_slot_state(root: root as NonEmptyStr, key: key), + ) + let refused_as_race = match classified { + CasPreconditionFailed { expected: _, observed: o } => match o { + CasReadablePresent { version: v } => v.generation == 6 && (v.value as String) == "6" + _ => false + } + _ => false + } + let not_overwritten = Filesystem.Read(path: target_path).content == "6" + let removed = shell.Remove.RecursiveForce(path: root) + seeded && admitted_at(a: appended, counter: 6) && stale_real && !stale_write.success && refused_as_race && not_overwritten && removed.success +} diff --git a/dag/test/claim/approval_broker_serve_witness_test.dag b/dag/test/claim/approval_broker_serve_witness_test.dag index fca76f5b84b..a5821b1c247 100644 --- a/dag/test/claim/approval_broker_serve_witness_test.dag +++ b/dag/test/claim/approval_broker_serve_witness_test.dag @@ -16,7 +16,7 @@ import gunbc.auth.approval_broker_marker { approval_broker_served_token, approval_serving_process_token, } import gunbc.auth.approval_broker_serve { - ApprovalBrokerHandler, + ApprovalBrokerHandler, DeviceEnrolHandler, DeviceRedeemHandler, DevicePendingHandler, DeviceRequestHandler, DeviceEnrollmentReadbackHandler, DevicePushUpdateHandler, ApprovalConfirmPageHandler, ApprovalDecideHandler, ApprovalSubmitHandler, ApprovalStatusHandler, approval_broker_route_specs, approval_broker_route_table_build, @@ -75,13 +75,30 @@ test fn approval_broker_table_selects_the_four_routes() -> Bool { && broker_selects(method: GET, path: "/approvals/esc-1", want: ApprovalStatusHandler) } -// THE TABLE IS EXACTLY THE FOUR. A fifth row is not a neutral addition: every route this process -// serves is one more thing whose demand shares the broker's slice, and the split exists because -// co-tenancy is what made an approval poll depend on a dashboard render. +// THE SIX DEVICE ROUTES ARE ANSWERED HERE AND ONLY AS POSTS (gunbc.auth.approval_device_wire: +// every device operation is a POST whose body carries its authentication). The two suffixed +// routes bind one segment; a GET on any of them is 405, not a read. +test fn approval_broker_table_selects_the_six_device_routes_as_posts() -> Bool { + broker_selects(method: POST, path: "/approve/device/enrol", want: DeviceEnrolHandler) + && broker_selects(method: POST, path: "/approve/device/redeem", want: DeviceRedeemHandler) + && broker_selects(method: POST, path: "/approve/device/pending", want: DevicePendingHandler) + && broker_selects(method: POST, path: "/approve/device/requests/id-ZXNj", want: DeviceRequestHandler) + && broker_selects(method: POST, path: "/approve/device/enrollments/id-ZW5y", want: DeviceEnrollmentReadbackHandler) + && broker_selects(method: POST, path: "/approve/device/push", want: DevicePushUpdateHandler) + && match serve_select_route(table: broker_table_or_empty(), method: GET, path: "/approve/device/pending") { + MethodNotAllowed { allowed: ms } => count(ms) == 1 + _ => false + } +} + +// THE TABLE IS EXACTLY THE TEN: the four approval routes and the six device routes. An eleventh +// row is not a neutral addition: every route this process serves is one more thing whose demand +// shares the broker's slice, and the split exists because co-tenancy is what made an approval +// poll depend on a dashboard render. test fn approval_broker_table_carries_no_other_route() -> Bool { - count(approval_broker_route_specs()) == 4 + count(approval_broker_route_specs()) == 10 && match approval_broker_route_table_build() { - ServedRouteTableBuilt { table: t } => count(t.routes) == 4 + ServedRouteTableBuilt { table: t } => count(t.routes) == 10 ServedRouteTableBuildRefused { raw: _, segment: _, reason: _ } => false } } diff --git a/dag/test/claim/approval_device_routes_wet_witness_test.dag b/dag/test/claim/approval_device_routes_wet_witness_test.dag new file mode 100644 index 00000000000..bca9b9d4d63 --- /dev/null +++ b/dag/test/claim/approval_device_routes_wet_witness_test.dag @@ -0,0 +1,32 @@ +module test.claim.approval_device_routes_wet_witness_test + +import std.logic { Bool } +import std.types { String, Timestamp, List } +import gunbc.auth.approval_device_routes { device_pending_response_at } +import gunbc.auth.approval_device_wire { ReadAuthentication, read_authentication_json } +import gunbc.auth.approval_device_crypto_realization { + DeviceCryptoRealization, DeviceCryptoObligation, NativeDeviceCryptoBound, DeviceCryptoHandlerReceipt, + P256SignatureVerification, AppAttestAttestationVerification, AppAttestAssertionVerification, P256BasePointOrder, +} + +// THE GATE'S DISCRIMINATING CONTROL, executed on the required floor's local-repo wet lane +// (v2.workflow.local_repo_wet_terminal local_repo_wet_schedule): under a bound realization the read +// proceeds past the gate into the enrolment store's Filesystem.Read, which has no mock_response, and +// the route takes no store as a parameter, so the store cannot be supplied at this interface. The +// gate claims it pairs with stay hermetic in test.claim.approval_device_routes_witness_test. + +fn fx_bound(covered: List) -> DeviceCryptoRealization { + NativeDeviceCryptoBound { receipt: DeviceCryptoHandlerReceipt { handler_identity: "fixture-native-handler", exact_revision: "0000000", covered: covered } } +} + +data fx_now: Timestamp = "2026-09-21T12:00:00Z" +data fx_auth: ReadAuthentication = ReadAuthentication { enrollment_id: "enr-482913", requested_at: "2026-09-21T12:00:30Z", assertion_b64: "omlzaWduYXR1cmU" } +data fx_unrealized: String = "native device-crypto realization is unavailable" + +// The discriminating control for the four gate claims in test.claim.approval_device_routes_witness_test: +// the SAME read under a bound realization does not answer the realization reason -- it proceeds past +// the gate and answers from the store -- so it is the gate, not a later failure, that decided them. +test fn a_bound_realization_passes_the_read_past_the_gate() -> Bool { + !string_contains(s: device_pending_response_at(realization: fx_bound(covered: [P256SignatureVerification, AppAttestAttestationVerification, AppAttestAssertionVerification, P256BasePointOrder]), body: read_authentication_json(a: fx_auth), observed_at: fx_now).body, pattern: fx_unrealized) +} + diff --git a/dag/test/claim/approval_device_routes_witness_test.dag b/dag/test/claim/approval_device_routes_witness_test.dag new file mode 100644 index 00000000000..652dc128164 --- /dev/null +++ b/dag/test/claim/approval_device_routes_witness_test.dag @@ -0,0 +1,230 @@ +module test.claim.approval_device_routes_witness_test + +import std.logic { Bool } +import std.types { String, NonEmptyStr, Timestamp, List } +import gunbc.auth.approval_writer_authority { ApprovalServingProcess, BrokerProcess, RoadmapProcess, ApprovalWriteAdmitted, ApprovalWriteRefused, approval_write_admission } +import gunbc.auth.approval_device_routes { + DeviceRouteResponse, + device_enrol_response_at, device_redeem_response_at, device_pending_response_at, device_request_response_at, device_enrollment_readback_response_at, device_push_update_response_at, + redemption_status, requested_at_within_skew, +} +import gunbc.auth.approval_device_redemption { observe_enrollment, EnrolmentSlotUnreadable, approval_device_store_root, DeviceLostTheRace, DeviceEnrollmentUnknown, DeviceChallengeNotIssuedHere, DeviceCommitRefused, DevicePlatformUnrealized, DeviceCapabilityTagMalformed } +import gunbc.auth.approval_device_redemption_fixtures { envelope_vector_body } +import gunbc.auth.approval_decision_store { observe_escalation, EscalationUnreadable } +import gunbc.auth.approval_device_wire { ReadAuthentication, read_authentication_json, PushUpdateRequest, push_update_request_json, ApnsRegistration, path_segment, SignedRedemption, DeviceRedemptionSigningInput, RedemptionChallenge, IosAppAttestAssertion, signed_redemption_json } +import extdeps.crypto.signature { SignatureBytes, EcdsaP256Sha256, P1363FixedWidth } +import gunbc.auth.approval_capability { ProposeApprove } +import extdeps.apple.apns { ApnsProduction } +import gunbc.auth.approval_app_attest_config { approval_app_attest_verifier, approval_app_attest_app_id, approval_app_bundle_id, AppAttestVerifierAwaitingOperator, AppAttestVerifierConfigured } +import gunbc.auth.approval_device_crypto_realization { + DeviceCryptoRealization, DeviceCryptoObligation, NativeDeviceCryptoBound, DeviceCryptoHandlerReceipt, DeviceCryptoAdmitted, DeviceCryptoRefused, + P256SignatureVerification, AppAttestAttestationVerification, AppAttestAssertionVerification, P256BasePointOrder, + device_crypto_admission, approval_device_crypto_realization, +} +import gunbc.roadmap_serve { roadmap_mounts_during_cutover } +import gunbc.auth.approval_broker_serve { DeviceEnrolHandler, DeviceRedeemHandler, DevicePendingHandler, DeviceRequestHandler, DeviceEnrollmentReadbackHandler, DevicePushUpdateHandler } + +// THE ROUTE FOLDS AT A SUPPLIED INSTANT, on the arms that decide before any store or verifier is +// reached: wire refusals, the writer gate, the segment rule, the enrolment-identity check, and the +// verifier's unconfigured refusal. Every arm past those needs the operator's App ID prefix +// (gunbc.auth.approval_app_attest_config) and a live store; they are the declared frontier the +// configuration row names, and a claim that greened them from designed bytes would assert a +// route nothing can reach. + +// The production binding, read from its row: every claim below that passes it asserts what the +// served route answers today. +data fx_unbound: DeviceCryptoRealization = approval_device_crypto_realization + +fn fx_bound(covered: List) -> DeviceCryptoRealization { + NativeDeviceCryptoBound { receipt: DeviceCryptoHandlerReceipt { handler_identity: "fixture-native-handler", exact_revision: "0000000", covered: covered } } +} + +data fx_now: Timestamp = "2026-09-21T12:00:00Z" +data fx_auth: ReadAuthentication = ReadAuthentication { enrollment_id: "enr-482913", requested_at: "2026-09-21T12:00:30Z", assertion_b64: "omlzaWduYXR1cmU" } + +fn non_writer() -> Bool { + match approval_write_admission(asker: BrokerProcess) { + ApprovalWriteAdmitted { writer: _ } => false + ApprovalWriteRefused { holder: _, asker: _ } => true + } +} + +fn device_route_refused_with(r: DeviceRouteResponse, status: Int, fragment: String) -> Bool { + r.status == status && string_contains(s: r.body, pattern: "\"refused\":") && string_contains(s: r.body, pattern: fragment) +} + +// A body that is not the wire's shape refuses 400 naming where, on every one of the six routes; the +// three mutating routes are asked by the writer, since the writer gate precedes decoding. +fn writer_process() -> ApprovalServingProcess { + if non_writer() { RoadmapProcess } else { BrokerProcess } +} + +test fn malformed_bodies_refuse_400_on_every_route() -> Bool { + device_route_refused_with(r: device_enrol_response_at(realization: fx_unbound, body: "{", process: writer_process(), observed_at: fx_now), status: 400, fragment: "enrolment request refused at") + && device_route_refused_with(r: device_redeem_response_at(realization: fx_unbound, body: "[]", process: writer_process(), observed_at: fx_now), status: 400, fragment: "redemption refused at") + && device_route_refused_with(r: device_pending_response_at(realization: fx_unbound, body: "{\"enrollment_id\":\"e\"}", observed_at: fx_now), status: 400, fragment: "read refused at") + && device_route_refused_with(r: device_request_response_at(realization: fx_unbound, body: "{}", segment: path_segment(s: "esc-1") as String, observed_at: fx_now), status: 400, fragment: "read refused at") + && device_route_refused_with(r: device_enrollment_readback_response_at(realization: fx_unbound, body: "{}", segment: path_segment(s: "enr-1") as String, observed_at: fx_now), status: 400, fragment: "read refused at") + && device_route_refused_with(r: device_push_update_response_at(realization: fx_unbound, body: "{\"auth\":{}}", process: writer_process(), observed_at: fx_now), status: 400, fragment: "push update refused at") +} + +// A malformed or non-canonical path segment refuses 400 before the body is read. +test fn a_bad_segment_refuses_400() -> Bool { + device_route_refused_with(r: device_request_response_at(realization: fx_unbound, body: "", segment: "esc-1", observed_at: fx_now), status: 400, fragment: "request path") + && device_route_refused_with(r: device_enrollment_readback_response_at(realization: fx_unbound, body: "", segment: "id-", observed_at: fx_now), status: 400, fragment: "enrollment path") +} + +// A readback whose body speaks for another enrolment than the path names refuses 403 before any +// verification. +test fn a_readback_for_another_enrolment_refuses_403() -> Bool { + device_route_refused_with(r: device_enrollment_readback_response_at(realization: fx_unbound, body: read_authentication_json(a: fx_auth), segment: path_segment(s: "enr-other") as String, observed_at: fx_now), status: 403, fragment: "another enrolment") +} + +// THE WRITER GATE IS THE FIRST THING THE THREE MUTATING ROUTES ASK: from the process that does not +// hold writer authority, the route refuses 503 with the writer reason before the body is decoded, so +// the body is irrelevant to this subject and is supplied as a bare object. (Which process holds it is +// the cutover posture's fact; the claim names the non-holder by asking the gate.) +test fn the_non_writer_process_is_refused_on_the_mutating_routes() -> Bool { + let asker = if non_writer() { BrokerProcess } else { RoadmapProcess } + device_route_refused_with(r: device_push_update_response_at(realization: fx_unbound, body: "{}", process: asker, observed_at: fx_now), status: 503, fragment: "writer authority") + && device_route_refused_with(r: device_enrol_response_at(realization: fx_unbound, body: "{}", process: asker, observed_at: fx_now), status: 503, fragment: "writer authority") + && device_route_refused_with(r: device_redeem_response_at(realization: fx_unbound, body: "{}", process: asker, observed_at: fx_now), status: 503, fragment: "writer authority") +} + +// THE VERIFIER ROW DECIDES WHETHER READS PROCEED, and this claim reads the row's own arm so it +// flips with the row: while the row awaits the operator every authenticated read refuses 503 +// naming what is missing; once configured (the operator's Team ID 72HGYAMBVQ, 2026-09-22) the row +// derives the App ID the verifier expects -- prefix.bundle -- and the read route reaches the store, +// which the hermetic route cannot follow, so the configured arm asserts the derived expectation. +test fn reads_refuse_unconfigured_until_the_operator_supplies_the_prefix() -> Bool { + match approval_app_attest_verifier { + AppAttestVerifierAwaitingOperator { missing: _ } => + device_route_refused_with(r: device_pending_response_at(realization: fx_unbound, body: read_authentication_json(a: fx_auth), observed_at: fx_now), status: 503, fragment: "not configured") + AppAttestVerifierConfigured { app_id_prefix: p, bundle_id: b, environment: _, admitted_validation_categories: cats, expected_bundle_version: _ } => + (match approval_app_attest_app_id(c: approval_app_attest_verifier) { + Absent => false + Present { value: app_id } => (app_id as String) == (p as String) + "." + (b as String) && b == approval_app_bundle_id + }) + && any(cats, c => c == 3) + } +} + +// A REQUEST-SUPPLIED IDENTITY NEVER BECOMES NAVIGATION (review 69793 of gunbc#12000): the two +// observers the device routes hand a body or path-segment identity to answer Unreadable with the +// store's fixed slot-addressability detail for a separator-carrying key -- the store refuses before +// any read, so no path outside the root is probed and the detail names no host state. +test fn a_traversal_identity_is_refused_by_the_store_before_any_read() -> Bool { + (match observe_enrollment(root: approval_device_store_root, enrollment_id: "enr-../../../etc/shadow") { + EnrolmentSlotUnreadable { detail: d } => string_contains(s: d as String, pattern: "not slot-addressable") + _ => false + }) + && (match observe_escalation(root: approval_device_store_root, escalation_id: "../../../etc/shadow") { + EscalationUnreadable { detail: d } => string_contains(s: d as String, pattern: "not slot-addressable") + _ => false + }) +} + +// The skew window is closed below and open above: 60 s before is inside, 61 s before is not; 59 s +// after is inside, 60 s after is not; a non-canonical claimed time is never inside. The bounds are a +// pure seconds comparison (gunbc.auth.approval_capability utc_instant_seconds_after), so the claim is +// hermetic; an observed instant that is not canonical is outside the window too. +test fn the_read_skew_window_brackets_sixty_seconds() -> Bool { + requested_at_within_skew(requested_at: "2026-09-21T11:59:00Z", observed_at: fx_now) + && !requested_at_within_skew(requested_at: "2026-09-21T11:58:59Z", observed_at: fx_now) + && requested_at_within_skew(requested_at: "2026-09-21T12:00:59Z", observed_at: fx_now) + && !requested_at_within_skew(requested_at: "2026-09-21T12:01:00Z", observed_at: fx_now) + && !requested_at_within_skew(requested_at: "not-a-time", observed_at: fx_now) + && !requested_at_within_skew(requested_at: fx_now, observed_at: "2026-02-30T12:00:00Z") + && requested_at_within_skew(requested_at: "2024-02-29T23:59:30Z", observed_at: "2024-03-01T00:00:29Z") + && !requested_at_within_skew(requested_at: "2023-12-31T23:59:59Z", observed_at: "2024-01-01T00:01:00Z") +} + +// The redemption outcome's status map, exhaustive over the closed outcome: the arms the app +// branches on, plus the two that answer neither 403 nor a store status (a malformed tag is the +// caller's 400; an unrealized platform is 501). +test fn redemption_outcomes_map_to_their_statuses() -> Bool { + redemption_status(o: DeviceLostTheRace) == 409 + && redemption_status(o: DeviceEnrollmentUnknown) == 404 + && redemption_status(o: DeviceChallengeNotIssuedHere) == 403 + && redemption_status(o: DeviceCommitRefused { detail: "x" }) == 503 + && redemption_status(o: DeviceCapabilityTagMalformed) == 400 + && redemption_status(o: DevicePlatformUnrealized) == 501 +} + +// THE ROADMAP NEVER MOUNTS A DEVICE ROUTE, during the cutover or after: the total match in +// gunbc.roadmap.roadmap_serve classifies all six as the broker's alone. +test fn the_roadmap_mounts_no_device_route() -> Bool { + !roadmap_mounts_during_cutover(h: DeviceEnrolHandler) && !roadmap_mounts_during_cutover(h: DeviceRedeemHandler) + && !roadmap_mounts_during_cutover(h: DevicePendingHandler) && !roadmap_mounts_during_cutover(h: DeviceRequestHandler) + && !roadmap_mounts_during_cutover(h: DeviceEnrollmentReadbackHandler) && !roadmap_mounts_during_cutover(h: DevicePushUpdateHandler) +} + +// THE VERIFIER-DEPENDENT ROUTES REFUSE 503 ON THE UNBOUND REALIZATION BEFORE ANY CRYPTO RUNS. Every +// body here is well formed and reaches past the wire and writer gates, the verifier row is +// configured, and each assertion/attestation/signature is bytes that would be handed to a verifier +// -- yet all six answer the realization's own reason. The route asks device_crypto_admission before +// it reads the enrolment store or calls a verifier, so no crypto can have started. +data fx_unrealized: String = "native device-crypto realization is unavailable" + +test fn the_three_reads_refuse_503_before_any_crypto_while_the_native_handler_is_unbound() -> Bool { + device_route_refused_with(r: device_pending_response_at(realization: fx_unbound, body: read_authentication_json(a: fx_auth), observed_at: fx_now), status: 503, fragment: fx_unrealized) + && device_route_refused_with(r: device_request_response_at(realization: fx_unbound, body: read_authentication_json(a: fx_auth), segment: path_segment(s: "esc-1") as String, observed_at: fx_now), status: 503, fragment: fx_unrealized) + && device_route_refused_with(r: device_enrollment_readback_response_at(realization: fx_unbound, body: read_authentication_json(a: fx_auth), segment: path_segment(s: "enr-482913") as String, observed_at: fx_now), status: 503, fragment: fx_unrealized) +} + +fn fx_writer() -> ApprovalServingProcess { + if non_writer() { RoadmapProcess } else { BrokerProcess } +} + +test fn the_push_update_refuses_503_before_any_crypto_while_the_native_handler_is_unbound() -> Bool { + let push = push_update_request_json(r: PushUpdateRequest { auth: fx_auth, push: ApnsRegistration { environment: ApnsProduction, topic: "ai.gunb.approve", token: "a1b2" } }) + device_route_refused_with(r: device_push_update_response_at(realization: fx_unbound, body: push, process: fx_writer(), observed_at: fx_now), status: 503, fragment: fx_unrealized) +} + +test fn the_enrolment_refuses_503_before_any_crypto_while_the_native_handler_is_unbound() -> Bool { + writer_route_refused_unrealized(name: "enrolment_request", route: fn(body) { device_enrol_response_at(realization: fx_unbound, body: body, process: fx_writer(), observed_at: fx_now) }) +} + +// THE REDEMPTION BODY IS SUPPLIED, NOT DERIVED (DESIGN section 3, a witness discriminates at one +// interface). The envelope vector's signing input is built from the redemption vectors, which mint +// real capability tags through interpreted hashing; this claim is about the gate, and needs only a +// body the wire decodes. The real vector's decode is the inhabitance claim in +// test.claim.approval_device_wire_witness_test, so supplying it here removes no execution of the real path. +data fx_signed_redemption: String = signed_redemption_json(r: SignedRedemption { + signing_input: DeviceRedemptionSigningInput { + audience: "gunbc-approval", enrollment_id: "enr-482913", + challenge: RedemptionChallenge { expires_at: "2026-09-21T12:05:00Z", nonce_hex: "9c1d" }, + escalation_id: "esc-1", request_revision: "sha256:abab", stored_request_text: "{}", + decision: ProposeApprove, capability_text: "approve-text", capability_tag_b64url: "dGFn", + }, + signature: SignatureBytes { suite: EcdsaP256Sha256, encoding: P1363FixedWidth, b64url: "c2lnbmF0dXJl" }, + platform_proof: IosAppAttestAssertion { assertion_b64: "omlzaWduYXR1cmU" }, +}) + +test fn the_redemption_refuses_503_before_any_crypto_while_the_native_handler_is_unbound() -> Bool { + device_route_refused_with(r: device_redeem_response_at(realization: fx_unbound, body: fx_signed_redemption, process: fx_writer(), observed_at: fx_now), status: 503, fragment: fx_unrealized) +} + +// The discriminating control for the claims above -- the same read under a bound realization -- +// reaches the store and so runs on the wet lane: test.claim.approval_device_routes_wet_witness_test. + +fn writer_route_refused_unrealized(name: String, route: fn(String) -> DeviceRouteResponse) -> Bool { + match envelope_vector_body(name: name) { + Absent => false + Present { value: body } => device_route_refused_with(r: route(body), status: 503, fragment: fx_unrealized) + } +} + +// THE RECEIPT MUST COVER THE NAMED POPULATION, THE P-256 ORDER FACT INCLUDED: a bound handler whose +// receipt covers every verifier but not the base-point order is refused 503 naming that witness and +// its (n-1)*G control; the full receipt is admitted with its identity and revision. +test fn a_bound_handler_without_the_base_point_order_fact_is_refused() -> Bool { + (match device_crypto_admission(r: fx_bound(covered: [P256SignatureVerification, AppAttestAttestationVerification, AppAttestAssertionVerification])) { + DeviceCryptoRefused { status: s, reason: why } => s == 503 && string_contains(s: why, pattern: "the_base_point_has_order_n") && string_contains(s: why, pattern: "(n-1)*G != infinity") + DeviceCryptoAdmitted { handler_identity: _, exact_revision: _ } => false + }) + && (match device_crypto_admission(r: fx_bound(covered: [P256BasePointOrder, AppAttestAssertionVerification, AppAttestAttestationVerification, P256SignatureVerification])) { + DeviceCryptoAdmitted { handler_identity: h, exact_revision: v } => (h as String) == "fixture-native-handler" && (v as String) == "0000000" + DeviceCryptoRefused { status: _, reason: _ } => false + }) +} diff --git a/dag/test/claim/approval_device_wire_witness_test.dag b/dag/test/claim/approval_device_wire_witness_test.dag index 8799f98d925..9fbf730d2e3 100644 --- a/dag/test/claim/approval_device_wire_witness_test.dag +++ b/dag/test/claim/approval_device_wire_witness_test.dag @@ -14,7 +14,7 @@ import gunbc.auth.approval_device_wire { approval_device_audience, MobileIos, MobileAndroid, device_read_client_data, EnrolmentRequest, IosAppAttestAttestation, ApnsRegistration, SignedRedemption, IosAppAttestAssertion, PushRegistration, WireDecoded, WireRefused, enrolment_request_json, decode_enrolment_request, signed_redemption_json, decode_signed_redemption, - push_update_json, decode_push_update, path_segment, device_request_path, device_push_update_client_data, decode_path_segment, PathSegmentDecoded, PathSegmentMalformed, + push_update_json, decode_push_update, ReadAuthentication, read_authentication_json, decode_read_request, PushUpdateRequest, push_update_request_json, decode_push_update_request, path_segment, device_request_path, device_push_update_client_data, decode_path_segment, PathSegmentDecoded, PathSegmentMalformed, } import extdeps.apple.apns { ApnsProduction } @@ -163,6 +163,43 @@ test fn witness_push_update_round_trips() -> Bool { } } +data fx_read_auth: ReadAuthentication = ReadAuthentication { enrollment_id: "enr-482913", requested_at: "2026-09-18T12:00:30Z", assertion_b64: "omlzaWduYXR1cmU" } + +// THE READ AUTHENTICATION BODY (every device operation is a POST; the assertion rides here, never +// in a header) round-trips, and the push-update envelope { auth, push } round-trips with it. +test fn witness_read_authentication_round_trips() -> Bool { + match decode_read_request(text: read_authentication_json(a: fx_read_auth)) { + WireDecoded { value: a } => a.enrollment_id == fx_read_auth.enrollment_id && a.requested_at == fx_read_auth.requested_at && a.assertion_b64 == fx_read_auth.assertion_b64 + WireRefused { at: _, cause: _ } => false + } +} + +test fn witness_push_update_request_round_trips() -> Bool { + let r = PushUpdateRequest { auth: fx_read_auth, push: fx_push } + match decode_push_update_request(text: push_update_request_json(r: r)) { + WireDecoded { value: d } => push_update_request_json(r: d) == push_update_request_json(r: r) + WireRefused { at: _, cause: _ } => false + } +} + +// A read body with an unknown member refuses at "auth"; an empty assertion refuses at its key; a +// push-update envelope missing "push" refuses at "push". +test fn witness_read_authentication_refuses_strictly() -> Bool { + match decode_read_request(text: "{\"enrollment_id\":\"e\",\"requested_at\":\"t\",\"assertion_b64\":\"a\",\"extra\":1}") { + WireRefused { at: a, cause: _ } => + (a as String) == "auth" + && match decode_read_request(text: "{\"enrollment_id\":\"e\",\"requested_at\":\"t\",\"assertion_b64\":\"\"}") { + WireRefused { at: a2, cause: _ } => (a2 as String) == "assertion_b64" + WireDecoded { value: _ } => false + } + && match decode_push_update_request(text: "{\"auth\":{\"enrollment_id\":\"e\",\"requested_at\":\"t\",\"assertion_b64\":\"a\"}}") { + WireRefused { at: a3, cause: _ } => (a3 as String) == "push" + WireDecoded { value: _ } => false + } + WireDecoded { value: _ } => false + } +} + // STRICTNESS: each refusal names where it failed. test fn witness_decoder_refuses_an_unknown_member() -> Bool { match decode_push_update(text: "{\"kind\":\"apns\",\"environment\":\"production\",\"topic\":\"t\",\"token\":\"x\",\"extra\":\"y\"}") { diff --git a/dag/test/claim/durable_cas_file_store_wet_witness_test.dag b/dag/test/claim/durable_cas_file_store_wet_witness_test.dag index f3d06be7bcd..dc2be56e479 100644 --- a/dag/test/claim/durable_cas_file_store_wet_witness_test.dag +++ b/dag/test/claim/durable_cas_file_store_wet_witness_test.dag @@ -11,9 +11,11 @@ import std.durable_compare_and_set { CasGenerationPublicationRefused, cas_generation_count, } +import std.checked_arithmetic { int_inclusive_max } import gunbc.durable_cas_file_store { CasAttemptAdmission, CasAttemptAdmitted, CasAttemptDigestMismatch, CasAttemptDigestIncomparable, CasAttemptKeyNotSlotAddressable, admit_cas_attempt, file_compare_and_set, DefaultAccessCreateOnly, observe_cas_slot_state, cas_file_slot_path, + CasSlotProbe, ProbedHead, cas_probe_gallop, } // Wet controls for the file-backed CAS provider. Hermetic mint and classification @@ -146,6 +148,28 @@ test fn a_non_contention_store_refusal_is_not_precondition_failed_by_real_execut planted.success && is_store_refused(o: outcome) && removed.success } +// THE GALLOP REACHES THE TOP OF THE GENERATION LINE WITHOUT OVERFLOWING. A search that has read +// generation max/2 + 1 present cannot double, so it probes the Int maximum itself. With only that +// generation on disk it bisects the whole upper half and reports it as the head; with the maximum +// also on disk it reports the maximum. Both searches run against a real directory. +test fn the_gallop_probes_the_int_maximum_instead_of_overflowing_by_real_execution() -> Bool { + let root = fresh_root() + let max = int_inclusive_max() + let upper = max / 2 + 1 + let w1 = Filesystem.WriteCreateNew(path: cas_file_slot_path(root: root as NonEmptyStr, key: "slot-top", generation: upper), content: "upper") + let below_max = match cas_probe_gallop(root: root as NonEmptyStr, key: "slot-top", present: upper, present_value: "upper") { + ProbedHead { generation: g, value: v } => g == upper && (v as String) == "upper" + _ => false + } + let w2 = Filesystem.WriteCreateNew(path: cas_file_slot_path(root: root as NonEmptyStr, key: "slot-top", generation: max), content: "top") + let at_max = match cas_probe_gallop(root: root as NonEmptyStr, key: "slot-top", present: upper, present_value: "upper") { + ProbedHead { generation: g, value: v } => g == max && (v as String) == "top" + _ => false + } + let removed = shell.Remove.RecursiveForce(path: root) + w1.success && w2.success && below_max && at_max && removed.success +} + // AN UNINITIALIZED STORE IS NOT AN EMPTY ONE. The slot root is missing, so the host answers // NotFound for generation 1 exactly as it would for an empty slot; the observation must refuse // rather than read "absent", and a writer expecting absence must be refused before it publishes. diff --git a/dag/test/claim/durable_cas_file_store_witness_test.dag b/dag/test/claim/durable_cas_file_store_witness_test.dag index a3cb53795aa..48ef3c7330a 100644 --- a/dag/test/claim/durable_cas_file_store_witness_test.dag +++ b/dag/test/claim/durable_cas_file_store_witness_test.dag @@ -15,8 +15,8 @@ import extdeps.filesystem.filesystem_io { } import gunbc.durable_cas_file_store { CasAttemptAdmission, CasAttemptAdmitted, CasAttemptDigestMismatch, CasAttemptDigestIncomparable, CasAttemptKeyNotSlotAddressable, - admit_cas_attempt, cas_file_slot_path, - cas_outcome_from_create, cas_probe_from_exact, cas_probe_as_observation, + admit_cas_attempt, cas_file_slot_path, observe_cas_slot_state, cas_key_not_slot_addressable_detail, + cas_outcome_from_create, cas_classify_generation_read, GenerationRefused, ProbedAbsent, cas_probe_as_observation, } // Evidence for the pure half of the file-backed CAS store. What is DELIBERATELY @@ -162,6 +162,22 @@ test fn a_key_that_would_escape_the_store_root_is_refused_at_the_mint() -> Bool } } +// THE READ VERB REFUSES THE SAME KEY, BEFORE ANY FILESYSTEM READ (review 69793 of gunbc#12000): +// a separator-carrying key on observe_cas_slot_state is unreadable with the store's own fixed +// detail, so a request-supplied identity cannot turn a read into a probe of a path outside the root +// and the answer discriminates nothing about the host. This runs hermetically precisely because no +// read happens; routing the key to the probe would fail here on the missing filesystem arm. +test fn a_key_that_would_escape_the_store_root_is_refused_at_the_read() -> Bool { + match observe_cas_slot_state(root: "/var/lib/gunbc/cas", key: "../../etc/passwd") { + CasObservedUnreadable { cause: c } => + match c { + CasUnreadableReadRefused { detail: d } => d == cas_key_not_slot_addressable_detail + _ => false + } + CasObservedReadable { readable: _ } => false + } +} + // A key with a slash that does NOT escape is still refused, because the defect // is not only traversal: the store does not create directories, so such a key // would refuse at the write with an operational error instead of being rejected @@ -260,13 +276,13 @@ test fn an_unrecognized_create_kind_is_store_refused_not_contention() -> Bool { } test fn an_unrecognized_read_kind_is_refused_as_unrecognized_not_as_other() -> Bool { - let probe = cas_probe_from_exact( - root: "/cas", - key: "slot-a", + let probe = match cas_classify_generation_read( generation: cas_generation_first(), - previous: "unread", exact: FilesystemExactPathKindUnrecognized { path: "/cas/slot-a.1", observed: "weird", error: "ignored text" }, - ) + ) { + GenerationRefused { probe: p } => p + _ => ProbedAbsent + } match cas_probe_as_observation(probe: probe) { CasObservedUnreadable { cause: c } => match c { diff --git a/dag/test/claim/durable_compare_and_set_witness_test.dag b/dag/test/claim/durable_compare_and_set_witness_test.dag index feb88df1861..60709fa44d5 100644 --- a/dag/test/claim/durable_compare_and_set_witness_test.dag +++ b/dag/test/claim/durable_compare_and_set_witness_test.dag @@ -228,3 +228,28 @@ test fn known_gap_attempt_key_unconsumed_red_here_means_the_gap_was_closed() -> committed_generation_of(outcome: for_slot_a) == 8 && committed_generation_of(outcome: for_slot_b) == 8 } + +fn occupied_at(g: CasGeneration) -> CasSlotObservation { + CasObservedReadable { readable: CasReadablePresent { version: CasSlotVersion { + generation: g, content: content_hash_of_value(value: "state" as NonEmptyStr), value: "state" as NonEmptyStr, + } } } +} + +// THE LAST GENERATION HAS NO SUCCESSOR, AND AN ADMITTED ATTEMPT AGAINST IT REFUSES AS EXHAUSTED rather +// than committing a successor that only an overflowing addition could name. The positive control is +// the generation one below: it still commits, to the maximum itself. +test fn an_attempt_against_the_last_generation_refuses_as_exhausted_and_one_below_commits_to_it() -> Bool { + let max = int_inclusive_max() + let exhausted = match cas_decide(attempt: proposal(expected: ExpectSlotGeneration { generation: max }), observed: occupied_at(g: max)) { + CasStoreRefused { cause: c } => match c { + CasGenerationSpaceExhausted { head: h } => h == max + _ => false + } + _ => false + } + let below = match cas_decide(attempt: proposal(expected: ExpectSlotGeneration { generation: max - 1 }), observed: occupied_at(g: max - 1)) { + CasCommitted { committed: v } => v.generation == max + _ => false + } + exhausted && below +} diff --git a/dag/test/fixture/approval_device_redemption/vectors.json b/dag/test/fixture/approval_device_redemption/vectors.json index d944f9e8bb1..0bc2a504f5b 100644 --- a/dag/test/fixture/approval_device_redemption/vectors.json +++ b/dag/test/fixture/approval_device_redemption/vectors.json @@ -1 +1 @@ -{"framing": "each field as :, concatenated", "redemption": [{"name": "approve-plain", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true}", "decision": "approve", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,71:{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true},7:approve,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}, {"name": "deny-plain", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true}", "decision": "deny", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,71:{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true},4:deny,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}, {"name": "approve-escapes", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"purpose\":\"Boot Mt. Collins \\\\ unit 1 — été\nline two\"}", "decision": "approve", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,55:{\"purpose\":\"Boot Mt. Collins \\\\ unit 1 — été\nline two\"},7:approve,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}], "enrolment": [{"name": "ios", "input": {"code": "482913", "platform": "ios", "point_b64url": "BHt2Zm9vYmFyYmF6cXV4"}, "expected": "27:gunbc.approval-enrolment.v1,6:482913,3:ios,20:BHt2Zm9vYmFyYmF6cXV4,"}, {"name": "android", "input": {"code": "482913", "platform": "android", "point_b64url": "BHt2Zm9vYmFyYmF6cXV4"}, "expected": "27:gunbc.approval-enrolment.v1,6:482913,7:android,20:BHt2Zm9vYmFyYmF6cXV4,"}], "read": [{"name": "pending", "input": {"path": "/approve/device/pending", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,23:/approve/device/pending,10:enr-482913,20:2026-09-18T12:00:30Z,"}, {"name": "request", "input": {"path": "/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,48:/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x,10:enr-482913,20:2026-09-18T12:00:30Z,"}, {"name": "enrollment_readback", "input": {"path": "/approve/device/enrollments/id-ZW5yLTQ4MjkxMw==", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,47:/approve/device/enrollments/id-ZW5yLTQ4MjkxMw==,10:enr-482913,20:2026-09-18T12:00:30Z,"}], "envelope": [{"name": "enrolment_request", "body": "{\"code\": \"482913\", \"platform\": \"ios\", \"decision_key\": {\"suite\": \"ECDSA-P256-SHA256\", \"encoding\": \"SEC1-uncompressed\", \"point_b64url\": \"BHt2Zm9vYmFyYmF6cXV4\"}, \"evidence\": {\"kind\": \"ios_app_attest\", \"attest_key_id\": \"attest-key-1\", \"attestation_b64\": \"o2NmbXRvYXBwbGUtYXBwYXR0ZXN0\"}, \"push\": {\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"}}"}, {"name": "signed_redemption", "body": "{\"signing_input\": {\"audience\": \"gunbc.roadmap_serve/device-redemption\", \"enrollment_id\": \"enr-7f3a\", \"challenge\": {\"expires_at\": \"2026-09-18T12:05:00Z\", \"nonce_hex\": \"9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5\"}, \"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"stored_request_text\": \"{\\\"kind\\\":\\\"request\\\",\\\"escalation_id\\\":\\\"esc-mtc1-boot-1\\\",\\\"destructive\\\":true}\", \"decision\": \"approve\", \"capability_text\": \"gunbc.approval-capability.v1\\u001Fgunbc.roadmap_serve\\u001Fgunbc.auth.approval_broker\", \"capability_tag_b64url\": \"0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=\"}, \"signature\": {\"suite\": \"ECDSA-P256-SHA256\", \"encoding\": \"P1363-fixed-width\", \"b64url\": \"c2lnbmF0dXJl\"}, \"platform_proof\": {\"kind\": \"ios_app_attest_assertion\", \"assertion_b64\": \"omlzaWduYXR1cmU\"}}"}, {"name": "push_update", "body": "{\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"}"}, {"name": "enrolment_grant", "body": "{\"enrollment_id\": \"enr-482913\"}"}, {"name": "pending_list", "body": "{\"pending\": [{\"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abab\"}]}"}, {"name": "fetched_request", "body": "{\"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abab\", \"stored_request_text\": \"{\\\"kind\\\":\\\"request\\\"}\", \"challenge\": {\"expires_at\": \"2026-09-18T12:05:00Z\", \"nonce_hex\": \"9c1d\"}, \"approve\": {\"capability_text\": \"approve-text\", \"capability_tag_b64url\": \"0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=\"}, \"deny\": {\"capability_text\": \"deny-text\", \"capability_tag_b64url\": \"DfEI-CJIvDgDxhGnedEBCKWBrsxopGkEpUqVsl6enGg=\"}}"}, {"name": "enrolment_readback", "body": "{\"enrollment_id\": \"enr-482913\", \"standing\": \"active\"}"}, {"name": "redemption_response_lost_the_race", "body": "{\"outcome\": \"DeviceLostTheRace\", \"message\": \"another decision landed first; this one changed nothing\"}"}, {"name": "redemption_response_challenge_expired", "body": "{\"outcome\": \"DeviceChallengeExpired\", \"message\": \"the challenge expired; reopen the request and decide again\"}"}, {"name": "redemption_response_signed_for_another_request", "body": "{\"outcome\": \"DeviceSignedForAnotherRequest\", \"message\": \"the signed bytes do not match the stored request: stored_request_text\"}"}, {"name": "redemption_response_enrollment_revoked", "body": "{\"outcome\": \"DeviceEnrollmentRevoked\", \"message\": \"this device's enrolment has been revoked\"}"}, {"name": "redemption_response_enrollment_unknown", "body": "{\"outcome\": \"DeviceEnrollmentUnknown\", \"message\": \"this device is not enrolled\"}"}, {"name": "push_update_client_data", "body": "29:gunbc.approval-device-push.v1,20:/approve/device/push,10:enr-482913,20:2026-09-18T12:00:30Z,98:{\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"},"}, {"name": "request_path", "body": "/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x"}, {"name": "enrollment_id_for_code_482913", "body": "enr-482913"}, {"name": "enrollment_path", "body": "/approve/device/enrollments/id-ZW5yLTQ4MjkxMw=="}], "stored_request": [{"name": "esc-mtc1-boot-1", "input": {"requester": "eager-owl-205", "purpose": "Boot Mt. Collins unit 1 once from the diskless image over BMC virtual media.", "destructive": true, "expires_at": "2026-09-17T20:00:00Z"}, "json": "{\"kind\": \"request\", \"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"attempt\": \"mtc1-boot-attempt-1\", \"requester\": \"eager-owl-205\", \"purpose\": \"Boot Mt. Collins unit 1 once from the diskless image over BMC virtual media.\", \"destructive\": true, \"issued_at\": \"2026-09-16T20:00:00Z\", \"expires_at\": \"2026-09-17T20:00:00Z\", \"key_id\": \"approval-capability-mac-key/1\"}"}, {"name": "esc-escapes-2", "input": {"requester": "wise-owl-628", "purpose": "Grant \"read\" on C:\\keys — été\nsecond line", "destructive": false, "expires_at": "2026-09-18T20:00:00Z"}, "json": "{\"kind\": \"request\", \"escalation_id\": \"esc-escapes-2\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"attempt\": \"mtc1-boot-attempt-1\", \"requester\": \"wise-owl-628\", \"purpose\": \"Grant \\\"read\\\" on C:\\\\keys — été\\nsecond line\", \"destructive\": false, \"issued_at\": \"2026-09-16T20:00:00Z\", \"expires_at\": \"2026-09-18T20:00:00Z\", \"key_id\": \"approval-capability-mac-key/1\"}"}], "surface": [{"name": "header_enrollment", "value": "X-Approval-Enrollment"}, {"name": "header_requested_at", "value": "X-Approval-Requested-At"}, {"name": "header_assertion", "value": "X-Approval-Assertion"}, {"name": "route_enrol", "value": "/approve/device/enrol"}, {"name": "route_pending", "value": "/approve/device/pending"}, {"name": "route_request_prefix", "value": "/approve/device/requests/"}, {"name": "route_redeem", "value": "/approve/device/redeem"}, {"name": "route_enrollment_prefix", "value": "/approve/device/enrollments/"}, {"name": "route_push", "value": "/approve/device/push"}], "path_segment": [{"input": "esc-mtc1_boot~1", "encoded": "id-ZXNjLW10YzFfYm9vdH4x"}, {"input": "482?913", "encoded": "id-NDgyPzkxMw=="}, {"input": "a%2Fb", "encoded": "id-YSUyRmI="}, {"input": "a#b", "encoded": "id-YSNi"}, {"input": "a/b", "encoded": "id-YS9i"}, {"input": "..", "encoded": "id-Li4="}, {"input": ".", "encoded": "id-Lg=="}, {"input": "sp ace", "encoded": "id-c3AgYWNl"}, {"input": "café", "encoded": "id-Y2Fmw6k="}, {"input": "☃", "encoded": "id-4piD"}, {"input": "🔒", "encoded": "id-8J-Ukg=="}]} +{"framing": "each field as :, concatenated", "redemption": [{"name": "approve-plain", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true}", "decision": "approve", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,71:{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true},7:approve,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}, {"name": "deny-plain", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true}", "decision": "deny", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,71:{\"kind\":\"request\",\"escalation_id\":\"esc-mtc1-boot-1\",\"destructive\":true},4:deny,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}, {"name": "approve-escapes", "input": {"audience": "gunbc.roadmap_serve/device-redemption", "enrollment_id": "enr-7f3a", "challenge_expires_at": "2026-09-18T12:05:00Z", "nonce_hex": "9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5", "escalation_id": "esc-mtc1-boot-1", "request_revision": "sha256:abababababababababababababababababababababababababababababababab", "stored_request_text": "{\"purpose\":\"Boot Mt. Collins \\\\ unit 1 — été\nline two\"}", "decision": "approve", "capability_text": "gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker", "capability_tag_b64url": "0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM="}, "expected": "28:gunbc.approval-redemption.v1,37:gunbc.roadmap_serve/device-redemption,8:enr-7f3a,20:2026-09-18T12:05:00Z,64:9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5,15:esc-mtc1-boot-1,71:sha256:abababababababababababababababababababababababababababababababab,55:{\"purpose\":\"Boot Mt. Collins \\\\ unit 1 — été\nline two\"},7:approve,75:gunbc.approval-capability.v1\u001Fgunbc.roadmap_serve\u001Fgunbc.auth.approval_broker,44:0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=,"}], "enrolment": [{"name": "ios", "input": {"code": "482913", "platform": "ios", "point_b64url": "BHt2Zm9vYmFyYmF6cXV4"}, "expected": "27:gunbc.approval-enrolment.v1,6:482913,3:ios,20:BHt2Zm9vYmFyYmF6cXV4,"}, {"name": "android", "input": {"code": "482913", "platform": "android", "point_b64url": "BHt2Zm9vYmFyYmF6cXV4"}, "expected": "27:gunbc.approval-enrolment.v1,6:482913,7:android,20:BHt2Zm9vYmFyYmF6cXV4,"}], "read": [{"name": "pending", "input": {"path": "/approve/device/pending", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,23:/approve/device/pending,10:enr-482913,20:2026-09-18T12:00:30Z,"}, {"name": "request", "input": {"path": "/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,48:/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x,10:enr-482913,20:2026-09-18T12:00:30Z,"}, {"name": "enrollment_readback", "input": {"path": "/approve/device/enrollments/id-ZW5yLTQ4MjkxMw==", "enrollment_id": "enr-482913", "requested_at": "2026-09-18T12:00:30Z"}, "expected": "29:gunbc.approval-device-read.v1,47:/approve/device/enrollments/id-ZW5yLTQ4MjkxMw==,10:enr-482913,20:2026-09-18T12:00:30Z,"}], "envelope": [{"name": "enrolment_request", "body": "{\"code\": \"482913\", \"platform\": \"ios\", \"decision_key\": {\"suite\": \"ECDSA-P256-SHA256\", \"encoding\": \"SEC1-uncompressed\", \"point_b64url\": \"BHt2Zm9vYmFyYmF6cXV4\"}, \"evidence\": {\"kind\": \"ios_app_attest\", \"attest_key_id\": \"attest-key-1\", \"attestation_b64\": \"o2NmbXRvYXBwbGUtYXBwYXR0ZXN0\"}, \"push\": {\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"}}"}, {"name": "signed_redemption", "body": "{\"signing_input\": {\"audience\": \"gunbc.roadmap_serve/device-redemption\", \"enrollment_id\": \"enr-7f3a\", \"challenge\": {\"expires_at\": \"2026-09-18T12:05:00Z\", \"nonce_hex\": \"9c1d2e3f4a5b6c7d8e9fa0b1c2d3e4f5061728394a5b6c7d8e9fa0b1c2d3e4f5\"}, \"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"stored_request_text\": \"{\\\"kind\\\":\\\"request\\\",\\\"escalation_id\\\":\\\"esc-mtc1-boot-1\\\",\\\"destructive\\\":true}\", \"decision\": \"approve\", \"capability_text\": \"gunbc.approval-capability.v1\\u001Fgunbc.roadmap_serve\\u001Fgunbc.auth.approval_broker\", \"capability_tag_b64url\": \"0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=\"}, \"signature\": {\"suite\": \"ECDSA-P256-SHA256\", \"encoding\": \"P1363-fixed-width\", \"b64url\": \"c2lnbmF0dXJl\"}, \"platform_proof\": {\"kind\": \"ios_app_attest_assertion\", \"assertion_b64\": \"omlzaWduYXR1cmU\"}}"}, {"name": "push_update", "body": "{\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"}"}, {"name": "read_authentication", "body": "{\"enrollment_id\": \"enr-482913\", \"requested_at\": \"2026-09-18T12:00:30Z\", \"assertion_b64\": \"omlzaWduYXR1cmU\"}"}, {"name": "push_update_request", "body": "{\"auth\": {\"enrollment_id\": \"enr-482913\", \"requested_at\": \"2026-09-18T12:00:30Z\", \"assertion_b64\": \"omlzaWduYXR1cmU\"}, \"push\": {\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"}}"}, {"name": "enrolment_grant", "body": "{\"enrollment_id\": \"enr-482913\"}"}, {"name": "pending_list", "body": "{\"pending\": [{\"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abab\"}]}"}, {"name": "fetched_request", "body": "{\"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abab\", \"stored_request_text\": \"{\\\"kind\\\":\\\"request\\\"}\", \"challenge\": {\"expires_at\": \"2026-09-18T12:05:00Z\", \"nonce_hex\": \"9c1d\"}, \"approve\": {\"capability_text\": \"approve-text\", \"capability_tag_b64url\": \"0fHxA0NwMC8UBb0LzXHpB8B56tW_kS2glcvhENeHZmM=\"}, \"deny\": {\"capability_text\": \"deny-text\", \"capability_tag_b64url\": \"DfEI-CJIvDgDxhGnedEBCKWBrsxopGkEpUqVsl6enGg=\"}}"}, {"name": "enrolment_readback", "body": "{\"enrollment_id\": \"enr-482913\", \"standing\": \"active\"}"}, {"name": "redemption_response_lost_the_race", "body": "{\"outcome\": \"DeviceLostTheRace\", \"message\": \"another decision landed first; this one changed nothing\"}"}, {"name": "redemption_response_challenge_expired", "body": "{\"outcome\": \"DeviceChallengeExpired\", \"message\": \"the challenge expired; reopen the request and decide again\"}"}, {"name": "redemption_response_signed_for_another_request", "body": "{\"outcome\": \"DeviceSignedForAnotherRequest\", \"message\": \"the signed bytes do not match the stored request: stored_request_text\"}"}, {"name": "redemption_response_enrollment_revoked", "body": "{\"outcome\": \"DeviceEnrollmentRevoked\", \"message\": \"this device's enrolment has been revoked\"}"}, {"name": "redemption_response_enrollment_unknown", "body": "{\"outcome\": \"DeviceEnrollmentUnknown\", \"message\": \"this device is not enrolled\"}"}, {"name": "push_update_client_data", "body": "29:gunbc.approval-device-push.v1,20:/approve/device/push,10:enr-482913,20:2026-09-18T12:00:30Z,98:{\"kind\": \"apns\", \"environment\": \"production\", \"topic\": \"ai.gunb.approve\", \"token\": \"a1b2c3d4e5f6\"},"}, {"name": "request_path", "body": "/approve/device/requests/id-ZXNjLW10YzEtYm9vdC0x"}, {"name": "enrollment_id_for_code_482913", "body": "enr-482913"}, {"name": "enrollment_path", "body": "/approve/device/enrollments/id-ZW5yLTQ4MjkxMw=="}], "stored_request": [{"name": "esc-mtc1-boot-1", "input": {"requester": "eager-owl-205", "purpose": "Boot Mt. Collins unit 1 once from the diskless image over BMC virtual media.", "destructive": true, "expires_at": "2026-09-17T20:00:00Z"}, "json": "{\"kind\": \"request\", \"escalation_id\": \"esc-mtc1-boot-1\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"attempt\": \"mtc1-boot-attempt-1\", \"requester\": \"eager-owl-205\", \"purpose\": \"Boot Mt. Collins unit 1 once from the diskless image over BMC virtual media.\", \"destructive\": true, \"issued_at\": \"2026-09-16T20:00:00Z\", \"expires_at\": \"2026-09-17T20:00:00Z\", \"key_id\": \"approval-capability-mac-key/1\"}"}, {"name": "esc-escapes-2", "input": {"requester": "wise-owl-628", "purpose": "Grant \"read\" on C:\\keys — été\nsecond line", "destructive": false, "expires_at": "2026-09-18T20:00:00Z"}, "json": "{\"kind\": \"request\", \"escalation_id\": \"esc-escapes-2\", \"request_revision\": \"sha256:abababababababababababababababababababababababababababababababab\", \"attempt\": \"mtc1-boot-attempt-1\", \"requester\": \"wise-owl-628\", \"purpose\": \"Grant \\\"read\\\" on C:\\\\keys — été\\nsecond line\", \"destructive\": false, \"issued_at\": \"2026-09-16T20:00:00Z\", \"expires_at\": \"2026-09-18T20:00:00Z\", \"key_id\": \"approval-capability-mac-key/1\"}"}], "surface": [{"name": "method_every_device_operation", "value": "POST"}, {"name": "route_enrol", "value": "/approve/device/enrol"}, {"name": "route_pending", "value": "/approve/device/pending"}, {"name": "route_request_prefix", "value": "/approve/device/requests/"}, {"name": "route_redeem", "value": "/approve/device/redeem"}, {"name": "route_enrollment_prefix", "value": "/approve/device/enrollments/"}, {"name": "route_push", "value": "/approve/device/push"}], "path_segment": [{"input": "esc-mtc1_boot~1", "encoded": "id-ZXNjLW10YzFfYm9vdH4x"}, {"input": "482?913", "encoded": "id-NDgyPzkxMw=="}, {"input": "a%2Fb", "encoded": "id-YSUyRmI="}, {"input": "a#b", "encoded": "id-YSNi"}, {"input": "a/b", "encoded": "id-YS9i"}, {"input": "..", "encoded": "id-Li4="}, {"input": ".", "encoded": "id-Lg=="}, {"input": "sp ace", "encoded": "id-c3AgYWNl"}, {"input": "café", "encoded": "id-Y2Fmw6k="}, {"input": "☃", "encoded": "id-4piD"}, {"input": "🔒", "encoded": "id-8J-Ukg=="}]} diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index a2bc996bdc0..7112f51f036 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -1117,8 +1117,13 @@ fn floor_route_gap_expectation_chunk_11() -> List { } } -// The four test.claim.durable_cas_file_store_wet_witness identities: CAS publication read-back, -// sequential loser naming the winner, generation-two advance, and a non-contention store refusal. +// The five test.claim.durable_cas_file_store_wet_witness identities: CAS publication read-back, +// sequential loser naming the winner, generation-two advance, a non-contention store refusal, and the +// head search reaching the Int maximum without overflowing -- plus the five +// test.claim.approval_assertion_counter_wet_witness_test identities (replay refused, per-enrolment +// standing, lost race refused, a 4200-generation prefix seeded through cas_file_slot_path past the +// former 4096 cliff followed by real replay and admission reads, and an append interleaved between +// the head search's reads), whose first effect is the same Mktemp. // First effect is shell.Mktemp.DirWithTemplate with no mock_response. Triple enrollment: this // expectation, WetScheduledClaim rows in local_repo_wet_schedule, and the // gunbc.ci_layer_roots witness_exclusion_frontier LocalRepoWetLane row for @@ -1134,6 +1139,18 @@ fn floor_route_gap_expectation_chunk_12() -> List { tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.a_non_contention_store_refusal_is_not_precondition_failed_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.the_gallop_probes_the_int_maximum_instead_of_overflowing_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.approval_assertion_counter_wet_witness_test.a_replayed_assertion_counter_is_refused_and_a_higher_one_admitted", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.approval_assertion_counter_wet_witness_test.the_counter_standing_is_per_enrolment", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.approval_assertion_counter_wet_witness_test.a_lost_counter_race_is_refused_not_admitted", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.approval_assertion_counter_wet_witness_test.an_enrolment_keeps_admitting_past_four_thousand_ninety_six_assertions", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { + head: FloorRouteGapExpectation { identity: "test.claim.approval_assertion_counter_wet_witness_test.an_append_landing_mid_search_yields_a_stale_real_head_and_the_stale_writer_is_refused_by_the_create", operation: "DirWithTemplate", ground: NoMockResponse {} }, + tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.a_missing_slot_root_refuses_rather_than_reading_absent_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.durable_cas_file_store_wet_witness.an_established_empty_root_reads_the_slot_absent_by_real_execution", operation: "DirWithTemplate", ground: NoMockResponse {} }, @@ -1144,6 +1161,12 @@ fn floor_route_gap_expectation_chunk_12() -> List { } } } + } + } + } + } + } + } } // V4.1 apply-seam DigestFile / DigestStdin claims (gunbc#11476, floor 35151938937). Hermetic @@ -1151,8 +1174,12 @@ fn floor_route_gap_expectation_chunk_12() -> List { // gunbc.hermetic_mock_fidelity (fabricated digest of arbitrary bytes). The real terminal is this // lane: sha256sum over committed patch paths (DigestFile) or stdin of the empty string // (DigestStdin). Sibling functions in those entries stay hermetic; they do not reach the ops. +// Plus the test.claim.approval_device_routes_wet_witness_test identity (gunbc#12000): the +// bound-realization control's enrolment-store Read. Triple enrollment: this expectation, its +// WetScheduledClaim row, and the gunbc.ci_layer_roots +// LocalRepoWetLane row for approval_device_routes_wet_witness_test.dag. fn floor_route_gap_expectation_chunk_13() -> List { - Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_row_store_encode_witness.the_receipt_was_produced_by_the_rendered_program_the_mode_ships", operation: "DigestStdin", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_engram_runtime_witness.the_live_storage_backed_patches_are_digestfile_of_committed_bytes", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_runtime_candidate_witness.observed_patches_do_not_mint_a_patched_source_tree", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_runtime_candidate_witness.the_live_candidate_is_keyed_end_to_end", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_source_patch_converge_witness.digestfile_inhabits_the_committed_patch_population", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_source_patch_converge_witness.empty_diff_has_a_real_digest", operation: "DigestStdin", ground: NoMockResponse {} }, tail: Empty {} } } } } } } + Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_row_store_encode_witness.the_receipt_was_produced_by_the_rendered_program_the_mode_ships", operation: "DigestStdin", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_engram_runtime_witness.the_live_storage_backed_patches_are_digestfile_of_committed_bytes", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_runtime_candidate_witness.observed_patches_do_not_mint_a_patched_source_tree", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_runtime_candidate_witness.the_live_candidate_is_keyed_end_to_end", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_source_patch_converge_witness.digestfile_inhabits_the_committed_patch_population", operation: "DigestFile", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.spark.v41_source_patch_converge_witness.empty_diff_has_a_real_digest", operation: "DigestStdin", ground: NoMockResponse {} }, tail: Cons { head: FloorRouteGapExpectation { identity: "test.claim.approval_device_routes_wet_witness_test.a_bound_realization_passes_the_read_past_the_gate", operation: "Read", ground: NoMockResponse {} }, tail: Empty {} } } } } } } } } // THE DECLARED-UNIT DIGEST MINT IS THE ONE ROUTE GAP THESE IDENTITIES SHARE. diff --git a/src/v2/workflow/local_repo_wet_terminal.dag b/src/v2/workflow/local_repo_wet_terminal.dag index 1039cdc9ce8..9f51339db8f 100644 --- a/src/v2/workflow/local_repo_wet_terminal.dag +++ b/src/v2/workflow/local_repo_wet_terminal.dag @@ -1397,6 +1397,48 @@ fn local_repo_wet_schedule() -> List { function: "a_non_contention_store_refusal_is_not_precondition_failed_by_real_execution", expectation: ExpectedToHold {} }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.durable_cas_file_store_wet_witness", function: "the_gallop_probes_the_int_maximum_instead_of_overflowing_by_real_execution" }, + entry: "dag/test/claim/durable_cas_file_store_wet_witness_test.dag", + function: "the_gallop_probes_the_int_maximum_instead_of_overflowing_by_real_execution", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_assertion_counter_wet_witness_test", function: "a_replayed_assertion_counter_is_refused_and_a_higher_one_admitted" }, + entry: "dag/test/claim/approval_assertion_counter_wet_witness_test.dag", + function: "a_replayed_assertion_counter_is_refused_and_a_higher_one_admitted", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_assertion_counter_wet_witness_test", function: "the_counter_standing_is_per_enrolment" }, + entry: "dag/test/claim/approval_assertion_counter_wet_witness_test.dag", + function: "the_counter_standing_is_per_enrolment", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_assertion_counter_wet_witness_test", function: "a_lost_counter_race_is_refused_not_admitted" }, + entry: "dag/test/claim/approval_assertion_counter_wet_witness_test.dag", + function: "a_lost_counter_race_is_refused_not_admitted", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_assertion_counter_wet_witness_test", function: "an_enrolment_keeps_admitting_past_four_thousand_ninety_six_assertions" }, + entry: "dag/test/claim/approval_assertion_counter_wet_witness_test.dag", + function: "an_enrolment_keeps_admitting_past_four_thousand_ninety_six_assertions", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_assertion_counter_wet_witness_test", function: "an_append_landing_mid_search_yields_a_stale_real_head_and_the_stale_writer_is_refused_by_the_create" }, + entry: "dag/test/claim/approval_assertion_counter_wet_witness_test.dag", + function: "an_append_landing_mid_search_yields_a_stale_real_head_and_the_stale_writer_is_refused_by_the_create", + expectation: ExpectedToHold {} + }, + WetScheduledClaim { + identity: WitnessIdentity { module_path: "test.claim.approval_device_routes_wet_witness_test", function: "a_bound_realization_passes_the_read_past_the_gate" }, + entry: "dag/test/claim/approval_device_routes_wet_witness_test.dag", + function: "a_bound_realization_passes_the_read_past_the_gate", + expectation: ExpectedToHold {} + }, WetScheduledClaim { identity: WitnessIdentity { module_path: "test.claim.durable_cas_file_store_wet_witness", function: "a_missing_slot_root_refuses_rather_than_reading_absent_by_real_execution" }, entry: "dag/test/claim/durable_cas_file_store_wet_witness_test.dag",