diff --git a/dag/extdeps/apple/app_attest.dag b/dag/extdeps/apple/app_attest.dag index 47823cd66cf..c947d2ec7e1 100644 --- a/dag/extdeps/apple/app_attest.dag +++ b/dag/extdeps/apple/app_attest.dag @@ -1,6 +1,22 @@ module extdeps.apple.app_attest import std.types { NonEmptyStr, String, Int } +import std.integer { UInt8 } +import std.encoding { base64_decode, base64_encode, Standard, UrlSafe } +import std.octet_span { + OctetSpan, OctetSpanReady, OctetSpanRefused, OctetUnsignedReady, OctetUnsignedRefused, OctetInputTruncated, + octet_span_read, octet_span_octets, octet_span_is, octet_span_length, octet_at, octet_in_span, octet_bit_is_set, octet_read_unsigned_be, +} +import extdeps.ietf.cbor { + CborItem, CborEntry, CborRefusal, CborMap, CborBytes, CborText, CborArray, CborUnsigned, + CborStep, CborStepped, CborStepRefused, CborDecode, CborDecoded, CborRefused, + cbor_decode, cbor_decode_item, cbor_decode_exact, cbor_max_depth, cbor_text_key_is, cbor_map_text_value, cbor_map_int_value, cbor_int_value, +} +import extdeps.ietf.x509 { + X509Refusal, X509Read, X509Ready, X509Refused, X509Certificate, X509Link, + X509ChainCheck, X509ChainStructurallyValid, X509ChainRefused, + x509_certificate, x509_chain_structure, +} import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -53,17 +69,50 @@ type AppAttestEnvironment // The server then STORES the credential public key and the receipt: the key verifies every later // assertion, and the receipt is the handle for Apple's fraud-metric call. type AttestationRefusal - = AttestationFormatUnexpected { declared: String } - | AttestationChainUntrusted { detail: String } + = AttestationMalformed { cause: AppAttestDecodeRefusal } + | AttestationFormatUnexpected + | AttestationChainUntrusted { cause: X509Refusal } | AttestationNonceMismatch | AttestationKeyIdMismatch { declared: AttestKeyId } | AttestationAppIdMismatch { expected_app_id: NonEmptyStr } | AttestationCounterNonZero { counter: Int } | AttestationEnvironmentUnexpected { expected: AppAttestEnvironment } | AttestationCredentialIdMismatch { declared: AttestKeyId } + | AttestationValidationCategoryAbsent | AttestationValidationCategoryRefused { category: Int } | AttestationBundleVersionAbsent - | AttestationUndecodable { cause: String } + | AttestationVerificationUnrealized { capability: AppAttestUnrealizedCapability } + +// What the wire decoder refuses, each located in the decoded input where a position exists. +type AppAttestDecodeRefusal + = AppAttestBase64Invalid + | AppAttestCborRefused { cause: CborRefusal } + | AppAttestFieldMissing { field: AppAttestField } + | AppAttestFieldUnexpected { field: AppAttestField } + | AppAttestUnknownField + | AppAttestAuthDataTruncated { needed: Int, available: Int } + | AppAttestAuthDataTrailing { remaining: Int } + | AppAttestAaguidUnknown + | AppAttestCredentialKeyMalformed + | AppAttestCertificateRefused { index: Int, cause: X509Refusal } + | AppAttestKeyIdNotBase64 + +type AppAttestField + = AppAttestFieldFmt + | AppAttestFieldAttStmt + | AppAttestFieldAuthData + | AppAttestFieldX5c + | AppAttestFieldReceipt + | AppAttestFieldSignature + | AppAttestFieldAuthenticatorData + | AppAttestFieldExtensions + +// The checks that need a cryptographic realization this corpus does not yet have. Each is a typed +// frontier, reported rather than skipped: ECDSA is gunbc.auth.approval_device_redemption +// ecdsa_verification_realization_frontier; SHA-256 is CRYPTO-0 (gunbc#11628). +type AppAttestUnrealizedCapability + = AppAttestEcdsaSignatureVerification + | AppAttestSha256Digest data app_attest_nonce_extension_oid: NonEmptyStr = "1.2.840.113635.100.8.2" @@ -129,7 +178,8 @@ type AssertionRefusal | AssertionAppIdMismatch { expected_app_id: NonEmptyStr } | AssertionValidationCategoryRefused { category: Int } | AssertionBundleVersionAbsent - | AssertionUndecodable { cause: String } + | AssertionMalformed { cause: AppAttestDecodeRefusal } + | AssertionVerificationUnrealized { capability: AppAttestUnrealizedCapability } type AuthenticAssertion sole_constructor { key_id: AttestKeyId @@ -154,3 +204,497 @@ fn assertion_verification_from_implementation( Absent => AssertionAuthentic { authentic: AuthenticAssertion { key_id: key_id, public_key_point_b64url: public_key_point_b64url, counter: counter, client_data: client_data } } } } + +// ── The pinned trust anchor ────────────────────────────────────────────────────────────────── +// Apple App Attestation Root CA (P-384, valid 2020-03-18 to 2045-03-15), DER, base64. SHA-256 +// fingerprint 1C:B9:82:3B:A2:8B:A6:AD:2D:33:A0:06:94:1D:E2:AE:4F:51:3E:F1:D4:E8:31:B9:F7:E0:FA:7B:62:42:C9:32, +// as published by Apple (www.apple.com/certificateauthority/Apple_App_Attestation_Root_CA.pem). +// THIS ROW IS THE PIN: the production verifier takes no anchor argument, so nothing a caller or an +// attestation supplies can stand in for it. +data apple_app_attestation_root_ca_der_b64: String = "MIICITCCAaegAwIBAgIQC/O+DvHN0uD7jG5yH2IXmDAKBggqhkjOPQQDAzBSMSYwJAYDVQQDDB1BcHBsZSBBcHAgQXR0ZXN0YXRpb24gUm9vdCBDQTETMBEGA1UECgwKQXBwbGUgSW5jLjETMBEGA1UECAwKQ2FsaWZvcm5pYTAeFw0yMDAzMTgxODMyNTNaFw00NTAzMTUwMDAwMDBaMFIxJjAkBgNVBAMMHUFwcGxlIEFwcCBBdHRlc3RhdGlvbiBSb290IENBMRMwEQYDVQQKDApBcHBsZSBJbmMuMRMwEQYDVQQIDApDYWxpZm9ybmlhMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAERTHhmLW07ATaFQIEVwTtT4dyctdhNbJhFs/Ii2FdCgAHGbpphY3+d8qjuDngIN3WVhQUBHAoMeQ/cLiP1sOUtgjqK9auYen1mMEvRq9Sk3Jm5X8U62H+xTD3FE9TgS41o0IwQDAPBgNVHRMBAf8EBTADAQH/MB0GA1UdDgQWBBSskRBTM72+aEH/pwyp5frq5eWKoTAOBgNVHQ8BAf8EBAMCAQYwCgYIKoZIzj0EAwMDaAAwZQIwQgFGnByvsiVbpTKwSga0kP0e8EeDS4+sQmTvb7vn53O5+FRXgeLhpJ06ysC5PrOyAjEAp5U4xDgEgllF7En3VcE3iexZZtKeYnpqtijVoyFraWVIyd/dganmrduC1bmTBGwD" + +// ── Wire keys, as the octets Apple's CBOR carries ──────────────────────────────────────────── +data app_attest_wire_fmt: List = [102, 109, 116] +data app_attest_wire_att_stmt: List = [97, 116, 116, 83, 116, 109, 116] +data app_attest_wire_auth_data: List = [97, 117, 116, 104, 68, 97, 116, 97] +data app_attest_wire_x5c: List = [120, 53, 99] +data app_attest_wire_receipt: List = [114, 101, 99, 101, 105, 112, 116] +data app_attest_wire_apple_appattest: List = [97, 112, 112, 108, 101, 45, 97, 112, 112, 97, 116, 116, 101, 115, 116] +data app_attest_wire_signature: List = [115, 105, 103, 110, 97, 116, 117, 114, 101] +data app_attest_wire_authenticator_data: List = [97, 117, 116, 104, 101, 110, 116, 105, 99, 97, 116, 111, 114, 68, 97, 116, 97] +data app_attest_wire_aaguid_development: List = [97, 112, 112, 97, 116, 116, 101, 115, 116, 100, 101, 118, 101, 108, 111, 112] +data app_attest_wire_aaguid_production: List = [97, 112, 112, 97, 116, 116, 101, 115, 116, 0, 0, 0, 0, 0, 0, 0] +data app_attest_wire_validation_category: List = [97, 112, 112, 108, 101, 95, 118, 97, 108, 105, 100, 97, 116, 105, 111, 110, 95, 99, 97, 116, 101, 103, 111, 114, 121, 95, 48, 49] + +// ── Authenticator data (WebAuthn Level 2, 6.1) ────────────────────────────────────────────── +// rpIdHash (32) | flags (1) | signCount (4, big-endian) | [attested credential data, when flag AT +// (bit 6): aaguid (16) | credentialIdLength (2) | credentialId | credentialPublicKey (COSE, CBOR)] +// | [extensions (CBOR map), when flag ED (bit 7)]. The structure must end exactly at the byte +// string's end; anything left over is refused rather than ignored. + +type AppAttestCredential { + aaguid: OctetSpan + credential_id: OctetSpan + x: OctetSpan + y: OctetSpan +} + +type AppAttestAuthData { + whole: OctetSpan + rp_id_hash: OctetSpan + counter: Int + credential: AppAttestCredential? + extensions: List? +} + +type AppAttestAuthDataRead + = AppAttestAuthDataReady { value: AppAttestAuthData } + | AppAttestAuthDataRefused { cause: AppAttestDecodeRefusal } + +fn app_attest_truncated(input: List, at: Int, needed: Int) -> AppAttestDecodeRefusal { + AppAttestAuthDataTruncated { needed: needed, available: count(input) - at } +} + +// COSE_Key for ES256 (RFC 9053 7.1.1): { 1: 2 (EC2), 3: -7 (ES256), -1: 1 (P-256), -2: x, -3: y }, +// x and y 32 octets each. +fn app_attest_cose_coordinate(entries: List, label: Int) -> OctetSpan? { + match cbor_map_int_value(entries: entries, label: label) { + Present { value: CborBytes { span: s } } => if octet_span_length(span: s) == 32 { Present { value: s } } else { none } + _ => none + } +} + +fn app_attest_cose_label_is(entries: List, label: Int, expected: Int) -> Bool { + match cbor_map_int_value(entries: entries, label: label) { + Present { value: item } => + match cbor_int_value(item: item) { + Present { value: v } => v == expected + Absent => false + } + Absent => false + } +} + +fn app_attest_cose_key(entries: List, aaguid: OctetSpan, credential_id: OctetSpan) -> AppAttestCredential? { + if count(entries) != 5 + || !app_attest_cose_label_is(entries: entries, label: 1, expected: 2) + || !app_attest_cose_label_is(entries: entries, label: 3, expected: 0 - 7) + || !app_attest_cose_label_is(entries: entries, label: 0 - 1, expected: 1) { + none + } else { + match app_attest_cose_coordinate(entries: entries, label: 0 - 2) { + Absent => none + Present { value: x } => + match app_attest_cose_coordinate(entries: entries, label: 0 - 3) { + Absent => none + Present { value: y } => Present { value: AppAttestCredential { aaguid: aaguid, credential_id: credential_id, x: x, y: y } } + } + } + } +} + +type AppAttestTail { + credential: AppAttestCredential? + next: Int +} + +type AppAttestTailRead + = AppAttestTailReady { value: AppAttestTail } + | AppAttestTailRefused { cause: AppAttestDecodeRefusal } + +fn app_attest_credential_data(input: List, at: Int) -> AppAttestTailRead { + match octet_span_read(input: input, at: at, length: 16) { + OctetSpanRefused { cause: _ } => AppAttestTailRefused { cause: app_attest_truncated(input: input, at: at, needed: 18) } + OctetSpanReady { span: aaguid } => + match octet_read_unsigned_be(input: input, at: aaguid.end, octets: 2) { + OctetUnsignedRefused { cause: _ } => AppAttestTailRefused { cause: app_attest_truncated(input: input, at: aaguid.end, needed: 2) } + OctetUnsignedReady { value: id_length, end: id_start } => + match octet_span_read(input: input, at: id_start, length: id_length) { + OctetSpanRefused { cause: _ } => AppAttestTailRefused { cause: app_attest_truncated(input: input, at: id_start, needed: id_length) } + OctetSpanReady { span: credential_id } => + match cbor_decode_item(input: input, at: credential_id.end, depth: cbor_max_depth) { + CborStepRefused { cause: c } => AppAttestTailRefused { cause: AppAttestCborRefused { cause: c } } + CborStepped { item: CborMap { entries: entries }, end: key_end } => + match app_attest_cose_key(entries: entries, aaguid: aaguid, credential_id: credential_id) { + Absent => AppAttestTailRefused { cause: AppAttestCredentialKeyMalformed } + Present { value: credential } => AppAttestTailReady { value: AppAttestTail { credential: Present { value: credential }, next: key_end } } + } + CborStepped { item: _, end: _ } => AppAttestTailRefused { cause: AppAttestCredentialKeyMalformed } + } + } + } + } +} + +fn app_attest_auth_data_extensions(input: List, span: OctetSpan, rp_id_hash: OctetSpan, counter: Int, tail: AppAttestTail, has_extensions: Bool) -> AppAttestAuthDataRead { + if has_extensions { + match cbor_decode_exact(input: input, at: tail.next, end: span.end) { + CborRefused { cause: c } => AppAttestAuthDataRefused { cause: AppAttestCborRefused { cause: c } } + CborDecoded { item: CborMap { entries: entries } } => + AppAttestAuthDataReady { value: AppAttestAuthData { whole: span, rp_id_hash: rp_id_hash, counter: counter, credential: tail.credential, extensions: Present { value: entries } } } + CborDecoded { item: _ } => AppAttestAuthDataRefused { cause: AppAttestFieldUnexpected { field: AppAttestFieldExtensions } } + } + } else if tail.next != span.end { + AppAttestAuthDataRefused { cause: AppAttestAuthDataTrailing { remaining: span.end - tail.next } } + } else { + AppAttestAuthDataReady { value: AppAttestAuthData { whole: span, rp_id_hash: rp_id_hash, counter: counter, credential: tail.credential, extensions: none } } + } +} + +// Authenticator data occupying `span` of `input` (the byte string's own extent). An ATTESTATION +// carries attested credential data and says so with flag AT. An ASSERTION's authenticator data is +// the fixed 37-octet header plus any extensions and carries no credential data -- yet Apple sets AT +// on it anyway: the genuine device assertion in test.claim.app_attest_parse_witness_test is 37 +// octets with flags 0x40. So whether credential data is read is the CALLER'S fact (which object this +// is), not inferred from AT, and an assertion that did carry more octets refuses as trailing. +fn app_attest_auth_data(input: List, span: OctetSpan, reads_credential: Bool) -> AppAttestAuthDataRead { + if octet_span_length(span: span) < 37 { + AppAttestAuthDataRefused { cause: AppAttestAuthDataTruncated { needed: 37, available: octet_span_length(span: span) } } + } else { + let rp_id_hash = OctetSpan { start: span.start, end: span.start + 32 } + match octet_in_span(input: input, span: span, at: span.start + 32) { + Absent => AppAttestAuthDataRefused { cause: AppAttestAuthDataTruncated { needed: 37, available: 32 } } + Present { value: flags } => + match octet_read_unsigned_be(input: input, at: span.start + 33, octets: 4) { + OctetUnsignedRefused { cause: _ } => AppAttestAuthDataRefused { cause: AppAttestAuthDataTruncated { needed: 37, available: 33 } } + OctetUnsignedReady { value: counter, end: after_counter } => { + let attested = reads_credential && octet_bit_is_set(octet: flags, bit: 6) + let has_extensions = octet_bit_is_set(octet: flags, bit: 7) + let bounded = input.take(n: span.end) + if attested { + match app_attest_credential_data(input: bounded, at: after_counter) { + AppAttestTailRefused { cause: c } => AppAttestAuthDataRefused { cause: c } + AppAttestTailReady { value: tail } => + app_attest_auth_data_extensions(input: bounded, span: span, rp_id_hash: rp_id_hash, counter: counter, tail: tail, has_extensions: has_extensions) + } + } else { + app_attest_auth_data_extensions( + input: bounded, span: span, rp_id_hash: rp_id_hash, counter: counter, + tail: AppAttestTail { credential: none, next: after_counter }, has_extensions: has_extensions, + ) + } + } + } + } + } +} + +// ── The attestation object ─────────────────────────────────────────────────────────────────── + +type AppAttestAttestationObject { + input: List + certificates: List + receipt: OctetSpan + auth_data: AppAttestAuthData +} + +type AppAttestAttestationRead + = AppAttestAttestationReady { value: AppAttestAttestationObject } + | AppAttestAttestationRefused { cause: AttestationRefusal } + +fn app_attest_malformed(cause: AppAttestDecodeRefusal) -> AppAttestAttestationRead { + AppAttestAttestationRefused { cause: AttestationMalformed { cause: cause } } +} + +// Every key of a protocol map must be one the protocol names: an unknown key is refused, because +// accepting it would let two different objects verify as one. +fn app_attest_keys_are(input: List, entries: List, known: List>) -> Bool { + all(entries, e => any(known, k => cbor_text_key_is(input: input, key: e.key, expected: k))) +} + +fn app_attest_byte_strings(items: List) -> List? { + fold(items, init: Present { value: [] }, f: (acc, item) => + match acc { + Absent => none + Present { value: spans } => + match item { + CborBytes { span: s } => Present { value: spans |> list_push(s) } + _ => none + } + }) +} + +fn app_attest_statement(input: List, statement: CborItem, auth_data: OctetSpan) -> AppAttestAttestationRead { + match statement { + CborMap { entries: entries } => + if !app_attest_keys_are(input: input, entries: entries, known: [app_attest_wire_x5c, app_attest_wire_receipt]) { + app_attest_malformed(cause: AppAttestUnknownField) + } else { + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_x5c) { + Absent => app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldX5c }) + Present { value: CborArray { items: certs } } => + match app_attest_byte_strings(items: certs) { + Absent => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldX5c }) + Present { value: cert_spans } => + if count(cert_spans) == 0 { + app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldX5c }) + } else { + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_receipt) { + Absent => app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldReceipt }) + Present { value: CborBytes { span: receipt } } => + match app_attest_auth_data(input: input, span: auth_data, reads_credential: true) { + AppAttestAuthDataRefused { cause: c } => app_attest_malformed(cause: c) + AppAttestAuthDataReady { value: ad } => + AppAttestAttestationReady { value: AppAttestAttestationObject { input: input, certificates: cert_spans, receipt: receipt, auth_data: ad } } + } + Present { value: _ } => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldReceipt }) + } + } + } + Present { value: _ } => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldX5c }) + } + } + _ => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldAttStmt }) + } +} + +// { fmt: "apple-appattest", attStmt: { x5c: [leaf, intermediate, ...], receipt }, authData }. +// The whole input must be this one map (CborTrailingInput otherwise), with no duplicate or unknown +// key at either level. +fn app_attest_attestation_object(input: List) -> AppAttestAttestationRead { + match cbor_decode(input: input) { + CborRefused { cause: c } => app_attest_malformed(cause: AppAttestCborRefused { cause: c }) + CborDecoded { item: CborMap { entries: entries } } => + if !app_attest_keys_are(input: input, entries: entries, known: [app_attest_wire_fmt, app_attest_wire_att_stmt, app_attest_wire_auth_data]) { + app_attest_malformed(cause: AppAttestUnknownField) + } else { + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_fmt) { + Absent => app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldFmt }) + Present { value: CborText { span: fmt } } => + if !octet_span_is(input: input, span: fmt, expected: app_attest_wire_apple_appattest) { + AppAttestAttestationRefused { cause: AttestationFormatUnexpected } + } else { + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_auth_data) { + Absent => app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldAuthData }) + Present { value: CborBytes { span: auth_data } } => + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_att_stmt) { + Absent => app_attest_malformed(cause: AppAttestFieldMissing { field: AppAttestFieldAttStmt }) + Present { value: statement } => app_attest_statement(input: input, statement: statement, auth_data: auth_data) + } + Present { value: _ } => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldAuthData }) + } + } + Present { value: _ } => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldFmt }) + } + } + CborDecoded { item: _ } => app_attest_malformed(cause: AppAttestFieldUnexpected { field: AppAttestFieldAttStmt }) + } +} + +// ── The chain ──────────────────────────────────────────────────────────────────────────────── + +type AppAttestChainRead + = AppAttestChainReady { links: List } + | AppAttestChainRefused { cause: AttestationRefusal } + +// Each x5c entry is its own DER certificate filling its byte string exactly. +fn app_attest_chain_links(input: List, spans: List, index: Int, acc: List) -> AppAttestChainRead { + match spans |> get(index) { + Absent => AppAttestChainReady { links: acc } + Present { value: span } => { + let cert_input = octet_span_octets(input: input, span: span) + match x509_certificate(input: cert_input, span: OctetSpan { start: 0, end: count(cert_input) }) { + X509Refused { cause: c } => AppAttestChainRefused { cause: AttestationMalformed { cause: AppAttestCertificateRefused { index: index, cause: c } } } + X509Ready { certificate: cert } => + app_attest_chain_links(input: input, spans: spans, index: index + 1, acc: acc |> list_push(X509Link { input: cert_input, certificate: cert })) + } + } + } +} + +type AppAttestAnchorRead + = AppAttestAnchorReady { link: X509Link } + | AppAttestAnchorRefused { cause: X509Refusal } + +fn app_attest_pinned_anchor() -> AppAttestAnchorRead? { + match base64_decode(s: apple_app_attestation_root_ca_der_b64, variant: Standard) { + Absent => none + Present { value: der } => + match x509_certificate(input: der, span: OctetSpan { start: 0, end: count(der) }) { + X509Refused { cause: c } => Present { value: AppAttestAnchorRefused { cause: c } } + X509Ready { certificate: cert } => Present { value: AppAttestAnchorReady { link: X509Link { input: der, certificate: cert } } } + } + } +} + +// ── The verifier ───────────────────────────────────────────────────────────────────────────── +// Apple's launch extensions (steps 9 and 10) are absent from objects produced before iOS 17, so +// whether their absence refuses is the CALLER'S policy, stated at the call rather than assumed. +type AppAttestLaunchExtensionPolicy + = LaunchExtensionsRequired + | LaunchExtensionsOptional + +fn app_attest_environment_of(input: List, aaguid: OctetSpan) -> AppAttestEnvironment? { + if octet_span_is(input: input, span: aaguid, expected: app_attest_wire_aaguid_development) { + Present { value: AppAttestDevelopment } + } else if octet_span_is(input: input, span: aaguid, expected: app_attest_wire_aaguid_production) { + Present { value: AppAttestProduction } + } else { + none + } +} + +fn app_attest_same_environment(a: AppAttestEnvironment, b: AppAttestEnvironment) -> Bool { + match a { + AppAttestDevelopment => match b { AppAttestDevelopment => true _ => false } + AppAttestProduction => match b { AppAttestProduction => true _ => false } + } +} + +// Step 9 over the extensions CBOR: the category, when present, must be admitted; when absent, the +// caller's policy decides. +fn app_attest_category_check(obj: AppAttestAttestationObject, policy: AppAttestLaunchExtensionPolicy, admitted_categories: List) -> AttestationRefusal? { + let category = match obj.auth_data.extensions { + Absent => none + Present { value: entries } => + match cbor_map_text_value(input: obj.input, entries: entries, key: app_attest_wire_validation_category) { + Present { value: CborUnsigned { value: c } } => Present { value: c } + _ => none + } + } + match category { + Present { value: c } => + if any(admitted_categories, a => a == c) { none } else { Present { value: AttestationValidationCategoryRefused { category: c } } } + Absent => + match policy { + LaunchExtensionsRequired => Present { value: AttestationValidationCategoryAbsent } + LaunchExtensionsOptional => none + } + } +} + +// Steps decidable without cryptography, in Apple's order: 1 (the chain's structure under the pinned +// root), 6 (counter), 7 (environment), 8 (credential id equals the key id), 9 (category). Steps 2-5 +// need SHA-256 and step 1's signatures need ECDSA; they are not skipped -- when every decidable step +// passes, the verifier refuses naming the first capability it could not exercise. +fn app_attest_decidable_steps( + obj: AppAttestAttestationObject, + links: List, + anchor: X509Link, + environment: AppAttestEnvironment, + key_id: AttestKeyId, + policy: AppAttestLaunchExtensionPolicy, + admitted_categories: List, + now_epoch: Int, +) -> AttestationRefusal { + match x509_chain_structure(chain: links, anchor: anchor, now: now_epoch, leaf_handled: []) { + X509ChainRefused { cause: c } => AttestationChainUntrusted { cause: c } + X509ChainStructurallyValid => + if obj.auth_data.counter != 0 { + AttestationCounterNonZero { counter: obj.auth_data.counter } + } else { + match obj.auth_data.credential { + Absent => AttestationMalformed { cause: AppAttestFieldMissing { field: AppAttestFieldAuthData } } + Present { value: credential } => + match app_attest_environment_of(input: obj.input, aaguid: credential.aaguid) { + Absent => AttestationMalformed { cause: AppAttestAaguidUnknown } + Present { value: observed } => + if !app_attest_same_environment(a: observed, b: environment) { + AttestationEnvironmentUnexpected { expected: environment } + } else { + match base64_decode(s: key_id as String, variant: Standard) { + Absent => AttestationMalformed { cause: AppAttestKeyIdNotBase64 } + Present { value: key_octets } => + if octet_span_octets(input: obj.input, span: credential.credential_id) != key_octets { + AttestationCredentialIdMismatch { declared: key_id } + } else { + match app_attest_category_check(obj: obj, policy: policy, admitted_categories: admitted_categories) { + Present { value: r } => r + Absent => AttestationVerificationUnrealized { capability: AppAttestEcdsaSignatureVerification } + } + } + } + } + } + } + } + } +} + +// THE PRODUCTION VERIFIER. It decodes the attestation for real and runs every decidable step; it +// cannot answer AttestationVerified until ECDSA is realized, and it does not pretend to: the only +// constructor of a verified attestation remains attestation_verification_from_implementation, +// which this function reaches only when every step, signatures included, has passed. +fn app_attest_verify( + environment: AppAttestEnvironment, + policy: AppAttestLaunchExtensionPolicy, + admitted_categories: List, + attestation_b64: NonEmptyStr, + key_id: AttestKeyId, + now_epoch: Int, +) -> AttestationVerification { + match base64_decode(s: attestation_b64 as String, variant: Standard) { + Absent => AttestationRefused { cause: AttestationMalformed { cause: AppAttestBase64Invalid } } + Present { value: decoded } => + match app_attest_attestation_object(input: decoded) { + AppAttestAttestationRefused { cause: c } => AttestationRefused { cause: c } + AppAttestAttestationReady { value: obj } => + match app_attest_chain_links(input: decoded, spans: obj.certificates, index: 0, acc: []) { + AppAttestChainRefused { cause: c } => AttestationRefused { cause: c } + AppAttestChainReady { links: links } => + match app_attest_pinned_anchor() { + Absent => AttestationRefused { cause: AttestationMalformed { cause: AppAttestBase64Invalid } } + Present { value: AppAttestAnchorRefused { cause: c } } => AttestationRefused { cause: AttestationChainUntrusted { cause: c } } + Present { value: AppAttestAnchorReady { link: anchor } } => + AttestationRefused { + cause: app_attest_decidable_steps( + obj: obj, links: links, anchor: anchor, environment: environment, key_id: key_id, + policy: policy, admitted_categories: admitted_categories, now_epoch: now_epoch, + ) + } + } + } + } + } +} + +// ── Assertions ─────────────────────────────────────────────────────────────────────────────── +// { signature: bstr, authenticatorData: bstr }, nothing else. Apple's step 1 (clientDataHash) is the +// first step and needs SHA-256, so after a real decode the assertion refuses at that frontier. + +type AppAttestAssertionObject { + input: List + signature: OctetSpan + auth_data: AppAttestAuthData +} + +type AppAttestAssertionRead + = AppAttestAssertionReady { value: AppAttestAssertionObject } + | AppAttestAssertionRefused { cause: AppAttestDecodeRefusal } + +fn app_attest_assertion_object(input: List) -> AppAttestAssertionRead { + match cbor_decode(input: input) { + CborRefused { cause: c } => AppAttestAssertionRefused { cause: AppAttestCborRefused { cause: c } } + CborDecoded { item: CborMap { entries: entries } } => + if !app_attest_keys_are(input: input, entries: entries, known: [app_attest_wire_signature, app_attest_wire_authenticator_data]) { + AppAttestAssertionRefused { cause: AppAttestUnknownField } + } else { + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_signature) { + Present { value: CborBytes { span: signature } } => + match cbor_map_text_value(input: input, entries: entries, key: app_attest_wire_authenticator_data) { + Present { value: CborBytes { span: ad_span } } => + match app_attest_auth_data(input: input, span: ad_span, reads_credential: false) { + AppAttestAuthDataRefused { cause: c } => AppAttestAssertionRefused { cause: c } + AppAttestAuthDataReady { value: ad } => AppAttestAssertionReady { value: AppAttestAssertionObject { input: input, signature: signature, auth_data: ad } } + } + Present { value: _ } => AppAttestAssertionRefused { cause: AppAttestFieldUnexpected { field: AppAttestFieldAuthenticatorData } } + Absent => AppAttestAssertionRefused { cause: AppAttestFieldMissing { field: AppAttestFieldAuthenticatorData } } + } + Present { value: _ } => AppAttestAssertionRefused { cause: AppAttestFieldUnexpected { field: AppAttestFieldSignature } } + Absent => AppAttestAssertionRefused { cause: AppAttestFieldMissing { field: AppAttestFieldSignature } } + } + } + CborDecoded { item: _ } => AppAttestAssertionRefused { cause: AppAttestFieldUnexpected { field: AppAttestFieldSignature } } + } +} + +fn app_attest_verify_assertion(assertion_b64: NonEmptyStr) -> AssertionVerification { + match base64_decode(s: assertion_b64 as String, variant: Standard) { + Absent => AssertionRefused { cause: AssertionMalformed { cause: AppAttestBase64Invalid } } + Present { value: decoded } => + match app_attest_assertion_object(input: decoded) { + AppAttestAssertionRefused { cause: c } => AssertionRefused { cause: AssertionMalformed { cause: c } } + AppAttestAssertionReady { value: _ } => AssertionRefused { cause: AssertionVerificationUnrealized { capability: AppAttestSha256Digest } } + } + } +} diff --git a/dag/extdeps/cloud/gcp/secret_manager.dag b/dag/extdeps/cloud/gcp/secret_manager.dag index 5b660d95f61..3ae1af0dc91 100644 --- a/dag/extdeps/cloud/gcp/secret_manager.dag +++ b/dag/extdeps/cloud/gcp/secret_manager.dag @@ -1,7 +1,7 @@ module extdeps.cloud.gcp.secret_manager import std.encoding { Standard, base64_decode, base64_encode, utf8_decode_bytes } -import std.bytes { bytes_octets, octets_bytes, utf8_encode_bytes } +import std.bytes { bytes_octets, octets_bytes, utf8_encode_bytes, pure_dag_seam_unreachable_string } import extdeps.cloud.gcp.iam { GcpBinding, GcpPolicy } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -199,11 +199,25 @@ fn sm_resolved_version_identity_is_well_formed(name: String) -> Bool { } } +// base64_encode gained a refusal channel when NUMERIC-BIT-0 (gunbc#11627) routed its packing +// through std.machine_word: it refuses an octet outside the byte range, where it previously +// multiplied one into a plausible wrong string. THE ARM IS UNREACHABLE HERE, and that is a +// statement about this call and not about base64_encode: the octets are the UTF-8 encoding of a +// String, so every member is a byte by construction and no in-range input can reach the refusal. +// An unreachable arm still has to answer, and "" is a valid base64 encoding -- of the empty +// credential -- so returning it would conflate a refusal with a real answer at a secret-provisioning +// boundary. std.bytes' divergent seam is the corpus's declared idiom for an arm that cannot be +// reached; it diverges rather than fabricating, which is the loud half of DESIGN section 5. +// This function's signature is deliberately unchanged: threading an Optional to the two actuators +// that call it would put a refusal channel where no refusal can arise. fn encode_sm_access_version_payload_wire(credential: Secret) -> String { - base64_encode( + match base64_encode( octets: bytes_octets(b: utf8_encode_bytes(s: credential as String)), variant: Standard - ) + ) { + Present { value: wire } => wire + Absent => pure_dag_seam_unreachable_string() + } } fn decode_sm_access_version_payload_wire(data_b64: String) -> SmAccessVersionPayloadDecodeOutcome { diff --git a/dag/extdeps/ietf/cbor.dag b/dag/extdeps/ietf/cbor.dag new file mode 100644 index 00000000000..29c6c81b1fc --- /dev/null +++ b/dag/extdeps/ietf/cbor.dag @@ -0,0 +1,315 @@ +module extdeps.ietf.cbor + +import std.integer { UInt8 } +import std.octet_span { + OctetSpan, OctetReadRefusal, OctetInputTruncated, OctetUnsignedTooWide, OctetWordRefused, + OctetUnsignedRead, OctetUnsignedReady, OctetUnsignedRefused, + OctetSpanRead, OctetSpanReady, OctetSpanRefused, + octet_at, octet_bit_field, octet_read_unsigned_be, octet_span_read, octet_span_equals, octet_span_is, +} +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// CBOR, RFC 8949 (Concise Binary Object Representation), as a total decoder over one octet input. +// +// Only what a named consumer decodes is modeled: App Attest attestation and assertion objects, their +// COSE credential keys and authenticator-data extensions (extdeps.apple.app_attest). Every data item +// is decoded structurally; strings are carried as spans into the input rather than copied, so a +// consumer compares or re-reads the exact wire octets. +// +// The accepted form is RFC 8949 section 4.2.1's deterministic encoding, and every departure from it +// is its own refusal rather than a best-effort reading, because a protocol that verifies bytes must +// not accept two encodings of one value: +// * an argument not in its shortest form -> CborNoncanonicalArgument +// * an indefinite-length string, array or map -> CborIndefiniteLengthUnsupported +// * additional information 28-30 (reserved, 3.1) -> CborReservedAdditionalInfo +// * a map with two equal keys (5.6) -> CborDuplicateMapKey +// * octets left over after the top-level item -> CborTrailingInput +// Floats and simple values other than false/true/null have no consumer and refuse as unsupported. +// An 8-octet argument refuses as too wide: std.machine_word does not yet realize 64-bit words, and +// no consumed App Attest field needs one. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.rfc-editor.org/rfc/rfc8949" + } +} + +type CborEntry { + key: CborItem + key_encoding: OctetSpan + value: CborItem +} + +type CborItem + = CborUnsigned { value: Int } + | CborNegative { argument: Int } + | CborBytes { span: OctetSpan } + | CborText { span: OctetSpan } + | CborArray { items: List } + | CborMap { entries: List } + | CborTagged { tag: Int, item: CborItem } + | CborFalse + | CborTrue + | CborNull + +type CborRefusal + = CborTruncated { at: Int, needed: Int, available: Int } + | CborReservedAdditionalInfo { at: Int, info: Int } + | CborIndefiniteLengthUnsupported { at: Int } + | CborNoncanonicalArgument { at: Int } + | CborArgumentTooWide { at: Int } + | CborSimpleValueUnsupported { at: Int, info: Int } + | CborDuplicateMapKey { at: Int } + | CborTrailingInput { at: Int, remaining: Int } + | CborNestingExhausted { at: Int } + +// One decoded item and the offset just past it. +type CborStep + = CborStepped { item: CborItem, end: Int } + | CborStepRefused { cause: CborRefusal } + +type CborDecode + = CborDecoded { item: CborItem } + | CborRefused { cause: CborRefusal } + +// Nesting bound. Every item consumes at least one octet, so the recursion also descends on the +// input; the depth bound makes the refusal for pathological nesting a named arm, not a stack. +data cbor_max_depth: Int = 16 + +type CborHead { + major: Int + argument: Int + end: Int +} + +type CborHeadRead + = CborHeadReady { head: CborHead } + | CborHeadIndefinite { major: Int } + | CborHeadSimple { info: Int, end: Int } + | CborHeadRefused { cause: CborRefusal } + +fn cbor_refusal_of_octet_read(cause: OctetReadRefusal) -> CborRefusal { + match cause { + OctetInputTruncated { at: a, needed: n, available: v } => CborTruncated { at: a, needed: n, available: v } + OctetUnsignedTooWide { at: a, octets: _ } => CborArgumentTooWide { at: a } + OctetWordRefused { at: a } => CborArgumentTooWide { at: a } + } +} + +// The smallest argument each extended form may carry (RFC 8949 4.2.1 preferred serialization). +fn cbor_extended_minimum(octets: Int) -> Int { + if octets == 1 { 24 } else if octets == 2 { 256 } else { 65536 } +} + +fn cbor_extended_octets(info: Int) -> Int { + if info == 24 { 1 } else if info == 25 { 2 } else if info == 26 { 4 } else { 8 } +} + +// The initial byte and its argument: major type = the top 3 bits, additional information = the low +// 5, both read through std.octet_span's machine-word bit field. +fn cbor_read_head(input: List, at: Int) -> CborHeadRead { + match octet_at(input: input, at: at) { + Absent => CborHeadRefused { cause: CborTruncated { at: at, needed: 1, available: 0 } } + Present { value: initial } => + match octet_bit_field(octet: initial, shift: 5, mask: 7) { + Absent => CborHeadRefused { cause: CborArgumentTooWide { at: at } } + Present { value: major } => + match octet_bit_field(octet: initial, shift: 0, mask: 31) { + Absent => CborHeadRefused { cause: CborArgumentTooWide { at: at } } + Present { value: info } => cbor_read_argument(input: input, at: at, major: major, info: info) + } + } + } +} + +fn cbor_read_argument(input: List, at: Int, major: Int, info: Int) -> CborHeadRead { + if info >= 28 && info <= 30 { + CborHeadRefused { cause: CborReservedAdditionalInfo { at: at, info: info } } + } else if major == 7 && info >= 20 && info != 24 && info != 31 { + CborHeadSimple { info: info, end: at + 1 } + } else if info < 24 { + CborHeadReady { head: CborHead { major: major, argument: info, end: at + 1 } } + } else if info == 31 { + CborHeadIndefinite { major: major } + } else { + let octets = cbor_extended_octets(info: info) + match octet_read_unsigned_be(input: input, at: at + 1, octets: octets) { + OctetUnsignedRefused { cause: c } => CborHeadRefused { cause: cbor_refusal_of_octet_read(cause: c) } + OctetUnsignedReady { value: v, end: e } => + if v < cbor_extended_minimum(octets: octets) { + CborHeadRefused { cause: CborNoncanonicalArgument { at: at } } + } else if major == 7 { + CborHeadRefused { cause: CborSimpleValueUnsupported { at: at, info: info } } + } else { + CborHeadReady { head: CborHead { major: major, argument: v, end: e } } + } + } + } +} + +fn cbor_simple_item(at: Int, info: Int, end: Int) -> CborStep { + if info == 20 { + CborStepped { item: CborFalse, end: end } + } else if info == 21 { + CborStepped { item: CborTrue, end: end } + } else if info == 22 { + CborStepped { item: CborNull, end: end } + } else { + CborStepRefused { cause: CborSimpleValueUnsupported { at: at, info: info } } + } +} + +fn cbor_decode_item(input: List, at: Int, depth: Int) -> CborStep { + if depth <= 0 { + CborStepRefused { cause: CborNestingExhausted { at: at } } + } else { + match cbor_read_head(input: input, at: at) { + CborHeadRefused { cause: c } => CborStepRefused { cause: c } + CborHeadIndefinite { major: _ } => CborStepRefused { cause: CborIndefiniteLengthUnsupported { at: at } } + CborHeadSimple { info: info, end: end } => cbor_simple_item(at: at, info: info, end: end) + CborHeadReady { head: head } => cbor_decode_body(input: input, at: at, head: head, depth: depth) + } + } +} + +fn cbor_string_span(input: List, head: CborHead) -> OctetSpanRead { + octet_span_read(input: input, at: head.end, length: head.argument) +} + +fn cbor_decode_body(input: List, at: Int, head: CborHead, depth: Int) -> CborStep { + if head.major == 0 { + CborStepped { item: CborUnsigned { value: head.argument }, end: head.end } + } else if head.major == 1 { + CborStepped { item: CborNegative { argument: head.argument }, end: head.end } + } else if head.major == 2 || head.major == 3 { + match cbor_string_span(input: input, head: head) { + OctetSpanRefused { cause: c } => CborStepRefused { cause: cbor_refusal_of_octet_read(cause: c) } + OctetSpanReady { span: span } => + if head.major == 2 { + CborStepped { item: CborBytes { span: span }, end: span.end } + } else { + CborStepped { item: CborText { span: span }, end: span.end } + } + } + } else if head.major == 4 { + cbor_decode_array(input: input, at: head.end, remaining: head.argument, depth: depth, acc: []) + } else if head.major == 5 { + cbor_decode_map(input: input, at: head.end, remaining: head.argument, depth: depth, acc: []) + } else { + match cbor_decode_item(input: input, at: head.end, depth: depth - 1) { + CborStepRefused { cause: c } => CborStepRefused { cause: c } + CborStepped { item: inner, end: end } => CborStepped { item: CborTagged { tag: head.argument, item: inner }, end: end } + } + } +} + +// A count larger than the octets left cannot be satisfied (each item takes at least one octet), so +// it refuses as truncation before any element is read. +fn cbor_count_fits(input: List, at: Int, remaining: Int) -> Bool { + remaining <= count(input) - at +} + +fn cbor_decode_array(input: List, at: Int, remaining: Int, depth: Int, acc: List) -> CborStep { + if remaining == 0 { + CborStepped { item: CborArray { items: acc }, end: at } + } else if !cbor_count_fits(input: input, at: at, remaining: remaining) { + CborStepRefused { cause: CborTruncated { at: at, needed: remaining, available: count(input) - at } } + } else { + match cbor_decode_item(input: input, at: at, depth: depth - 1) { + CborStepRefused { cause: c } => CborStepRefused { cause: c } + CborStepped { item: item, end: end } => + cbor_decode_array(input: input, at: end, remaining: remaining - 1, depth: depth, acc: acc |> list_push(item)) + } + } +} + +fn cbor_key_seen(input: List, entries: List, key: OctetSpan) -> Bool { + any(entries, e => octet_span_equals(input: input, a: e.key_encoding, b: key)) +} + +fn cbor_decode_map(input: List, at: Int, remaining: Int, depth: Int, acc: List) -> CborStep { + if remaining == 0 { + CborStepped { item: CborMap { entries: acc }, end: at } + } else if !cbor_count_fits(input: input, at: at, remaining: remaining * 2) { + CborStepRefused { cause: CborTruncated { at: at, needed: remaining * 2, available: count(input) - at } } + } else { + match cbor_decode_item(input: input, at: at, depth: depth - 1) { + CborStepRefused { cause: c } => CborStepRefused { cause: c } + CborStepped { item: key, end: key_end } => { + let key_span = OctetSpan { start: at, end: key_end } + if cbor_key_seen(input: input, entries: acc, key: key_span) { + CborStepRefused { cause: CborDuplicateMapKey { at: at } } + } else { + match cbor_decode_item(input: input, at: key_end, depth: depth - 1) { + CborStepRefused { cause: c } => CborStepRefused { cause: c } + CborStepped { item: value, end: value_end } => + cbor_decode_map( + input: input, at: value_end, remaining: remaining - 1, depth: depth, + acc: acc |> list_push(CborEntry { key: key, key_encoding: key_span, value: value }) + ) + } + } + } + } + } +} + +// One item starting at `at` that must end exactly at `end`: used for an embedded CBOR value whose +// extent the enclosing structure already fixed. +fn cbor_decode_exact(input: List, at: Int, end: Int) -> CborDecode { + match cbor_decode_item(input: input, at: at, depth: cbor_max_depth) { + CborStepRefused { cause: c } => CborRefused { cause: c } + CborStepped { item: item, end: e } => + if e == end { + CborDecoded { item: item } + } else if e < end { + CborRefused { cause: CborTrailingInput { at: e, remaining: end - e } } + } else { + CborRefused { cause: CborTruncated { at: end, needed: e - end, available: 0 } } + } + } +} + +// A whole input that is exactly one CBOR data item. +fn cbor_decode(input: List) -> CborDecode { + cbor_decode_exact(input: input, at: 0, end: count(input)) +} + +// ── Reading decoded maps ───────────────────────────────────────────────────────────────────── +// Protocol maps are keyed by text strings (App Attest) or small integers (COSE). A key is looked up +// by its WIRE octets, so a consumer states the exact encoding it expects and nothing is transcoded. + +fn cbor_text_key_is(input: List, key: CborItem, expected: List) -> Bool { + match key { + CborText { span: span } => octet_span_is(input: input, span: span, expected: expected) + _ => false + } +} + +fn cbor_map_text_value(input: List, entries: List, key: List) -> CborItem? { + fold(entries, init: none, f: (acc, e) => + if cbor_text_key_is(input: input, key: e.key, expected: key) { Present { value: e.value } } else { acc }) +} + +// A COSE integer label: non-negative n is CborUnsigned n; negative -1 - a is CborNegative a. +fn cbor_int_key_is(key: CborItem, label: Int) -> Bool { + match key { + CborUnsigned { value: v } => label >= 0 && v == label + CborNegative { argument: a } => label < 0 && (0 - 1 - a) == label + _ => false + } +} + +fn cbor_map_int_value(entries: List, label: Int) -> CborItem? { + fold(entries, init: none, f: (acc, e) => + if cbor_int_key_is(key: e.key, label: label) { Present { value: e.value } } else { acc }) +} + +fn cbor_int_value(item: CborItem) -> Int? { + match item { + CborUnsigned { value: v } => Present { value: v } + CborNegative { argument: a } => Present { value: 0 - 1 - a } + _ => none + } +} diff --git a/dag/extdeps/ietf/x509.dag b/dag/extdeps/ietf/x509.dag new file mode 100644 index 00000000000..4a4895f595c --- /dev/null +++ b/dag/extdeps/ietf/x509.dag @@ -0,0 +1,785 @@ +module extdeps.ietf.x509 + +import std.integer { UInt8 } +import std.octet_span { OctetSpan, octet_span_octets, octet_span_length, octet_span_equals, octet_at, octet_in_span, octet_bit_is_set } +import extdeps.itu.der { + DerElement, DerRefusal, DerRead, DerReadReady, DerReadRefused, DerChildren, DerChildrenReady, DerChildrenRefused, + DerContextSpecific, DerUniversal, DerUnexpectedElement, + DerSmallInteger, DerSmallIntegerReady, DerSmallIntegerRefused, + DerBoolean, DerBooleanReady, DerBooleanRefused, + DerBitString, DerBitStringRead, DerBitStringReady, DerBitStringRefused, + DerObjectIdentifier, DerObjectIdentifierReady, DerObjectIdentifierRefused, + der_read_exact, der_children, der_expect, der_expect_universal, der_is, der_integer_content, + der_small_unsigned, der_boolean, der_bit_string, der_octet_string, der_object_identifier, + der_tag_sequence, der_tag_utc_time, der_tag_generalized_time, der_tag_boolean, +} +import extdeps.time.posix_epoch { CivilDateTime, civil_epoch_seconds } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// X.509 v3 CERTIFICATES, RFC 5280, read from DER (extdeps.itu.der). The named consumer is +// extdeps.apple.app_attest, whose attestation carries a two-certificate chain (credential leaf and +// Apple App Attestation CA 1) under a pinned root. Exactly the fields that consumer needs are +// modeled: the signed TBS bytes, signature algorithm and value, issuer and subject as raw Name +// encodings (compared octet for octet, RFC 5280 7.1's binary-comparison rule for the names this +// chain carries), validity, the subject public key, and extensions. +// +// Path validation here is RFC 5280 6.1's STRUCTURAL part, which needs no cryptography: name +// chaining, validity at a caller-supplied time, basicConstraints cA and pathLenConstraint on every +// issuing certificate, keyUsage keyCertSign when keyUsage is present, the signature algorithm being +// one this verifier admits and agreeing between the TBS and the outer certificate, and refusal of +// any CRITICAL extension this reader does not process (4.2). The signature over each TBS is NOT +// checked here: that is ECDSA verification, and its realization is the typed unbound frontier +// gunbc.auth.approval_device_redemption ecdsa_verification_realization_frontier. A structurally +// valid chain therefore comes back as X509ChainStructurallyValid -- a name that claims no signature. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.rfc-editor.org/rfc/rfc5280" + } +} + +// Object identifiers read by this module, as arcs. +data oid_ecdsa_with_sha256: List = [1, 2, 840, 10045, 4, 3, 2] +data oid_ecdsa_with_sha384: List = [1, 2, 840, 10045, 4, 3, 3] +data oid_ec_public_key: List = [1, 2, 840, 10045, 2, 1] +data oid_prime256v1: List = [1, 2, 840, 10045, 3, 1, 7] +data oid_secp384r1: List = [1, 3, 132, 0, 34] +data oid_basic_constraints: List = [2, 5, 29, 19] +data oid_key_usage: List = [2, 5, 29, 15] + +type X509Extension { + oid: List + critical: Bool + value: OctetSpan +} + +type X509PublicKey { + algorithm: List + curve: List + point: OctetSpan +} + +type X509Certificate { + whole: OctetSpan + tbs: OctetSpan + version: Int + signature_algorithm: List + issuer: OctetSpan + subject: OctetSpan + not_before: Int + not_after: Int + public_key: X509PublicKey + extensions: List + signature: OctetSpan +} + +type X509Refusal + = X509Malformed { cause: DerRefusal } + | X509VersionUnsupported { version: Int } + | X509SignatureAlgorithmMismatch + | X509SignatureAlgorithmUnsupported { oid: List } + | X509TimeMalformed { at: Int } + | X509PublicKeyUnsupported { algorithm: List } + | X509DuplicateExtension { oid: List } + | X509UnhandledCriticalExtension { oid: List } + | X509IssuerNameMismatch { depth: Int } + | X509NotYetValid { depth: Int, not_before: Int } + | X509Expired { depth: Int, not_after: Int } + | X509IssuerNotCa { depth: Int } + | X509IssuerLacksKeyCertSign { depth: Int } + | X509PathLengthExceeded { depth: Int, limit: Int } + +type X509Read + = X509Ready { certificate: X509Certificate } + | X509Refused { cause: X509Refusal } + +// ── Small readers ──────────────────────────────────────────────────────────────────────────── + +type X509Children + = X509ChildrenReady { children: List } + | X509ChildrenRefused { cause: X509Refusal } + +fn x509_sequence_children(input: List, element: DerElement) -> X509Children { + match der_expect_universal(element: element, tag: der_tag_sequence) { + DerReadRefused { cause: c } => X509ChildrenRefused { cause: X509Malformed { cause: c } } + DerReadReady { element: e } => + match der_children(input: input, parent: e) { + DerChildrenRefused { cause: c } => X509ChildrenRefused { cause: X509Malformed { cause: c } } + DerChildrenReady { children: cs } => X509ChildrenReady { children: cs } + } + } +} + +fn x509_unexpected(element: DerElement, tag: Int) -> X509Refusal { + X509Malformed { cause: DerUnexpectedElement { at: element.whole.start, expected_tag: tag } } +} + +type X509Oid + = X509OidReady { arcs: List } + | X509OidRefused { cause: X509Refusal } + +// AlgorithmIdentifier ::= SEQUENCE { algorithm OID, parameters ANY OPTIONAL }; returns the algorithm +// and, when the parameters are themselves an OID (a named curve), that OID; otherwise []. +type X509Algorithm { + algorithm: List + parameter: List +} + +type X509AlgorithmRead + = X509AlgorithmReady { value: X509Algorithm } + | X509AlgorithmRefused { cause: X509Refusal } + +fn x509_algorithm(input: List, element: DerElement) -> X509AlgorithmRead { + match x509_sequence_children(input: input, element: element) { + X509ChildrenRefused { cause: c } => X509AlgorithmRefused { cause: c } + X509ChildrenReady { children: cs } => + match cs.first() { + Absent => X509AlgorithmRefused { cause: x509_unexpected(element: element, tag: 6) } + Present { value: oid_el } => + match der_object_identifier(input: input, element: oid_el) { + DerObjectIdentifierRefused { cause: c } => X509AlgorithmRefused { cause: X509Malformed { cause: c } } + DerObjectIdentifierReady { arcs: arcs } => + match cs |> get(1) { + Absent => X509AlgorithmReady { value: X509Algorithm { algorithm: arcs, parameter: [] } } + Present { value: p } => + match der_object_identifier(input: input, element: p) { + DerObjectIdentifierReady { arcs: param } => X509AlgorithmReady { value: X509Algorithm { algorithm: arcs, parameter: param } } + DerObjectIdentifierRefused { cause: _ } => X509AlgorithmReady { value: X509Algorithm { algorithm: arcs, parameter: [] } } + } + } + } + } + } +} + +// ── Time (RFC 5280 4.1.2.5) ────────────────────────────────────────────────────────────────── +// UTCTime is YYMMDDHHMMSSZ, with YY >= 50 meaning 19YY and YY < 50 meaning 20YY; GeneralizedTime +// is YYYYMMDDHHMMSSZ. Both must end in Z and carry seconds; anything else is refused. + +fn x509_digit(input: List, at: Int) -> Int? { + match octet_at(input: input, at: at) { + Absent => none + Present { value: o } => if o >= 48 && o <= 57 { Present { value: o - 48 } } else { none } + } +} + +fn x509_digits(input: List, at: Int, n: Int, acc: Int) -> Int? { + if n == 0 { + Present { value: acc } + } else { + match x509_digit(input: input, at: at) { + Absent => none + Present { value: d } => x509_digits(input: input, at: at + 1, n: n - 1, acc: acc * 10 + d) + } + } +} + +fn x509_civil_from(input: List, at: Int, year: Int) -> CivilDateTime? { + match x509_digits(input: input, at: at, n: 2, acc: 0) { + Absent => none + Present { value: month } => + match x509_digits(input: input, at: at + 2, n: 2, acc: 0) { + Absent => none + Present { value: day } => + match x509_digits(input: input, at: at + 4, n: 2, acc: 0) { + Absent => none + Present { value: hour } => + match x509_digits(input: input, at: at + 6, n: 2, acc: 0) { + Absent => none + Present { value: minute } => + match x509_digits(input: input, at: at + 8, n: 2, acc: 0) { + Absent => none + Present { value: second } => + Present { value: CivilDateTime { year: year, month: month, day: day, hour: hour, minute: minute, second: second } } + } + } + } + } + } +} + +fn x509_ends_in_z(input: List, element: DerElement) -> Bool { + match octet_in_span(input: input, span: element.content, at: element.content.end - 1) { + Present { value: z } => z == 90 + Absent => false + } +} + +fn x509_time(input: List, element: DerElement) -> Int? { + let start = element.content.start + let length = octet_span_length(span: element.content) + let civil = if der_is(element: element, class: DerUniversal, tag: der_tag_utc_time) && length == 13 && x509_ends_in_z(input: input, element: element) { + match x509_digits(input: input, at: start, n: 2, acc: 0) { + Absent => none + Present { value: yy } => x509_civil_from(input: input, at: start + 2, year: if yy >= 50 { 1900 + yy } else { 2000 + yy }) + } + } else if der_is(element: element, class: DerUniversal, tag: der_tag_generalized_time) && length == 15 && x509_ends_in_z(input: input, element: element) { + match x509_digits(input: input, at: start, n: 4, acc: 0) { + Absent => none + Present { value: yyyy } => x509_civil_from(input: input, at: start + 4, year: yyyy) + } + } else { + none + } + match civil { + Absent => none + Present { value: t } => civil_epoch_seconds(t: t) + } +} + +// ── Extensions (RFC 5280 4.1, 4.2) ─────────────────────────────────────────────────────────── + +type X509ExtensionRead + = X509ExtensionReady { value: X509Extension } + | X509ExtensionRefused { cause: X509Refusal } + +// Extension ::= SEQUENCE { extnID OID, critical BOOLEAN DEFAULT FALSE, extnValue OCTET STRING }. +// DER forbids encoding a DEFAULT value, so an explicit critical FALSE is refused as noncanonical. +fn x509_extension(input: List, element: DerElement) -> X509ExtensionRead { + match x509_sequence_children(input: input, element: element) { + X509ChildrenRefused { cause: c } => X509ExtensionRefused { cause: c } + X509ChildrenReady { children: cs } => + match cs.first() { + Absent => X509ExtensionRefused { cause: x509_unexpected(element: element, tag: 6) } + Present { value: oid_el } => + match der_object_identifier(input: input, element: oid_el) { + DerObjectIdentifierRefused { cause: c } => X509ExtensionRefused { cause: X509Malformed { cause: c } } + DerObjectIdentifierReady { arcs: arcs } => + if count(cs) == 2 { + x509_extension_value(input: input, oid: arcs, critical: false, value_el: cs |> get(1)) + } else if count(cs) == 3 { + match cs |> get(1) { + Absent => X509ExtensionRefused { cause: x509_unexpected(element: element, tag: der_tag_boolean) } + Present { value: crit_el } => + match der_boolean(input: input, element: crit_el) { + DerBooleanRefused { cause: c } => X509ExtensionRefused { cause: X509Malformed { cause: c } } + DerBooleanReady { value: critical } => + if critical { + x509_extension_value(input: input, oid: arcs, critical: true, value_el: cs |> get(2)) + } else { + X509ExtensionRefused { cause: X509Malformed { cause: DerUnexpectedElement { at: crit_el.whole.start, expected_tag: 4 } } } + } + } + } + } else { + X509ExtensionRefused { cause: x509_unexpected(element: element, tag: 4) } + } + } + } + } +} + +fn x509_extension_value(input: List, oid: List, critical: Bool, value_el: DerElement?) -> X509ExtensionRead { + match value_el { + Absent => X509ExtensionRefused { cause: X509Malformed { cause: DerUnexpectedElement { at: 0, expected_tag: 4 } } } + Present { value: v } => + match der_octet_string(element: v) { + DerReadRefused { cause: c } => X509ExtensionRefused { cause: X509Malformed { cause: c } } + DerReadReady { element: os } => X509ExtensionReady { value: X509Extension { oid: oid, critical: critical, value: os.content } } + } + } +} + +type X509Extensions + = X509ExtensionsReady { extensions: List } + | X509ExtensionsRefused { cause: X509Refusal } + +fn x509_extensions_from(input: List, items: List, acc: List) -> X509Extensions { + match items.first() { + Absent => X509ExtensionsReady { extensions: acc } + Present { value: el } => + match x509_extension(input: input, element: el) { + X509ExtensionRefused { cause: c } => X509ExtensionsRefused { cause: c } + X509ExtensionReady { value: ext } => + if any(acc, e => e.oid == ext.oid) { + X509ExtensionsRefused { cause: X509DuplicateExtension { oid: ext.oid } } + } else { + x509_extensions_from(input: input, items: items.skip(n: 1), acc: acc |> list_push(ext)) + } + } + } +} + +// extensions [3] EXPLICIT SEQUENCE SIZE (1..MAX) OF Extension +fn x509_extensions(input: List, tagged: DerElement) -> X509Extensions { + match der_children(input: input, parent: tagged) { + DerChildrenRefused { cause: c } => X509ExtensionsRefused { cause: X509Malformed { cause: c } } + DerChildrenReady { children: inner } => + match inner.first() { + Absent => X509ExtensionsRefused { cause: x509_unexpected(element: tagged, tag: der_tag_sequence) } + Present { value: seq } => + if count(inner) != 1 { + X509ExtensionsRefused { cause: x509_unexpected(element: tagged, tag: der_tag_sequence) } + } else { + match x509_sequence_children(input: input, element: seq) { + X509ChildrenRefused { cause: c } => X509ExtensionsRefused { cause: c } + X509ChildrenReady { children: items } => x509_extensions_from(input: input, items: items, acc: []) + } + } + } + } +} + +fn x509_extension_named(cert: X509Certificate, oid: List) -> X509Extension? { + fold(cert.extensions, init: none, f: (acc, e) => if e.oid == oid { Present { value: e } } else { acc }) +} + +// ── The certificate ────────────────────────────────────────────────────────────────────────── + +fn x509_admitted_signature_algorithm(oid: List) -> Bool { + oid == oid_ecdsa_with_sha256 || oid == oid_ecdsa_with_sha384 +} + +type X509PublicKeyRead + = X509PublicKeyReady { value: X509PublicKey } + | X509PublicKeyRefused { cause: X509Refusal } + +// SubjectPublicKeyInfo ::= SEQUENCE { algorithm AlgorithmIdentifier, subjectPublicKey BIT STRING }. +// Only id-ecPublicKey on a named curve is admitted, with the point as whole octets (unused bits 0). +fn x509_subject_public_key(input: List, element: DerElement) -> X509PublicKeyRead { + match x509_sequence_children(input: input, element: element) { + X509ChildrenRefused { cause: c } => X509PublicKeyRefused { cause: c } + X509ChildrenReady { children: cs } => + if count(cs) != 2 { + X509PublicKeyRefused { cause: x509_unexpected(element: element, tag: der_tag_sequence) } + } else { + match cs.first() { + Absent => X509PublicKeyRefused { cause: x509_unexpected(element: element, tag: der_tag_sequence) } + Present { value: alg_el } => + match x509_algorithm(input: input, element: alg_el) { + X509AlgorithmRefused { cause: c } => X509PublicKeyRefused { cause: c } + X509AlgorithmReady { value: alg } => + if alg.algorithm != oid_ec_public_key || (alg.parameter != oid_prime256v1 && alg.parameter != oid_secp384r1) { + X509PublicKeyRefused { cause: X509PublicKeyUnsupported { algorithm: alg.algorithm } } + } else { + match cs |> get(1) { + Absent => X509PublicKeyRefused { cause: x509_unexpected(element: element, tag: 3) } + Present { value: key_el } => + match der_bit_string(input: input, element: key_el) { + DerBitStringRefused { cause: c } => X509PublicKeyRefused { cause: X509Malformed { cause: c } } + DerBitStringReady { value: bits } => + if bits.unused_bits != 0 { + X509PublicKeyRefused { cause: X509PublicKeyUnsupported { algorithm: alg.algorithm } } + } else { + X509PublicKeyReady { value: X509PublicKey { algorithm: alg.algorithm, curve: alg.parameter, point: bits.bits } } + } + } + } + } + } + } + } + } +} + +type X509Tbs { + version: Int + signature_algorithm: List + issuer: OctetSpan + subject: OctetSpan + not_before: Int + not_after: Int + public_key: X509PublicKey + extensions: List +} + +type X509TbsRead + = X509TbsReady { value: X509Tbs } + | X509TbsRefused { cause: X509Refusal } + +// TBSCertificate: version [0] must be v3 (value 2) -- App Attest's chain is v3 and extensions exist +// only in v3 -- so an absent version (v1) is refused rather than defaulted. issuerUniqueID and +// subjectUniqueID ([1], [2]) have no consumer and refuse through the element count. +fn x509_tbs(input: List, element: DerElement) -> X509TbsRead { + match x509_sequence_children(input: input, element: element) { + X509ChildrenRefused { cause: c } => X509TbsRefused { cause: c } + X509ChildrenReady { children: cs } => + match x509_tbs_parts(cs: cs) { + Absent => X509TbsRefused { cause: x509_unexpected(element: element, tag: der_tag_sequence) } + Present { value: parts } => x509_tbs_fields(input: input, parts: parts) + } + } +} + +fn x509_version(input: List, tagged: DerElement) -> Int? { + if !der_is(element: tagged, class: DerContextSpecific, tag: 0) { + none + } else { + match der_children(input: input, parent: tagged) { + DerChildrenRefused { cause: _ } => none + DerChildrenReady { children: inner } => + if count(inner) != 1 { + none + } else { + match inner.first() { + Absent => none + Present { value: v } => + match der_small_unsigned(input: input, element: v) { + DerSmallIntegerRefused { cause: _ } => none + DerSmallIntegerReady { value: n } => Present { value: n } + } + } + } + } + } +} + +// The TBSCertificate's eight elements by name. Built only when all eight are present, so no reader +// below indexes a list it has not proved long enough. +type X509TbsParts { + version: DerElement + serial: DerElement + signature: DerElement + issuer: DerElement + validity: DerElement + subject: DerElement + public_key: DerElement + extensions: DerElement +} + +fn x509_tbs_parts(cs: List) -> X509TbsParts? { + match cs |> get(0) { Absent => none Present { value: a } => + match cs |> get(1) { Absent => none Present { value: b } => + match cs |> get(2) { Absent => none Present { value: c } => + match cs |> get(3) { Absent => none Present { value: d } => + match cs |> get(4) { Absent => none Present { value: e } => + match cs |> get(5) { Absent => none Present { value: f } => + match cs |> get(6) { Absent => none Present { value: g } => + match cs |> get(7) { Absent => none Present { value: h } => + if count(cs) == 8 { + Present { value: X509TbsParts { version: a, serial: b, signature: c, issuer: d, validity: e, subject: f, public_key: g, extensions: h } } + } else { + none + } + } } } } } } } } +} + +type X509Pair { + first: DerElement + second: DerElement +} + +fn x509_pair(cs: List) -> X509Pair? { + match cs |> get(0) { Absent => none Present { value: a } => + match cs |> get(1) { Absent => none Present { value: b } => + if count(cs) == 2 { Present { value: X509Pair { first: a, second: b } } } else { none } + } } +} + +type X509Triple { + first: DerElement + second: DerElement + third: DerElement +} + +fn x509_triple(cs: List) -> X509Triple? { + match cs |> get(0) { Absent => none Present { value: a } => + match cs |> get(1) { Absent => none Present { value: b } => + match cs |> get(2) { Absent => none Present { value: c } => + if count(cs) == 3 { Present { value: X509Triple { first: a, second: b, third: c } } } else { none } + } } } +} + +fn x509_tbs_fields(input: List, parts: X509TbsParts) -> X509TbsRead { + let serial_el = parts.serial + let sig_el = parts.signature + let issuer_el = parts.issuer + let validity_el = parts.validity + let subject_el = parts.subject + let spki_el = parts.public_key + let ext_el = parts.extensions + match x509_version(input: input, tagged: parts.version) { + Absent => X509TbsRefused { cause: X509VersionUnsupported { version: 0 } } + Present { value: version } => + if version != 2 { + X509TbsRefused { cause: X509VersionUnsupported { version: version } } + } else { + match der_integer_content(input: input, element: serial_el) { + DerReadRefused { cause: c } => X509TbsRefused { cause: X509Malformed { cause: c } } + DerReadReady { element: _ } => + match x509_algorithm(input: input, element: sig_el) { + X509AlgorithmRefused { cause: c } => X509TbsRefused { cause: c } + X509AlgorithmReady { value: sig_alg } => + match der_expect_universal(element: issuer_el, tag: der_tag_sequence) { + DerReadRefused { cause: c } => X509TbsRefused { cause: X509Malformed { cause: c } } + DerReadReady { element: issuer } => + match der_expect_universal(element: subject_el, tag: der_tag_sequence) { + DerReadRefused { cause: c } => X509TbsRefused { cause: X509Malformed { cause: c } } + DerReadReady { element: subject } => + x509_tbs_validity( + input: input, validity_el: validity_el, spki_el: spki_el, ext_el: ext_el, + version: version, sig_alg: sig_alg.algorithm, issuer: issuer.whole, subject: subject.whole, + ) + } + } + } + } + } + } +} + +fn x509_tbs_validity( + input: List, validity_el: DerElement, spki_el: DerElement, ext_el: DerElement, + version: Int, sig_alg: List, issuer: OctetSpan, subject: OctetSpan, +) -> X509TbsRead { + match x509_sequence_children(input: input, element: validity_el) { + X509ChildrenRefused { cause: c } => X509TbsRefused { cause: c } + X509ChildrenReady { children: times } => + match x509_pair(cs: times) { + Absent => X509TbsRefused { cause: X509TimeMalformed { at: validity_el.whole.start } } + Present { value: pair } => + match x509_time(input: input, element: pair.first) { + Absent => X509TbsRefused { cause: X509TimeMalformed { at: validity_el.whole.start } } + Present { value: not_before } => + match x509_time(input: input, element: pair.second) { + Absent => X509TbsRefused { cause: X509TimeMalformed { at: validity_el.whole.start } } + Present { value: not_after } => + match x509_subject_public_key(input: input, element: spki_el) { + X509PublicKeyRefused { cause: c } => X509TbsRefused { cause: c } + X509PublicKeyReady { value: key } => + if !der_is(element: ext_el, class: DerContextSpecific, tag: 3) { + X509TbsRefused { cause: x509_unexpected(element: ext_el, tag: 3) } + } else { + match x509_extensions(input: input, tagged: ext_el) { + X509ExtensionsRefused { cause: c } => X509TbsRefused { cause: c } + X509ExtensionsReady { extensions: exts } => + X509TbsReady { + value: X509Tbs { + version: version, signature_algorithm: sig_alg, issuer: issuer, subject: subject, + not_before: not_before, not_after: not_after, public_key: key, extensions: exts, + } + } + } + } + } + } + } + } + } +} + +// Certificate ::= SEQUENCE { tbsCertificate, signatureAlgorithm, signatureValue BIT STRING }, which +// must occupy `span` exactly (swift-ibex-621's finding (f): each certificate consumes its bytes). +fn x509_certificate(input: List, span: OctetSpan) -> X509Read { + match der_read_exact(input: input, span: span) { + DerReadRefused { cause: c } => X509Refused { cause: X509Malformed { cause: c } } + DerReadReady { element: cert_el } => + match x509_sequence_children(input: input, element: cert_el) { + X509ChildrenRefused { cause: c } => X509Refused { cause: c } + X509ChildrenReady { children: cs } => + match x509_triple(cs: cs) { + Absent => X509Refused { cause: x509_unexpected(element: cert_el, tag: der_tag_sequence) } + Present { value: parts } => { + let tbs_el = parts.first + match x509_tbs(input: input, element: tbs_el) { + X509TbsRefused { cause: c } => X509Refused { cause: c } + X509TbsReady { value: tbs } => + match x509_algorithm(input: input, element: parts.second) { + X509AlgorithmRefused { cause: c } => X509Refused { cause: c } + X509AlgorithmReady { value: outer } => + if outer.algorithm != tbs.signature_algorithm { + X509Refused { cause: X509SignatureAlgorithmMismatch } + } else if !x509_admitted_signature_algorithm(oid: outer.algorithm) { + X509Refused { cause: X509SignatureAlgorithmUnsupported { oid: outer.algorithm } } + } else { + match der_bit_string(input: input, element: parts.third) { + DerBitStringRefused { cause: c } => X509Refused { cause: X509Malformed { cause: c } } + DerBitStringReady { value: sig } => + X509Ready { + certificate: X509Certificate { + whole: cert_el.whole, tbs: tbs_el.whole, version: tbs.version, + signature_algorithm: outer.algorithm, issuer: tbs.issuer, subject: tbs.subject, + not_before: tbs.not_before, not_after: tbs.not_after, public_key: tbs.public_key, + extensions: tbs.extensions, signature: sig.bits, + } + } + } + } + } + } + } + } + } + } +} + +// ── Structural path validation (RFC 5280 6.1, without signatures) ──────────────────────────── + +type X509BasicConstraints { + ca: Bool + path_length: Int? +} + +// BasicConstraints ::= SEQUENCE { cA BOOLEAN DEFAULT FALSE, pathLenConstraint INTEGER OPTIONAL } +fn x509_basic_constraints(input: List, ext: X509Extension) -> X509BasicConstraints? { + match der_read_exact(input: input, span: ext.value) { + DerReadRefused { cause: _ } => none + DerReadReady { element: seq } => + match x509_sequence_children(input: input, element: seq) { + X509ChildrenRefused { cause: _ } => none + X509ChildrenReady { children: cs } => + if count(cs) == 0 { + Present { value: X509BasicConstraints { ca: false, path_length: none } } + } else { + match der_boolean(input: input, element: match cs.first() { Present { value: f } => f Absent => seq }) { + DerBooleanRefused { cause: _ } => none + DerBooleanReady { value: ca } => + if count(cs) == 1 { + Present { value: X509BasicConstraints { ca: ca, path_length: none } } + } else if count(cs) == 2 { + match der_small_unsigned(input: input, element: match cs |> get(1) { Present { value: f } => f Absent => seq }) { + DerSmallIntegerRefused { cause: _ } => none + DerSmallIntegerReady { value: n } => Present { value: X509BasicConstraints { ca: ca, path_length: Present { value: n } } } + } + } else { + none + } + } + } + } + } +} + +// KeyUsage ::= BIT STRING; keyCertSign is bit 5, i.e. the octet's bit 2 counting from the low end. +fn x509_key_usage_permits_cert_sign(input: List, ext: X509Extension) -> Bool { + match der_read_exact(input: input, span: ext.value) { + DerReadRefused { cause: _ } => false + DerReadReady { element: e } => + match der_bit_string(input: input, element: e) { + DerBitStringRefused { cause: _ } => false + DerBitStringReady { value: bits } => + match octet_in_span(input: input, span: bits.bits, at: bits.bits.start) { + Absent => false + Present { value: first } => octet_bit_is_set(octet: first, bit: 2) + } + } + } +} + +fn x509_unhandled_critical(cert: X509Certificate, handled: List>) -> List? { + fold(cert.extensions, init: none, f: (acc, e) => + match acc { + Present { value: _ } => acc + Absent => if e.critical && !any(handled, h => h == e.oid) { Present { value: e.oid } } else { none } + }) +} + +type X509ChainCheck + = X509ChainStructurallyValid + | X509ChainRefused { cause: X509Refusal } + +fn x509_check_validity(cert: X509Certificate, depth: Int, now: Int) -> X509Refusal? { + if now < cert.not_before { + Present { value: X509NotYetValid { depth: depth, not_before: cert.not_before } } + } else if now > cert.not_after { + Present { value: X509Expired { depth: depth, not_after: cert.not_after } } + } else { + none + } +} + +// Issuing-certificate checks for the certificate at `depth` that signs `below` further non-anchor +// certificates: basicConstraints with cA TRUE, keyUsage keyCertSign when keyUsage is present, and +// pathLenConstraint >= the number of intermediates beneath it. +fn x509_check_issuer(input: List, cert: X509Certificate, depth: Int, intermediates_below: Int) -> X509Refusal? { + match x509_extension_named(cert: cert, oid: oid_basic_constraints) { + Absent => Present { value: X509IssuerNotCa { depth: depth } } + Present { value: bc_ext } => + match x509_basic_constraints(input: input, ext: bc_ext) { + Absent => Present { value: X509IssuerNotCa { depth: depth } } + Present { value: bc } => + if !bc.ca { + Present { value: X509IssuerNotCa { depth: depth } } + } else { + let usage_ok = match x509_extension_named(cert: cert, oid: oid_key_usage) { + Absent => true + Present { value: ku } => x509_key_usage_permits_cert_sign(input: input, ext: ku) + } + if !usage_ok { + Present { value: X509IssuerLacksKeyCertSign { depth: depth } } + } else { + match bc.path_length { + Present { value: limit } => + if intermediates_below > limit { + Present { value: X509PathLengthExceeded { depth: depth, limit: limit } } + } else { + none + } + Absent => none + } + } + } + } + } +} + +// One certificate's own checks: validity at `now`, and no critical extension outside `handled`. +fn x509_check_certificate(cert: X509Certificate, depth: Int, now: Int, handled: List>) -> X509Refusal? { + match x509_check_validity(cert: cert, depth: depth, now: now) { + Present { value: r } => Present { value: r } + Absent => + match x509_unhandled_critical(cert: cert, handled: handled) { + Present { value: oid } => Present { value: X509UnhandledCriticalExtension { oid: oid } } + Absent => none + } + } +} + +// A chain [leaf, ..., last] where each certificate is issued by the next and `last` is issued by +// `anchor`. Each certificate is read from its own input (x5c entries are separate byte strings; the +// anchor is a pinned constant), so the chain carries (input, certificate) pairs. `leaf_handled` +// names the critical extensions the leaf's consumer processes, beyond basicConstraints and keyUsage. +type X509Link { + input: List + certificate: X509Certificate +} + +fn x509_names_chain(child: X509Link, issuer: X509Link) -> Bool { + octet_span_octets(input: child.input, span: child.certificate.issuer) + == octet_span_octets(input: issuer.input, span: issuer.certificate.subject) +} + +// The certificate that issued the one at `depth`: the next in the chain, or the anchor after the last. +fn x509_issuer_link(chain: List, anchor: X509Link, depth: Int) -> X509Link { + match chain |> get(depth + 1) { + Present { value: next } => next + Absent => anchor + } +} + +fn x509_chain_step(chain: List, anchor: X509Link, depth: Int, now: Int, leaf_handled: List>) -> X509ChainCheck { + match chain |> get(depth) { + Absent => X509ChainStructurallyValid + Present { value: link } => { + let issuer = x509_issuer_link(chain: chain, anchor: anchor, depth: depth) + let handled = if depth == 0 { append([oid_basic_constraints, oid_key_usage], items: leaf_handled) } else { [oid_basic_constraints, oid_key_usage] } + let below = if depth == 0 { 0 } else { depth - 1 } + if !x509_names_chain(child: link, issuer: issuer) { + X509ChainRefused { cause: X509IssuerNameMismatch { depth: depth } } + } else { + match x509_check_certificate(cert: link.certificate, depth: depth, now: now, handled: handled) { + Present { value: r } => X509ChainRefused { cause: r } + Absent => + if depth > 0 { + match x509_check_issuer(input: link.input, cert: link.certificate, depth: depth, intermediates_below: below) { + Present { value: r } => X509ChainRefused { cause: r } + Absent => x509_chain_step(chain: chain, anchor: anchor, depth: depth + 1, now: now, leaf_handled: leaf_handled) + } + } else { + x509_chain_step(chain: chain, anchor: anchor, depth: depth + 1, now: now, leaf_handled: leaf_handled) + } + } + } + } + } +} + +// The anchor itself is trusted by pinning (RFC 5280 6.1.1(d)): its own validity and constraints are +// not path inputs. It must still be an issuing certificate for the chain's last element. +fn x509_chain_structure(chain: List, anchor: X509Link, now: Int, leaf_handled: List>) -> X509ChainCheck { + match x509_check_issuer(input: anchor.input, cert: anchor.certificate, depth: count(chain), intermediates_below: count(chain) - 1) { + Present { value: r } => X509ChainRefused { cause: r } + Absent => x509_chain_step(chain: chain, anchor: anchor, depth: 0, now: now, leaf_handled: leaf_handled) + } +} diff --git a/dag/extdeps/itu/der.dag b/dag/extdeps/itu/der.dag new file mode 100644 index 00000000000..d9ee73d8bca --- /dev/null +++ b/dag/extdeps/itu/der.dag @@ -0,0 +1,391 @@ +module extdeps.itu.der + +import std.integer { UInt8 } +import std.octet_span { + OctetSpan, OctetReadRefusal, OctetInputTruncated, OctetUnsignedTooWide, OctetWordRefused, + OctetUnsignedReady, OctetUnsignedRefused, OctetSpanReady, OctetSpanRefused, + octet_at, octet_in_span, octet_bit_field, octet_bit_is_set, octet_read_unsigned_be, octet_span_read, octet_span_length, +} +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// DER, ITU-T X.690 (08/2015) section 10, the distinguished subset of BER, as a reader over one octet +// input. Its named consumer is extdeps.ietf.x509 (App Attest's certificate chain), and only the +// encodings that consumer reads are modeled: TLV framing with definite lengths, SEQUENCE, INTEGER, +// BIT STRING, OCTET STRING, OBJECT IDENTIFIER, BOOLEAN, and context-specific tags. +// +// DER admits exactly one encoding per value, so each BER latitude is its own refusal: +// * the indefinite length form (0x80) -> DerIndefiniteLength (X.690 10.1) +// * a long-form length that fits a shorter form -> DerNoncanonicalLength (X.690 10.1, 8.1.3.5) +// * an INTEGER with a redundant leading octet -> DerNoncanonicalInteger (X.690 8.3.2) +// * a BOOLEAN other than 0x00/0xFF -> DerNoncanonicalBoolean (X.690 11.1) +// * a BIT STRING whose unused-bit count is > 7, +// or nonzero on an empty string -> DerBitStringMalformed (X.690 8.6.2) +// A tag number >= 31 (the high-tag-number form) has no consumed field and refuses as unsupported. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "www.itu.int/rec/T-REC-X.690-202102-I/en" + } +} + +type DerTagClass + = DerUniversal + | DerApplication + | DerContextSpecific + | DerPrivate + +type DerElement { + class: DerTagClass + constructed: Bool + tag: Int + whole: OctetSpan + content: OctetSpan +} + +type DerRefusal + = DerTruncated { at: Int, needed: Int, available: Int } + | DerHighTagNumberUnsupported { at: Int } + | DerIndefiniteLength { at: Int } + | DerNoncanonicalLength { at: Int } + | DerLengthTooWide { at: Int } + | DerTrailingInput { at: Int, remaining: Int } + | DerUnexpectedElement { at: Int, expected_tag: Int } + | DerNoncanonicalInteger { at: Int } + | DerNoncanonicalBoolean { at: Int } + | DerBitStringMalformed { at: Int } + | DerObjectIdentifierMalformed { at: Int } + +type DerRead + = DerReadReady { element: DerElement } + | DerReadRefused { cause: DerRefusal } + +type DerChildren + = DerChildrenReady { children: List } + | DerChildrenRefused { cause: DerRefusal } + +// Universal tag numbers read by the consumer (X.680 8.4). +data der_tag_boolean: Int = 1 +data der_tag_integer: Int = 2 +data der_tag_bit_string: Int = 3 +data der_tag_octet_string: Int = 4 +data der_tag_object_identifier: Int = 6 +data der_tag_utf8_string: Int = 12 +data der_tag_sequence: Int = 16 +data der_tag_set: Int = 17 +data der_tag_printable_string: Int = 19 +data der_tag_utc_time: Int = 23 +data der_tag_generalized_time: Int = 24 + +fn der_refusal_of_octet_read(cause: OctetReadRefusal) -> DerRefusal { + match cause { + OctetInputTruncated { at: a, needed: n, available: v } => DerTruncated { at: a, needed: n, available: v } + OctetUnsignedTooWide { at: a, octets: _ } => DerLengthTooWide { at: a } + OctetWordRefused { at: a } => DerLengthTooWide { at: a } + } +} + +fn der_tag_class(bits: Int) -> DerTagClass { + if bits == 0 { DerUniversal } else if bits == 1 { DerApplication } else if bits == 2 { DerContextSpecific } else { DerPrivate } +} + +type DerLength { + length: Int + content_start: Int +} + +type DerLengthRead + = DerLengthReady { length: DerLength } + | DerLengthRefused { cause: DerRefusal } + +// X.690 8.1.3: short form below 128; long form 0x81..0x84 followed by that many length octets, which +// DER requires to be the minimum (no leading zero octet, and never a value short form could carry). +fn der_read_length(input: List, at: Int) -> DerLengthRead { + match octet_at(input: input, at: at) { + Absent => DerLengthRefused { cause: DerTruncated { at: at, needed: 1, available: 0 } } + Present { value: first } => + if first < 128 { + DerLengthReady { length: DerLength { length: first + 0, content_start: at + 1 } } + } else if first == 128 { + DerLengthRefused { cause: DerIndefiniteLength { at: at } } + } else { + let octets = first - 128 + match octet_read_unsigned_be(input: input, at: at + 1, octets: octets) { + OctetUnsignedRefused { cause: c } => DerLengthRefused { cause: der_refusal_of_octet_read(cause: c) } + OctetUnsignedReady { value: v, end: e } => + match octet_at(input: input, at: at + 1) { + Absent => DerLengthRefused { cause: DerTruncated { at: at + 1, needed: 1, available: 0 } } + Present { value: lead } => + if v < 128 || lead == 0 { + DerLengthRefused { cause: DerNoncanonicalLength { at: at } } + } else { + DerLengthReady { length: DerLength { length: v, content_start: e } } + } + } + } + } + } +} + +// One TLV element starting at `at`. Its extent is fixed by its own length octets; whether it ends +// where its container says it must is the caller's check (der_read_exact, der_children). +fn der_read_element(input: List, at: Int) -> DerRead { + match octet_at(input: input, at: at) { + Absent => DerReadRefused { cause: DerTruncated { at: at, needed: 1, available: 0 } } + Present { value: identifier } => + match octet_bit_field(octet: identifier, shift: 0, mask: 31) { + Absent => DerReadRefused { cause: DerHighTagNumberUnsupported { at: at } } + Present { value: tag } => + if tag == 31 { + DerReadRefused { cause: DerHighTagNumberUnsupported { at: at } } + } else { + match octet_bit_field(octet: identifier, shift: 6, mask: 3) { + Absent => DerReadRefused { cause: DerHighTagNumberUnsupported { at: at } } + Present { value: class_bits } => + match der_read_length(input: input, at: at + 1) { + DerLengthRefused { cause: c } => DerReadRefused { cause: c } + DerLengthReady { length: l } => + match octet_span_read(input: input, at: l.content_start, length: l.length) { + OctetSpanRefused { cause: c } => DerReadRefused { cause: der_refusal_of_octet_read(cause: c) } + OctetSpanReady { span: content } => + DerReadReady { + element: DerElement { + class: der_tag_class(bits: class_bits), + constructed: octet_bit_is_set(octet: identifier, bit: 5), + tag: tag, + whole: OctetSpan { start: at, end: content.end }, + content: content, + } + } + } + } + } + } + } + } +} + +// One element that must occupy [at, end) exactly -- a certificate inside an x5c byte string, or the +// value of an extension's OCTET STRING. +fn der_read_exact(input: List, span: OctetSpan) -> DerRead { + match der_read_element(input: input, at: span.start) { + DerReadRefused { cause: c } => DerReadRefused { cause: c } + DerReadReady { element: e } => + if e.whole.end == span.end { + DerReadReady { element: e } + } else if e.whole.end < span.end { + DerReadRefused { cause: DerTrailingInput { at: e.whole.end, remaining: span.end - e.whole.end } } + } else { + DerReadRefused { cause: DerTruncated { at: span.end, needed: e.whole.end - span.end, available: 0 } } + } + } +} + +fn der_children_from(input: List, at: Int, end: Int, acc: List) -> DerChildren { + if at == end { + DerChildrenReady { children: acc } + } else { + match der_read_element(input: input, at: at) { + DerReadRefused { cause: c } => DerChildrenRefused { cause: c } + DerReadReady { element: e } => + if e.whole.end > end { + DerChildrenRefused { cause: DerTruncated { at: end, needed: e.whole.end - end, available: 0 } } + } else { + der_children_from(input: input, at: e.whole.end, end: end, acc: acc |> list_push(e)) + } + } + } +} + +// The elements a constructed element's content consists of, which must tile it exactly. +fn der_children(input: List, parent: DerElement) -> DerChildren { + der_children_from(input: input, at: parent.content.start, end: parent.content.end, acc: []) +} + +fn der_is(element: DerElement, class: DerTagClass, tag: Int) -> Bool { + element.tag == tag && match class { + DerUniversal => match element.class { DerUniversal => true _ => false } + DerApplication => match element.class { DerApplication => true _ => false } + DerContextSpecific => match element.class { DerContextSpecific => true _ => false } + DerPrivate => match element.class { DerPrivate => true _ => false } + } +} + +fn der_expect(element: DerElement, class: DerTagClass, tag: Int) -> DerRead { + if der_is(element: element, class: class, tag: tag) { + DerReadReady { element: element } + } else { + DerReadRefused { cause: DerUnexpectedElement { at: element.whole.start, expected_tag: tag } } + } +} + +fn der_expect_universal(element: DerElement, tag: Int) -> DerRead { + der_expect(element: element, class: DerUniversal, tag: tag) +} + +// ── Primitive values ───────────────────────────────────────────────────────────────────────── + +// INTEGER content, checked minimal (X.690 8.3.2): no leading 0x00 before an octet < 0x80, and no +// leading 0xFF before an octet >= 0x80. The value itself stays a span: serial numbers and ECDSA +// scalars are wider than any machine word, and their consumers compare or hand on the octets. +fn der_integer_content(input: List, element: DerElement) -> DerRead { + match der_expect_universal(element: element, tag: der_tag_integer) { + DerReadRefused { cause: c } => DerReadRefused { cause: c } + DerReadReady { element: e } => + if octet_span_length(span: e.content) == 0 { + DerReadRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + } else if octet_span_length(span: e.content) == 1 { + DerReadReady { element: e } + } else { + match octet_in_span(input: input, span: e.content, at: e.content.start) { + Absent => DerReadRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + Present { value: first } => + match octet_in_span(input: input, span: e.content, at: e.content.start + 1) { + Absent => DerReadRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + Present { value: second } => + if (first == 0 && second < 128) || (first == 255 && second >= 128) { + DerReadRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + } else { + DerReadReady { element: e } + } + } + } + } + } +} + +type DerSmallInteger + = DerSmallIntegerReady { value: Int } + | DerSmallIntegerRefused { cause: DerRefusal } + +// A non-negative INTEGER small enough for a machine word (certificate version, pathLenConstraint). +fn der_small_unsigned(input: List, element: DerElement) -> DerSmallInteger { + match der_integer_content(input: input, element: element) { + DerReadRefused { cause: c } => DerSmallIntegerRefused { cause: c } + DerReadReady { element: e } => + match octet_in_span(input: input, span: e.content, at: e.content.start) { + Absent => DerSmallIntegerRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + Present { value: first } => + if first >= 128 { + DerSmallIntegerRefused { cause: DerNoncanonicalInteger { at: e.whole.start } } + } else { + match octet_read_unsigned_be(input: input, at: e.content.start, octets: octet_span_length(span: e.content)) { + OctetUnsignedRefused { cause: c } => DerSmallIntegerRefused { cause: der_refusal_of_octet_read(cause: c) } + OctetUnsignedReady { value: v, end: _ } => DerSmallIntegerReady { value: v } + } + } + } + } +} + +type DerBoolean + = DerBooleanReady { value: Bool } + | DerBooleanRefused { cause: DerRefusal } + +fn der_boolean(input: List, element: DerElement) -> DerBoolean { + match der_expect_universal(element: element, tag: der_tag_boolean) { + DerReadRefused { cause: c } => DerBooleanRefused { cause: c } + DerReadReady { element: e } => + if octet_span_length(span: e.content) != 1 { + DerBooleanRefused { cause: DerNoncanonicalBoolean { at: e.whole.start } } + } else { + match octet_in_span(input: input, span: e.content, at: e.content.start) { + Absent => DerBooleanRefused { cause: DerNoncanonicalBoolean { at: e.whole.start } } + Present { value: b } => + if b == 0 { + DerBooleanReady { value: false } + } else if b == 255 { + DerBooleanReady { value: true } + } else { + DerBooleanRefused { cause: DerNoncanonicalBoolean { at: e.whole.start } } + } + } + } + } +} + +type DerBitString { + unused_bits: Int + bits: OctetSpan +} + +type DerBitStringRead + = DerBitStringReady { value: DerBitString } + | DerBitStringRefused { cause: DerRefusal } + +fn der_bit_string(input: List, element: DerElement) -> DerBitStringRead { + match der_expect_universal(element: element, tag: der_tag_bit_string) { + DerReadRefused { cause: c } => DerBitStringRefused { cause: c } + DerReadReady { element: e } => + match octet_in_span(input: input, span: e.content, at: e.content.start) { + Absent => DerBitStringRefused { cause: DerBitStringMalformed { at: e.whole.start } } + Present { value: unused } => + if unused > 7 || (unused > 0 && octet_span_length(span: e.content) == 1) { + DerBitStringRefused { cause: DerBitStringMalformed { at: e.whole.start } } + } else { + DerBitStringReady { + value: DerBitString { unused_bits: unused + 0, bits: OctetSpan { start: e.content.start + 1, end: e.content.end } } + } + } + } + } +} + +fn der_octet_string(element: DerElement) -> DerRead { + der_expect_universal(element: element, tag: der_tag_octet_string) +} + +type DerObjectIdentifier + = DerObjectIdentifierReady { arcs: List } + | DerObjectIdentifierRefused { cause: DerRefusal } + +type DerArcState { + arcs: List + pending: Int + started: Bool + malformed: Bool +} + +// X.690 8.19: base-128 subidentifiers, high bit set on every octet but the last, no leading 0x80 +// octet (which would be a non-minimal encoding), and the first subidentifier split as 40 * a + b. +fn der_arc_step(input: List, st: DerArcState, octet: UInt8) -> DerArcState { + if st.malformed { + st + } else { + match octet_bit_field(octet: octet, shift: 0, mask: 127) { + Absent => DerArcState { arcs: st.arcs, pending: 0, started: false, malformed: true } + Present { value: low } => + if !st.started && octet == 128 { + DerArcState { arcs: st.arcs, pending: 0, started: false, malformed: true } + } else if octet_bit_is_set(octet: octet, bit: 7) { + DerArcState { arcs: st.arcs, pending: st.pending * 128 + low, started: true, malformed: false } + } else { + DerArcState { arcs: st.arcs |> list_push(st.pending * 128 + low), pending: 0, started: false, malformed: false } + } + } + } +} + +fn der_oid_first_arcs(first: Int) -> List { + if first < 40 { [0, first] } else if first < 80 { [1, first - 40] } else { [2, first - 80] } +} + +fn der_object_identifier(input: List, element: DerElement) -> DerObjectIdentifier { + match der_expect_universal(element: element, tag: der_tag_object_identifier) { + DerReadRefused { cause: c } => DerObjectIdentifierRefused { cause: c } + DerReadReady { element: e } => { + let octets = input.skip(n: e.content.start).take(n: octet_span_length(span: e.content)) + let st = fold(octets, init: DerArcState { arcs: [], pending: 0, started: false, malformed: false }, + f: (acc, octet) => der_arc_step(input: input, st: acc, octet: octet)) + if st.malformed || st.started || count(st.arcs) == 0 { + DerObjectIdentifierRefused { cause: DerObjectIdentifierMalformed { at: e.whole.start } } + } else { + match st.arcs.first() { + Absent => DerObjectIdentifierRefused { cause: DerObjectIdentifierMalformed { at: e.whole.start } } + Present { value: first } => + DerObjectIdentifierReady { arcs: append(der_oid_first_arcs(first: first), items: st.arcs.skip(n: 1)) } + } + } + } + } +} diff --git a/dag/extdeps/npm.dag b/dag/extdeps/npm.dag index b70d895f9d4..bdb613a24f1 100644 --- a/dag/extdeps/npm.dag +++ b/dag/extdeps/npm.dag @@ -270,7 +270,10 @@ fn npm_octets_to_lower_hex(octets: List) -> String { } fn npm_sri_base64_payload_is_canonical(encoded: String, octets: List) -> Bool { - encoded == base64_encode(octets: octets, variant: Standard) + match base64_encode(octets: octets, variant: Standard) { + Present { value: canonical } => encoded == canonical + Absent => false + } } fn npm_decode_integrity_expression(expression: String) -> NpmIntegrityDecode { diff --git a/dag/extdeps/time/posix_epoch.dag b/dag/extdeps/time/posix_epoch.dag new file mode 100644 index 00000000000..4691219b134 --- /dev/null +++ b/dag/extdeps/time/posix_epoch.dag @@ -0,0 +1,75 @@ +module extdeps.time.posix_epoch + +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// SECONDS SINCE THE EPOCH, POSIX.1-2017 Base Definitions 4.16: a UTC civil date-time (proleptic +// Gregorian calendar, leap seconds not counted) maps to +// tm_sec + tm_min*60 + tm_hour*3600 + days_since_1970_01_01 * 86400. +// Its consumer is extdeps.ietf.x509, whose validity times (UTCTime, GeneralizedTime) are civil +// date-times that a verifier compares against a caller's epoch-seconds `now`. +// +// days_from_civil is the proleptic-Gregorian day count in era form (400-year cycles of 146097 days), +// the arithmetic the POSIX definition's own expression expands to, stated once here so no parser +// re-derives calendar arithmetic. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "pubs.opengroup.org/onlinepubs/9699919799/basedefs/V1_chap04.html#tag_04_16" + } +} + +type CivilDateTime { + year: Int + month: Int + day: Int + hour: Int + minute: Int + second: Int +} + +fn civil_is_leap_year(year: Int) -> Bool { + (year % 4 == 0 && year % 100 != 0) || year % 400 == 0 +} + +fn civil_days_in_month(year: Int, month: Int) -> Int { + if month == 2 { + if civil_is_leap_year(year: year) { 29 } else { 28 } + } else if month == 4 || month == 6 || month == 9 || month == 11 { + 30 + } else { + 31 + } +} + +// A civil date-time whose fields are in range. Second 60 is refused: POSIX time does not count leap +// seconds, and X.509 (RFC 5280 4.1.2.5) forbids them in validity times. +fn civil_is_valid(t: CivilDateTime) -> Bool { + t.month >= 1 && t.month <= 12 + && t.day >= 1 && t.day <= civil_days_in_month(year: t.year, month: t.month) + && t.hour >= 0 && t.hour <= 23 + && t.minute >= 0 && t.minute <= 59 + && t.second >= 0 && t.second <= 59 +} + +fn civil_floor_div(a: Int, b: Int) -> Int { + if a >= 0 { a / b } else { 0 - ((0 - a + b - 1) / b) } +} + +fn days_from_civil(year: Int, month: Int, day: Int) -> Int { + let y = if month <= 2 { year - 1 } else { year } + let era = civil_floor_div(a: y, b: 400) + let yoe = y - era * 400 + let mp = if month > 2 { month - 3 } else { month + 9 } + let doy = (153 * mp + 2) / 5 + day - 1 + let doe = yoe * 365 + yoe / 4 - yoe / 100 + doy + era * 146097 + doe - 719468 +} + +fn civil_epoch_seconds(t: CivilDateTime) -> Int? { + if civil_is_valid(t: t) { + Present { value: days_from_civil(year: t.year, month: t.month, day: t.day) * 86400 + t.hour * 3600 + t.minute * 60 + t.second } + } else { + none + } +} diff --git a/dag/extdeps/time/rfc3339.dag b/dag/extdeps/time/rfc3339.dag index 596c4809986..2f2ae4e51f1 100644 --- a/dag/extdeps/time/rfc3339.dag +++ b/dag/extdeps/time/rfc3339.dag @@ -3,6 +3,7 @@ module extdeps.time.rfc3339 import std.types { Bool, String, NonEmptyStr } import std.algebra { Less, Equal, Greater } import std.string_type { string_lex_compare } +import extdeps.time.posix_epoch { CivilDateTime, civil_epoch_seconds } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } @@ -90,3 +91,47 @@ fn rfc3339_compare(left: Rfc3339Timestamp, right: Rfc3339Timestamp) -> Rfc3339Co } } } + +// THE REAL PARSE the comparator above tells callers to supply, for the one spelling it admits +// without fractional seconds: YYYY-MM-DDTHH:MM:SSZ, exactly twenty characters, uppercase T and Z. +// It yields POSIX epoch seconds through extdeps.time.posix_epoch, so an RFC 3339 instant and an +// X.509 validity time are compared on one scale. Any other spelling is absent, never approximated. +fn rfc3339_digit_at(value: String, at: Int) -> Int? { + let cp = code_point(substring(s: value, start: at, end: at + 1)) + if cp >= 48 && cp <= 57 { Present { value: cp - 48 } } else { none } +} + +fn rfc3339_number_at(value: String, at: Int, digits: Int, acc: Int) -> Int? { + if digits == 0 { + Present { value: acc } + } else { + match rfc3339_digit_at(value: value, at: at) { + Absent => none + Present { value: d } => rfc3339_number_at(value: value, at: at + 1, digits: digits - 1, acc: acc * 10 + d) + } + } +} + +fn rfc3339_separators_hold(value: String) -> Bool { + substring(s: value, start: 4, end: 5) == "-" + && substring(s: value, start: 7, end: 8) == "-" + && substring(s: value, start: 10, end: 11) == rfc3339_date_time_separator + && substring(s: value, start: 13, end: 14) == ":" + && substring(s: value, start: 16, end: 17) == ":" + && substring(s: value, start: 19, end: 20) == rfc3339_utc_designator +} + +fn rfc3339_epoch_seconds(value: String) -> Int? { + if string_length(s: value) != 20 || !rfc3339_separators_hold(value: value) { + none + } else { + match rfc3339_number_at(value: value, at: 0, digits: 4, acc: 0) { Absent => none Present { value: year } => + match rfc3339_number_at(value: value, at: 5, digits: 2, acc: 0) { Absent => none Present { value: month } => + match rfc3339_number_at(value: value, at: 8, digits: 2, acc: 0) { Absent => none Present { value: day } => + match rfc3339_number_at(value: value, at: 11, digits: 2, acc: 0) { Absent => none Present { value: hour } => + match rfc3339_number_at(value: value, at: 14, digits: 2, acc: 0) { Absent => none Present { value: minute } => + match rfc3339_number_at(value: value, at: 17, digits: 2, acc: 0) { Absent => none Present { value: second } => + civil_epoch_seconds(t: CivilDateTime { year: year, month: month, day: day, hour: hour, minute: minute, second: second }) + } } } } } } + } +} diff --git a/dag/gunbc/auth/approval_capability.dag b/dag/gunbc/auth/approval_capability.dag index 2d9dfdcbc2d..c0e4c52d165 100644 --- a/dag/gunbc/auth/approval_capability.dag +++ b/dag/gunbc/auth/approval_capability.dag @@ -178,6 +178,7 @@ type CapabilityIssuanceRefusal = IssuanceKeyIdDisagrees { claimed: MacKeyId, signing_key: MacKeyId } | IssuanceKeyMaterialNotHex { key_id: MacKeyId } | IssuanceImplementationTagNotHex { key_id: MacKeyId } + | IssuanceImplementationTagNotOctets { key_id: MacKeyId } type CapabilityIssuance = CapabilityIssued { capability: ApprovalCapability } @@ -196,11 +197,15 @@ fn issue_capability(claims: ApprovalCapabilityClaims, key: MacKey) -> Capability match base16_decode_lower(hex: t.hex as String) { Absent => CapabilityIssuanceRefused { cause: IssuanceImplementationTagNotHex { key_id: t.key_id } } Present { value: octets } => - CapabilityIssued { - capability: ApprovalCapability { - claims: claims, - tag_b64url: base64_encode(octets: octets, variant: UrlSafe) as NonEmptyStr, - } + match base64_encode(octets: octets, variant: UrlSafe) { + Absent => CapabilityIssuanceRefused { cause: IssuanceImplementationTagNotOctets { key_id: t.key_id } } + Present { value: encoded } => + CapabilityIssued { + capability: ApprovalCapability { + claims: claims, + tag_b64url: encoded as NonEmptyStr, + } + } } } } @@ -216,10 +221,14 @@ fn capability_tag_hex(capability: ApprovalCapability) -> NonEmptyStr? { match base64_decode(s: presented, variant: UrlSafe) { Absent => none Present { value: octets } => - if base64_encode(octets: octets, variant: UrlSafe) != presented || octets == [] { - none - } else { - Present { value: base16_encode_lower(octets: octets) as NonEmptyStr } + match base64_encode(octets: octets, variant: UrlSafe) { + Absent => none + Present { value: canonical } => + if canonical != presented || octets == [] { + none + } else { + Present { value: base16_encode_lower(octets: octets) as NonEmptyStr } + } } } } diff --git a/dag/gunbc/auth/approval_device_redemption.dag b/dag/gunbc/auth/approval_device_redemption.dag index 2710354e370..dc816df81b1 100644 --- a/dag/gunbc/auth/approval_device_redemption.dag +++ b/dag/gunbc/auth/approval_device_redemption.dag @@ -13,7 +13,9 @@ import extdeps.apple.apns { import extdeps.apple.app_attest { AttestKeyId, AttestationVerification, AttestationVerified, AttestationRefused, AttestationRefusal, AssertionVerification, AssertionAuthentic, AssertionRefused, AssertionRefusal, + AppAttestEnvironment, AppAttestLaunchExtensionPolicy, app_attest_verify, } +import extdeps.time.rfc3339 { rfc3339_epoch_seconds } import extdeps.apple.secure_enclave { EnclaveKeyAccessPolicy, BiometryCurrentSet } import extdeps.crypto.mac { MacKey, MacVerified, mac_verify } import gunbc.auth.approval_capability { @@ -128,6 +130,7 @@ type EnrolmentRefusal | EnrolmentAttestationRefused { cause: AttestationRefusal } | EnrolmentAttestationForOtherBytes | EnrolmentAndroidUnrealized + | EnrolmentObservationTimeUnreadable { observed_at: Timestamp } type EnrolmentAdmission = EnrolmentAdmitted { enrollment: VerifiedDeviceEnrollment } @@ -178,6 +181,40 @@ fn enrolment_admission( } } +// THE iOS ENROLMENT ROUTE'S PARSE STAGE (ENCODING-0, gunbc#11629). The attestation arrives as the +// app's base64 bytes and is decoded and checked in .dag by extdeps.apple.app_attest app_attest_verify +// -- CBOR, the DER certificate chain under the pinned Apple root, the authenticator data -- rather +// than by a host parser. Its `now` is the same instant as observed_at, read through +// extdeps.time.rfc3339, so certificate validity and code expiry are judged at one time. Until ECDSA +// is realized (ecdsa_verification_realization_frontier) every genuine attestation ends in +// AttestationVerificationUnrealized, which enrolment_admission refuses like any other refusal: this +// route never admits an enrolment its evidence did not verify. +fn ios_enrolment_admission( + slot: EnrolmentSlotStanding, + decision_key: VerifyingKey, + attestation_b64: NonEmptyStr, + key_id: AttestKeyId, + environment: AppAttestEnvironment, + policy: AppAttestLaunchExtensionPolicy, + admitted_categories: List, + observed_at: Timestamp, +) -> EnrolmentAdmission { + match rfc3339_epoch_seconds(value: observed_at) { + Absent => EnrolmentRefused { cause: EnrolmentObservationTimeUnreadable { observed_at: observed_at } } + Present { value: now_epoch } => + enrolment_admission( + slot: slot, + platform: MobileIos, + decision_key: decision_key, + attestation: app_attest_verify( + environment: environment, policy: policy, admitted_categories: admitted_categories, + attestation_b64: attestation_b64, key_id: key_id, now_epoch: now_epoch, + ), + observed_at: observed_at, + ) + } +} + // ── Push provider outcome ──────────────────────────────────────────────────────────────────── // Named for what a provider can establish: it ACCEPTED the message. Not delivered, not displayed, // never consent. retryable is Apple's reading of its own status, not a policy here. @@ -760,7 +797,7 @@ data approval_device_routes_frontier: DissolutionCondition = unbound_dissolution ) data ecdsa_verification_realization_frontier: DissolutionCondition = unbound_dissolution( - description: "host primitives binding RustCrypto p256 ECDSA verification behind extdeps.crypto.signature signature_verification_from_implementation, and an App Attest attestation and assertion verifier (CBOR decode, X.509 chain to the pinned Apple App Attestation Root CA, App ID prefix RP ID, validation category and bundle version) behind extdeps.apple.app_attest attestation_verification_from_implementation and assertion_verification_from_implementation -- SUFFICIENT FOR the device routes to mint SignatureVerified, AttestationVerified and AssertionAuthentic from real bytes", + description: "a realization of ECDSA verification (P-256 and P-384 over SHA-256/SHA-384) behind extdeps.crypto.signature signature_verification_from_implementation, and of SHA-256, consumed by extdeps.apple.app_attest app_attest_verify and app_attest_verify_assertion for the steps they report today as AppAttestEcdsaSignatureVerification and AppAttestSha256Digest (the certificate-chain signatures under the pinned Apple root, the nonce, the key id and the App ID RP ID hash) -- SUFFICIENT FOR the device routes to mint SignatureVerified, AttestationVerified and AssertionAuthentic from real bytes. The App Attest WIRE DECODING this row once also named -- CBOR, the DER/X.509 chain, authenticator data and the structural RFC 5280 path checks -- is realized in .dag (extdeps.ietf.cbor, extdeps.itu.der, extdeps.ietf.x509, gunbc#11629) and is no longer part of this frontier", ) data ios_realization_frontier: DissolutionCondition = unbound_dissolution( diff --git a/dag/gunbc/auth/approval_device_wire.dag b/dag/gunbc/auth/approval_device_wire.dag index 173790862f4..00d7c697aa4 100644 --- a/dag/gunbc/auth/approval_device_wire.dag +++ b/dag/gunbc/auth/approval_device_wire.dag @@ -12,7 +12,7 @@ import extdeps.android.key_attestation { AndroidAttestationChain } import gunbc.auth.approval_capability { ProposedDecision, ProposeApprove, ProposeDeny, proposed_decision_name } import std.logic { Bool } import std.encoding { base64_encode, base64_decode, UrlSafe, utf8_decode_octets } -import std.bytes { utf8_encode_bytes, bytes_octets } +import std.bytes { utf8_encode_bytes, bytes_octets, pure_dag_seam_unreachable_string } import std.integer { UInt8 } import extdeps.languages.json.emit { JsonValue, JsonObject, JsonString, JsonKeyValue, serialize_json, json_object, json_kv, json_string, json_array } import extdeps.languages.json.parse { @@ -826,8 +826,27 @@ fn device_push_update_client_data(enrollment_id: NonEmptyStr, requested_at: Time // utf8_encode_bytes / bytes_octets for UTF-8 and std.encoding base64_encode for base64url. data path_segment_prefix: String = "id-" +// base64_encode GAINED A REFUSAL CHANNEL in gunbc#11643, which landed the modeled word substrate +// under std.encoding: an octet outside the byte range used to be multiplied into a plausible wrong +// string and now refuses. This call site arrived on main from gunbc#11660 while that PR was in +// review, so the two are correct separately and wrong together -- nothing overlaps textually, the +// merge is clean, and the Optional was being joined into the path segment itself. +// +// THE ARM IS UNREACHABLE HERE, and that is a statement about this call rather than about +// base64_encode: the octets are the UTF-8 encoding of a String, so every member is a byte by +// construction. THE DECLARED CONTRACT IS TOTALITY -- the annotation above says this segment is +// total and injective and never refused, and every identity the store admits has a route -- so +// threading an Optional out of here would not be honesty, it would be a different and weaker +// contract at a route-identity boundary, rippling into decode_path_segment and the wire model. +// std.bytes' divergent seam is the corpus's declared idiom for an arm that cannot be reached: it +// diverges rather than fabricating, which keeps the totality claim true instead of quietly false. +// Same treatment, same reason, as extdeps.cloud.gcp.secret_manager +// encode_sm_access_version_payload_wire in that same PR. fn path_segment(s: NonEmptyStr) -> NonEmptyStr { - join([path_segment_prefix, base64_encode(octets: bytes_octets(b: utf8_encode_bytes(s: s as String)), variant: UrlSafe)], "") as NonEmptyStr + match base64_encode(octets: bytes_octets(b: utf8_encode_bytes(s: s as String)), variant: UrlSafe) { + Present { value: encoded } => join([path_segment_prefix, encoded], "") as NonEmptyStr + Absent => pure_dag_seam_unreachable_string() as NonEmptyStr + } } // THE SERVER'S INVERSE, typed and consuming the raw route suffix exactly once. The route takes the diff --git a/dag/gunbc/census_closure_frontier.dag b/dag/gunbc/census_closure_frontier.dag index 78ca0405c57..bd69c9a7ea0 100644 --- a/dag/gunbc/census_closure_frontier.dag +++ b/dag/gunbc/census_closure_frontier.dag @@ -60,6 +60,7 @@ import extdeps.ebay.marketplace_account_deletion { ebay_account_deletion_frontie import gunbc.cloudflare.r2_permission_group_observe { cloudflare_permission_group_observation_frontier_rows } import gunbc.where_refinement_predicate_vocabulary { http_status_where_clause_names_declaration_frontier_rows } import gunbc.arm_ci_seller_census { arm_ci_seller_census_later_consumer_frontier_rows } +import std.machine_word { machine_word_consumer_frontier_rows } import product.data_class { data_class_frontier_rows } import product.data_category { data_category_frontier_rows } @@ -129,6 +130,7 @@ fn census_closure_frontier_row_groups() -> List> { job_admission_frontier_rows, arm_ci_seller_census_later_consumer_frontier_rows, runner_canary_executed_evidence_frontier, + machine_word_consumer_frontier_rows, ] } diff --git a/dag/gunbc/plans/blackjack_onboarding.dag b/dag/gunbc/plans/blackjack_onboarding.dag index 98a2226a143..76cd41c5c60 100644 --- a/dag/gunbc/plans/blackjack_onboarding.dag +++ b/dag/gunbc/plans/blackjack_onboarding.dag @@ -133,7 +133,7 @@ fn section_4_model() -> List { h3(text: "4.4 `examples.blackjack.shuffle` — the boundary"), p(text: "Anchor in the file: `ShuffleSeed`. Two pure functions and nothing else: a seed-to-permutation and a bytes-to-seed. The **only** effectful call in the whole project lives in one test (§7), not here."), - code(text: "module examples.blackjack.shuffle\n\nimport std.integer { UInt8 }\nimport std.encoding { base64_octet_int }\nimport examples.blackjack.cards { Card }\nimport examples.blackjack.round { Shoe }\n\ntype ShuffleSeed { value: Int }\n\n// Deterministic: same deck + same seed = same shoe. A linear congruential step\n// threaded through a fold over positions is enough; this is a teaching fixture,\n// not a claim about randomness quality.\nfn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { … }\n\n// The step function of the generator, exposed so a test can pin its sequence.\nfn next_seed(seed: ShuffleSeed) -> ShuffleSeed { … }\n\n// The bridge from the entropy boundary. The octets arrive as the List that\n// std.encoding.base64_decode returns; base64_octet_int (same module) reads each one as an\n// Int, and a fold combines them. Take the real decoded type here -- do not mint an Int list.\nfn seed_from_octets(octets: List) -> ShuffleSeed { … }\n"), + code(text: "module examples.blackjack.shuffle\n\nimport std.integer { UInt8 }\nimport std.encoding { base64_octet_word }\nimport examples.blackjack.cards { Card }\nimport examples.blackjack.round { Shoe }\n\ntype ShuffleSeed { value: Int }\n\n// Deterministic: same deck + same seed = same shoe. A linear congruential step\n// threaded through a fold over positions is enough; this is a teaching fixture,\n// not a claim about randomness quality.\nfn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { … }\n\n// The step function of the generator, exposed so a test can pin its sequence.\nfn next_seed(seed: ShuffleSeed) -> ShuffleSeed { … }\n\n// The bridge from the entropy boundary. The octets arrive as the List that\n// std.encoding.base64_decode returns; base64_octet_word (same module) ADMITS each one through\n// word_of_int at Width8, so an octet outside the byte range refuses rather than being renamed,\n// and a fold combines them. Take the real decoded type here -- do not mint an Int list.\nfn seed_from_octets(octets: List) -> ShuffleSeed { … }\n"), h3(text: "4.5 `examples.blackjack.simulation` — analysis"), p(text: "Anchor in the file: `Strategy`. Reuses the engine; reimplements nothing. Each round emits one observation; a summary is a fold over observations; and the reconciliation invariant is a **test**, not an assumption of the report."), @@ -153,7 +153,7 @@ fn section_5_tests() -> List { ol(items: [ li(text: "**Pure unit tests** supply cards, hands and values directly. Most of your tests."), li(text: "**State-transition tests** supply a complete `RoundState` and an action, and assert the exact next state or the exact refusal. One test per refusal arm."), - li(text: "**Boundary tests** supply the value an effectful producer *would* return — a `List` of octets (built with `std.encoding` `base64_octet_of_int`, the same constructor the decoder uses) handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer."), + li(text: "**Boundary tests** supply the value an effectful producer *would* return — a `List` of octets written directly, which is exactly the type `std.encoding` `base64_decode` returns, handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer."), li(text: "**One integration test** calls the real producer, `Urandom.ReadBytes`, and establishes only that its output inhabits the shape the boundary tests assumed (the right number of octets, decodable). It does not assert that a random shoe has any particular order."), ]), p(text: "Level 3 without level 4 is the trap DESIGN §3 names: a suite that is fast, green, and proves no program, because every boundary was supplied and none was ever executed. Level 4 is what turns your supplied inputs from hypotheses into readings. Keep it to one test, keep it narrow, and know that it is *wet* — it shells out — so it runs with `--wet` locally and is the one that can fail for reasons that are not yours."), @@ -165,7 +165,7 @@ fn section_5_tests() -> List { fn section_6_randomness() -> List { [ h2(text: "6. The randomness boundary"), - p(text: "Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and reads each octet with `base64_octet_int` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes."), + p(text: "Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and admits each octet with `base64_octet_word` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes."), p(text: "The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, so a surprising row in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck."), ] } diff --git a/dag/std/bytes.dag b/dag/std/bytes.dag index 20159884c2e..09c1dece78d 100644 --- a/dag/std/bytes.dag +++ b/dag/std/bytes.dag @@ -36,6 +36,17 @@ fn pure_dag_seam_unreachable_float() -> Float { // dissolve-on a bottom type, at which point one divergent seam inhabits every result type and the // Float projection deletes. +// The String projection of the same divergence, added for the same reason the Float one exists and +// borrowing the Int seam's divergence the same way: a caller whose result type is String and whose +// refusal arm is unreachable BY CONSTRUCTION has nowhere to put a value, and "" is a perfectly good +// String, which is exactly what makes it a fabricated plausible output. The condition forces the +// Int seam to evaluate, so divergence happens before any String is produced; both arms are the same +// literal because neither is ever reached. DISSOLVE-ON: the same bottom type the Float projection +// names -- one divergent seam inhabits every result type and both projections delete. +fn pure_dag_seam_unreachable_string() -> String { + if pure_dag_seam_unreachable() == 0 { "" } else { "" } +} + fn bytes_octets(b: Bytes) -> List { [pure_dag_seam_unreachable()] } diff --git a/dag/std/encoding.dag b/dag/std/encoding.dag index b8f041849b5..447a4b171b5 100644 --- a/dag/std/encoding.dag +++ b/dag/std/encoding.dag @@ -3,6 +3,8 @@ module std.encoding import std.algebra { BoundedLattice } import std.types { Bytes } import std.integer { UInt8 } +import std.machine_word { Word, Width8, Width32, WordResult, WordReady, WordRefused, OctetsReady, OctetsRefused, QualifiedWord, word_of_int, word_from_octets, word_to_octets, word_shift_left, word_shift_right, word_and, word_or, octet_int_values } +import extdeps.toolchain.architecture_profile { BigEndian } import std.bytes { pure_dag_seam_unreachable } import std.disposition { Disposition, Scaffold, Terminal, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } @@ -136,63 +138,192 @@ type Base64EncodeState { buf: Base64EncodeBuf } -fn base64_octet_int(b: UInt8) -> Int { - b + 0 +// BASE64 IS A BIT PACKING, AND UNTIL NOW IT SAID SO IN LITERALS. Three octets become one 24-bit +// group and four six-bit fields; the previous form spelled that as x * 65536 + y * 256 + octet and +// (n / 262144) % 64, where 65536 is a byte shift, 262144 is a sextet shift and 64 is a six-bit +// mask. Those are shifts and masks written as decimal magic numbers, which is width and place as +// PROSE -- nothing in the corpus could tell that 4096 was a shift rather than a quantity, no +// refusal existed for an octet outside the byte range, and the crossings in and out of UInt8 were +// `b + 0` and `n`, two identity functions asserting a width they never checked. std.machine_word +// now carries the width as a fact the value holds, so this file states the packing and the +// substrate states the arithmetic. THE ENCODING MODEL IS UNCHANGED -- alphabet, grouping, padding +// and variant behaviour are exactly as before, byte for byte; only the arithmetic moved, and the +// refusal channel appears because an out-of-range octet previously produced a wrong answer rather +// than an error. std.encoding's Base64 authority is ENCODING-0's (gunbc#11629) to grow; this change +// is NUMERIC-BIT-0 (gunbc#11627) substituting the bit arithmetic underneath it. + +fn base64_group_word(octets: List) -> WordResult { + word_from_octets(width: Width32, octets: octets, endianness: BigEndian) } -fn base64_sextet_char(alphabet: String, n: Int, divisor: Int) -> String { - char_at(alphabet, (n / divisor) % 64) +fn base64_octet_word(b: UInt8) -> WordResult { + word_of_int(width: Width8, value: b + 0) } -fn base64_encode_step(st: Base64EncodeState, octet: Int, alphabet: String) -> Base64EncodeState { +fn base64_sextet_mask() -> WordResult { + word_of_int(width: Width32, value: 63) +} + +// The group is a 32-bit word whose top octet is zero, because 24 is not a machine width this +// substrate realizes and inventing a Width24 for one caller would be a width authority minted for +// a convenience. The leading zero octet is the packing's own statement that the group occupies the +// low three octets, and every field offset below is measured from that. +fn base64_zero_octet() -> WordResult { + word_of_int(width: Width8, value: 0) +} + +fn base64_sextet_at(group: Word, offset: Int) -> Int? { + match word_shift_right(a: group, amount: offset) { + WordRefused { cause: _ } => none + WordReady { word: shifted } => + match base64_sextet_mask() { + WordRefused { cause: _ } => none + WordReady { word: mask } => + match word_and(a: shifted, b: mask) { + WordRefused { cause: _ } => none + WordReady { word: field } => Present { value: field.value } + } + } + } +} + +fn base64_sextet_char_at(alphabet: String, group: Word, offset: Int) -> String? { + match base64_sextet_at(group: group, offset: offset) { + Absent => none + Present { value: n } => Present { value: char_at(alphabet, n) } + } +} + +fn base64_group_of_words(a: Word, b: Word, c: Word) -> WordResult { + match base64_zero_octet() { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: zero } => base64_group_word(octets: [zero, a, b, c]) + } +} + +fn base64_group_of_octets(x: UInt8, y: UInt8, z: UInt8) -> WordResult { + match base64_octet_word(b: x) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: a } => + match base64_octet_word(b: y) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: b } => + match base64_octet_word(b: z) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: c } => base64_group_of_words(a: a, b: b, c: c) + } + } + } +} + +fn base64_quad(alphabet: String, group: Word) -> String? { + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 18) { + Absent => none + Present { value: c0 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 12) { + Absent => none + Present { value: c1 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 6) { + Absent => none + Present { value: c2 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 0) { + Absent => none + Present { value: c3 } => Present { value: concat(c0, c1, c2, c3) } + } + } + } + } +} + +fn base64_encode_step(st: Base64EncodeState, octet: UInt8, alphabet: String) -> Base64EncodeState? { match st.buf { - EncEmpty => Base64EncodeState { out: st.out, buf: EncOne { b0: octet } } - EncOne { b0: x } => Base64EncodeState { out: st.out, buf: EncTwo { b0: x, b1: octet } } - EncTwo { b0: x, b1: y } => { - let n = x * 65536 + y * 256 + octet - let quad = concat( - base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144), - base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096), - base64_sextet_char(alphabet: alphabet, n: n, divisor: 64), - char_at(alphabet, n % 64) - ) - Base64EncodeState { out: concat(st.out, quad), buf: EncEmpty } - } + EncEmpty => Present { value: Base64EncodeState { out: st.out, buf: EncOne { b0: octet } } } + EncOne { b0: x } => Present { value: Base64EncodeState { out: st.out, buf: EncTwo { b0: x, b1: octet } } } + EncTwo { b0: x, b1: y } => + match base64_group_of_octets(x: x, y: y, z: octet) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_quad(alphabet: alphabet, group: group) { + Absent => none + Present { value: quad } => Present { value: Base64EncodeState { out: concat(st.out, quad), buf: EncEmpty } } + } + } + } +} + +fn base64_encode_step_optional(st: Base64EncodeState?, octet: UInt8, alphabet: String) -> Base64EncodeState? { + match st { + Absent => none + Present { value: s } => base64_encode_step(st: s, octet: octet, alphabet: alphabet) } } -fn base64_encode_flush(st: Base64EncodeState, alphabet: String) -> String { +fn base64_encode_flush(st: Base64EncodeState, alphabet: String) -> String? { match st.buf { - EncEmpty => st.out - EncOne { b0: x } => { - let n = x * 65536 - concat( - st.out, - base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144), - base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096), - "==" - ) - } - EncTwo { b0: x, b1: y } => { - let n = x * 65536 + y * 256 - concat( - st.out, - base64_sextet_char(alphabet: alphabet, n: n, divisor: 262144), - base64_sextet_char(alphabet: alphabet, n: n, divisor: 4096), - base64_sextet_char(alphabet: alphabet, n: n, divisor: 64), - "=" - ) - } + EncEmpty => Present { value: st.out } + EncOne { b0: x } => + match base64_octet_word(b: x) { + WordRefused { cause: _ } => none + WordReady { word: a } => + match base64_zero_octet() { + WordRefused { cause: _ } => none + WordReady { word: zero } => + match base64_group_of_words(a: a, b: zero, c: zero) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 18) { + Absent => none + Present { value: c0 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 12) { + Absent => none + Present { value: c1 } => Present { value: concat(st.out, c0, c1, "==") } + } + } + } + } + } + EncTwo { b0: x, b1: y } => + match base64_octet_word(b: x) { + WordRefused { cause: _ } => none + WordReady { word: a } => + match base64_octet_word(b: y) { + WordRefused { cause: _ } => none + WordReady { word: b } => + match base64_zero_octet() { + WordRefused { cause: _ } => none + WordReady { word: zero } => + match base64_group_of_words(a: a, b: b, c: zero) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 18) { + Absent => none + Present { value: c0 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 12) { + Absent => none + Present { value: c1 } => + match base64_sextet_char_at(alphabet: alphabet, group: group, offset: 6) { + Absent => none + Present { value: c2 } => Present { value: concat(st.out, c0, c1, c2, "=") } + } + } + } + } + } + } + } } } -fn base64_encode(octets: List, variant: Base64Variant) -> String { +fn base64_encode(octets: List, variant: Base64Variant) -> String? { let alphabet = base64_alphabet(variant: variant) let st = fold(octets, - init: Base64EncodeState { out: "", buf: EncEmpty }, - f: (acc, octet) => base64_encode_step(st: acc, octet: base64_octet_int(b: octet), alphabet: alphabet) + init: Present { value: Base64EncodeState { out: "", buf: EncEmpty } }, + f: (acc, octet) => base64_encode_step_optional(st: acc, octet: octet, alphabet: alphabet) ) - base64_encode_flush(st: st, alphabet: alphabet) + match st { + Absent => none + Present { value: s } => base64_encode_flush(st: s, alphabet: alphabet) + } } fn base64_char_value(c: String, variant: Base64Variant) -> Int? { @@ -247,21 +378,75 @@ type Base64DecodeState { buf: Base64DecodeBuf } -fn base64_decode_step(st: Base64DecodeState, v: Int) -> Base64DecodeState { +// The decode direction is the same packing read backwards: four six-bit fields are placed into one +// 32-bit group and the group's low three octets ARE the answer, so word_to_octets replaces the +// previous (n / 65536) % 256 ladder outright. The leading octet is dropped rather than masked away +// because it is the zero octet base64_group_of_words put there. +fn base64_group_of_sextets(a: Int, b: Int, c: Int, v: Int) -> WordResult { + match base64_place_sextet(value: a, offset: 18) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: wa } => + match base64_place_sextet(value: b, offset: 12) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: wb } => + match base64_place_sextet(value: c, offset: 6) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: wc } => + match base64_place_sextet(value: v, offset: 0) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: wv } => base64_or_all(a: wa, b: wb, c: wc, d: wv) + } + } + } + } +} + +fn base64_place_sextet(value: Int, offset: Int) -> WordResult { + match word_of_int(width: Width32, value: value) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: w } => word_shift_left(a: w, amount: offset) + } +} + +fn base64_or_all(a: Word, b: Word, c: Word, d: Word) -> WordResult { + match word_or(a: a, b: b) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: ab } => + match word_or(a: ab, b: c) { + WordRefused { cause: cause } => WordRefused { cause: cause } + WordReady { word: abc } => word_or(a: abc, b: d) + } + } +} + +fn base64_group_octet_values(group: Word) -> List? { + match word_to_octets(a: group, endianness: BigEndian) { + OctetsRefused { cause: _ } => none + OctetsReady { octets: octets } => Present { value: octet_int_values(octets: octets.skip(n: 1)) } + } +} + +fn base64_decode_step(st: Base64DecodeState, v: Int) -> Base64DecodeState? { match st.buf { - DecEmpty => Base64DecodeState { out: st.out, buf: DecOne { v0: v } } - DecOne { v0: a } => Base64DecodeState { out: st.out, buf: DecTwo { v0: a, v1: v } } - DecTwo { v0: a, v1: b } => Base64DecodeState { out: st.out, buf: DecThree { v0: a, v1: b, v2: v } } - DecThree { v0: a, v1: b, v2: c } => { - let n = a * 262144 + b * 4096 + c * 64 + v - let byte0 = (n / 65536) % 256 - let byte1 = (n / 256) % 256 - let byte2 = n % 256 - Base64DecodeState { - out: st.out |> list_push(byte0) |> list_push(byte1) |> list_push(byte2), - buf: DecEmpty + DecEmpty => Present { value: Base64DecodeState { out: st.out, buf: DecOne { v0: v } } } + DecOne { v0: a } => Present { value: Base64DecodeState { out: st.out, buf: DecTwo { v0: a, v1: v } } } + DecTwo { v0: a, v1: b } => Present { value: Base64DecodeState { out: st.out, buf: DecThree { v0: a, v1: b, v2: v } } } + DecThree { v0: a, v1: b, v2: c } => + match base64_group_of_sextets(a: a, b: b, c: c, v: v) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_group_octet_values(group: group) { + Absent => none + Present { value: octets } => Present { value: Base64DecodeState { out: concat(st.out, octets), buf: DecEmpty } } + } } - } + } +} + +fn base64_decode_step_optional(st: Base64DecodeState?, v: Int) -> Base64DecodeState? { + match st { + Absent => none + Present { value: s } => base64_decode_step(st: s, v: v) } } @@ -269,29 +454,40 @@ fn base64_decode_flush(st: Base64DecodeState) -> List? { match st.buf { DecEmpty => Present { value: st.out } DecOne { v0: _ } => none - DecTwo { v0: a, v1: b } => { - let n = a * 262144 + b * 4096 - Present { value: st.out |> list_push((n / 65536) % 256) } - } - DecThree { v0: a, v1: b, v2: c } => { - let n = a * 262144 + b * 4096 + c * 64 - Present { value: st.out |> list_push((n / 65536) % 256) |> list_push((n / 256) % 256) } - } + DecTwo { v0: a, v1: b } => + match base64_group_of_sextets(a: a, b: b, c: 0, v: 0) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_group_octet_values(group: group) { + Absent => none + Present { value: octets } => Present { value: concat(st.out, octets.take(n: 1)) } + } + } + DecThree { v0: a, v1: b, v2: c } => + match base64_group_of_sextets(a: a, b: b, c: c, v: 0) { + WordRefused { cause: _ } => none + WordReady { word: group } => + match base64_group_octet_values(group: group) { + Absent => none + Present { value: octets } => Present { value: concat(st.out, octets.take(n: 2)) } + } + } } } -fn base64_octet_of_int(n: Int) -> UInt8 { - n -} - +// The crossing back to UInt8 was `fn base64_octet_of_int(n: Int) -> UInt8 { n }` -- an identity +// function whose whole content was an assertion about width that it never checked, so a value +// outside the byte range became a "UInt8" by being named one. It is deleted: every value here came +// out of word_to_octets as a Width8 word, so the range is established by the operation that +// produced it rather than re-asserted by a cast. fn base64_decode_values(vals: List) -> List? { let st = fold(vals, - init: Base64DecodeState { out: [], buf: DecEmpty }, - f: (acc, v) => base64_decode_step(st: acc, v: v) + init: Present { value: Base64DecodeState { out: [], buf: DecEmpty } }, + f: (acc, v) => base64_decode_step_optional(st: acc, v: v) ) - match base64_decode_flush(st: st) { + match st { Absent => none - Present { value: octets } => Present { value: octets |> map(n => base64_octet_of_int(n: n)) } + Present { value: s } => base64_decode_flush(st: s) } } @@ -372,8 +568,27 @@ fn utf8_step(d: Utf8DecodeState, o: Int) -> Utf8DecodeState { } } +// THE OCTET IS ADMITTED, NOT ASSERTED. This fold read each member through base64_octet_int, the +// `b + 0` identity whose whole content was a width claim it never checked -- NUMERIC-BIT-0 +// (gunbc#11627) deleted it, and this consumer arrived on main from gunbc#11660 while that cut was +// in review, so the two are correct separately and refuse together. A semantic conflict, not a +// textual one: nothing overlaps in the diff and the merge is clean. +// +// The replacement is the seam that already exists for base64's own octets: base64_octet_word admits +// the member through word_of_int at Width8, so a value outside the byte range REFUSES instead of +// being renamed. Utf8Refused is the honest destination for that -- a decoder handed something that +// is not an octet has not been handed UTF-8 -- and it is the state this fold already uses for every +// other malformed input, so no new refusal vocabulary is minted for a case the model already had a +// word for. +fn utf8_admit_octet(d: Utf8DecodeState, b: UInt8) -> Utf8DecodeState { + match base64_octet_word(b: b) { + WordRefused { cause: _ } => Utf8Refused + WordReady { word: w } => utf8_step(d: d, o: w.value) + } +} + fn utf8_decode_octets(octets: List) -> List? { - match fold(octets, init: Utf8Ready { out: [] }, f: (d, octet) => utf8_step(d: d, o: base64_octet_int(b: octet))) { + match fold(octets, init: Utf8Ready { out: [] }, f: (d, octet) => utf8_admit_octet(d: d, b: octet)) { Utf8Ready { out: out } => Present { value: out } _ => none } diff --git a/dag/std/machine_word.dag b/dag/std/machine_word.dag new file mode 100644 index 00000000000..f5e31b95dcf --- /dev/null +++ b/dag/std/machine_word.dag @@ -0,0 +1,802 @@ +module std.machine_word + +import std.induction { int_pow_bounded } +import std.roster_frontier { FrontierRow, frontier_row_decl } +import std.decl_ref { decl_ref } +import std.dissolution { unbound_dissolution } +import std.measure { bits_per_byte } +import extdeps.toolchain.architecture_profile { Endianness, BigEndian, LittleEndian } + +// THE FIXED-WIDTH MACHINE WORD, AND WHY IT IS A VALUE-LEVEL WIDTH. +// +// std.integer models the width tower type-level: UInt32 = Compose>, one axis +// rather than ten types. That is the right shape for DECLARING what a value is, and it is not +// sufficient for OPERATING on one: an operation has to reduce modulo the width, and a phantom +// cannot be reduced by. WordWidth is therefore the value-level projection of MachineWidth over +// the widths this substrate realizes, joined to it by word_width_bits, and NOT a second width +// authority -- a width that std.integer cannot spell must not appear here, and one it can spell but +// this substrate cannot realize refuses by name rather than being omitted (Width64 below). +// +// std.bit's Word8..Word128 are a different concept again and are deliberately not reused: they are +// bit-RECORDS (List of List) with no cardinality refinement, consumed as type vocabulary +// by extdeps.languages.rust.primitives and v2.std.machine to NAME a width. They carry no value a +// fold can compute with. Reusing the name for a computational carrier would be a meaning fork. +// +// ENDIANNESS IS NOT DECLARED HERE. extdeps.toolchain.architecture_profile already owns it, and byte +// order is one concept whether it is read off an architecture profile or supplied to a conversion. +// A std module importing extdeps is not a layer inversion: DESIGN section 3 makes acyclicity the +// only structural law of the import graph and the folders browsing conventions. +type WordWidth + = Width8 + | Width16 + | Width32 + | Width64 + +fn word_width_bits(w: WordWidth) -> Int { + match w { + Width8 => 8 + Width16 => 16 + Width32 => 32 + Width64 => 64 + } +} + +// THE CARRIER. The width travels WITH the value rather than beside it in a caller's convention, +// which is what makes a width MISMATCH a fact an operation can refuse on instead of a silent +// reinterpretation. The value field is the residue in [0, 2^bits), and word_of_int is the only +// sanctioned entry that establishes that. RESIDUE, NAMED: the record is directly constructible, so +// a caller can write Word { width: Width32, value: 0 - 1 } and no construction refuses it. That is +// mitigatable, not structural. NEXT-RUNG TRIGGER: sole_constructor over this carrier -- the +// capability that makes word_of_int the only way to inhabit Word -- at which point the range +// invariant holds by construction and word_of_int's range arm becomes unreachable rather than +// merely sanctioned. +type Word { + width: WordWidth + value: Int +} + +type WordRefusal + = WordValueOutOfRange { width: WordWidth, value: Int } + | WordWidthUnrealizable { width: WordWidth } + | WordWidthMismatch { left: WordWidth, right: WordWidth } + | ShiftAmountOutOfRange { width: WordWidth, amount: Int } + | OctetCountMismatch { width: WordWidth, expected: Int, observed: Int } + | OctetWidthMismatch { observed: WordWidth } + | IntegerDoesNotFitOctets { value: Int, octets: Int } + | OctetCountOutOfRange { observed: Int } + +type WordResult + = WordReady { word: Word } + | WordRefused { cause: WordRefusal } + +type OctetsResult + = OctetsReady { octets: List } + | OctetsRefused { cause: WordRefusal } + +type CarryingSum { + sum: Word + carry: Bool +} + +type CarryingSumResult + = CarryingSumReady { result: CarryingSum } + | CarryingSumRefused { cause: WordRefusal } + +// THE ONE PLACE A WIDTH BECOMES A NUMBER, and the one place a width is refused. +// +// 2^64 is not representable in the Int the seed and the emitted Rust realize as i64, so a Width64 +// word has no residue this carrier can hold and EVERY operation on one refuses with +// WordWidthUnrealizable rather than answering with a truncated or wrapped number. That refusal is +// the honest statement of the realization boundary std.checked_arithmetic declares: the model has +// unbounded integers, the realization has i64, and code that computes 64-bit words on an i64 is +// asserting the first about the second. NEXT-RUNG TRIGGER, naming the capability and not an +// artifact: a multi-limb magnitude carrier in this module sufficient for a word whose modulus +// exceeds the Int bound to be REPRESENTED and operated on -- at which point Width64 stops refusing +// and the big-integer substrate P-256/P-384 needs is the same carrier, not a second one. +// +// THE MODULUS IS DERIVED ONCE PER WIDTH, NOT ONCE PER OPERATION, AND THAT IS A CORRECTNESS-GRADE +// FIX RATHER THAN A TUNING ONE. The first cut called int_pow_bounded here, which is a non-tail +// linear recursion with a checked multiply per step, so EVERY operation -- including shifts and +// rotates that are otherwise a division -- paid a walk proportional to its width just to learn a +// constant. WordWidth is a CLOSED four-member coproduct, so the fact being recomputed is one of +// four numbers, and DESIGN section 2 is explicit that when repeated demands share a least common +// ancestor the repetition is authored duplication to be carried rather than made cheap; section 6 +// forecloses the "n is small here" defence outright. Stating the shape in an annotation, which the +// first cut did, is not discharging it. +// +// THE VALUES ARE DERIVED, NOT TRANSCRIBED, AND THE DERIVATION IS CHECKED BY EXECUTION. The reason +// to avoid a literal table is that a second representation of a derived constant can go stale +// silently; that objection is against TRANSCRIBING a value, not against materialising one. So +// std.induction int_pow_bounded remains the authority for what 2^bits IS, and +// word_modulus_agrees_with_the_power_authority_holds runs this function against it for every +// member of the closed set, including Width64 where both must answer with nothing. A wrong number +// here reds that claim; it does not wait to be noticed. +fn word_modulus(w: WordWidth) -> Int? { + match w { + Width8 => Present { value: 256 } + Width16 => Present { value: 65536 } + Width32 => Present { value: 4294967296 } + Width64 => none + } +} + +// THE SPLIT POINT OF A WIDTH, DERIVED ONCE FOR THE SAME REASON THE MODULUS IS. word_wrapping_multiply +// splits its left operand at half the width and walked int_pow_bounded per call to find where. The +// reviewer named word_modulus, but the defect is the CLASS -- a constant over a closed coproduct +// recomputed per demand -- and fixing only the instance that was cited would be repairing the +// symptom rather than the boundary (DESIGN section 6b). Checked against the authority by +// word_half_radix_agrees_with_the_power_authority_holds, exactly as the modulus is. +fn word_half_radix(w: WordWidth) -> Int? { + match w { + Width8 => Present { value: 16 } + Width16 => Present { value: 256 } + Width32 => Present { value: 65536 } + Width64 => none + } +} + +fn word_of_int(width: WordWidth, value: Int) -> WordResult { + match word_modulus(w: width) { + Absent => WordRefused { cause: WordWidthUnrealizable { width: width } } + Present { value: m } => + if value < 0 || value >= m { + WordRefused { cause: WordValueOutOfRange { width: width, value: value } } + } else { + WordReady { word: Word { width: width, value: value } } + } + } +} + +// THE QUALIFICATION IS A CARRIER, NOT A CHECK EACH HELPER REMEMBERS TO REPEAT. +// +// .dag has NO module-private, so every top-level helper is a callable boundary and there is no +// wall to hide one behind. The first repair qualified each PUBLIC operation and left the helpers +// below them taking raw Word -- word_from_octets_realizable was callable directly with Width64 and +// would reconstruct up to 2^64 - 1 in the i64 before word_of_int refused, which is the exact +// overflow-after-compute defect the public wrapper exists to prevent. Splitting that body out and +// naming it "_realizable" asserted a property the language does not enforce: a name is not a proof. +// +// Re-validating inside every helper is the wrong repair -- that is validation multiplied by helper +// count, and it fails the moment someone adds helper N+1 and forgets, which is precisely how the +// projection survived the last pass. So the proof moves into the TYPE. QualifiedWord is produced +// only by word_qualified and word_pair_qualified; RealizableWidth is produced only by +// word_realizable_width, the one function that refuses Width64. Every helper below the public +// boundary takes those carriers and therefore CANNOT be handed an unqualified value -- not because +// a wall stops it, but because the call does not typecheck. +// +// HONEST ABOUT WHAT THIS IS. A record with public fields is still constructible, so this is a +// sealed-wrapper convention rather than a private constructor, and a caller determined to forge +// QualifiedWord { word: ... } can. What it changes is the DEFAULT: the failure mode stops being +// "a helper forgot to qualify" and becomes "someone deliberately forged the proof", which is a +// different and far rarer mistake. Rung unchanged -- mitigatable -- and the next-rung trigger is +// still sole construction, which would make the forgery unwritable and delete word_qualified's +// range arm along with it. +// +// THE WALL ITSELF IS UNWITNESSED, AND THAT IS A GAP RATHER THAN A CEILING. Everything above rests +// on one property: handing a bare Word where a QualifiedWord is declared DOES NOT TYPECHECK. No +// claim in this corpus establishes that. It cannot be established from the accepted corpus -- if +// the bad call were writable there the tree would not compile -- so the evidence has to be fixture +// source compiled through the real acceptance path, which DESIGN section 4b explicitly says is +// available and therefore owed. +// +// I WROTE THAT WITNESS AND WITHDREW IT, which is worth recording precisely because the approving +// review cited it as a strength while it was not executing. test.claim.machine_word_qualification_ +// typecheck compiled three illegal sources plus an acceptance-asserting green control through +// gunbc.compile_diagnostic_census. All four claims FAILED on every run: first uniformly, which the +// 0 - 1 not-runnable sentinel is designed to produce when the harness is dead, and then still +// uniformly after the probe sources' record-literal braces were unescaped to match the corpus +// precedent -- the REDs failing a > 0 assertion and the green failing an == 0 assertion at the same +// time, which no single count explains. The floor's own reach probe reports +// reach=opaque_host_call_unbounded:compile_dag_diagnostic_census, last_builtin=census_total_count, +// ~2.3s of shared fill per claim. Diagnosing further needs a harness that can print the census +// cause, which is another cycle per hypothesis. +// +// Shipping four claims that cannot run would have been worse than none -- they would be cited as +// coverage, which is exactly what happened in review before anyone looked at a run. Weakening them +// until they passed would have been worse still. So the module is withdrawn and the obligation is +// stated here, on the carrier whose property it was meant to establish. +// +// TRIGGER, at capability grain: a census probe in this lane that can report CompileDiagnosticCensus +// CensusNotRunnable's cause string, sufficient to tell a harness that did not run from a source +// that compiled clean. Nothing else retires this; re-adding the same four claims without that +// discrimination reproduces the state being recorded. +type QualifiedWord { + word: Word +} + +type QualifiedWordResult + = QualifiedWordReady { qualified: QualifiedWord } + | QualifiedWordRefused { cause: WordRefusal } + +type RealizableWidth { + width: WordWidth + modulus: Int +} + +type RealizableWidthResult + = RealizableWidthReady { realizable: RealizableWidth } + | RealizableWidthRefused { cause: WordRefusal } + +// The ONE producer of RealizableWidth, and the one place Width64 is refused. A helper holding this +// carrier has the modulus in hand and never asks for it again, so the width refusal cannot be +// skipped by a caller who reached the helper another way. +fn word_realizable_width(w: WordWidth) -> RealizableWidthResult { + match word_modulus(w: w) { + Absent => RealizableWidthRefused { cause: WordWidthUnrealizable { width: w } } + Present { value: m } => RealizableWidthReady { realizable: RealizableWidth { width: w, modulus: m } } + } +} + +fn qualified_word_value(q: QualifiedWord) -> Int { + q.word.value +} + +fn qualified_word_width(q: QualifiedWord) -> WordWidth { + q.word.width +} + +fn qualified_word_unwrap(q: QualifiedWord) -> Word { + q.word +} + +// THE ROUND TRIP NEEDS THIS AND IT IS NOT A HOLE IN THE CARRIER. word_to_octets answers qualified +// members and word_from_octets takes raw ones -- deliberately, because a caller assembling octets +// by hand legitimately has raw Words and the entry qualifies them. Feeding one into the other is +// an ordinary consumer pattern (SHA-2 block packing is exactly this), so the unwrap is exported +// rather than open-coded per caller. It DISCARDS a proof, which is safe in this direction: every +// member is re-qualified by word_from_octets, so the worst case is paying the check twice, not +// skipping it. +fn qualified_words_to_words(octets: List) -> List { + octets |> map(o => qualified_word_unwrap(q: o)) +} + +// The ONE producer of QualifiedWord. word_of_int establishes both facts a helper below here needs: +// the width is realizable and the value inhabits it. +fn word_qualified(w: Word) -> QualifiedWordResult { + match word_of_int(width: w.width, value: w.value) { + WordRefused { cause: c } => QualifiedWordRefused { cause: c } + WordReady { word: x } => QualifiedWordReady { qualified: QualifiedWord { word: x } } + } +} + +type WordPairResult + = WordPairReady { left: QualifiedWord, right: QualifiedWord } + | WordPairRefused { cause: WordRefusal } + +// The width disagreement is decided BEFORE either operand is qualified, because a mismatch is a +// fact about the call and an out-of-range value is a fact about one operand; reporting the operand +// first would answer a narrower question than the one that is wrong. +fn word_pair_qualified(a: Word, b: Word) -> WordPairResult { + if word_width_bits(w: a.width) != word_width_bits(w: b.width) { + WordPairRefused { cause: WordWidthMismatch { left: a.width, right: b.width } } + } else { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordPairRefused { cause: c } + QualifiedWordReady { qualified: qa } => + match word_qualified(w: b) { + QualifiedWordRefused { cause: c } => WordPairRefused { cause: c } + QualifiedWordReady { qualified: qb } => WordPairReady { left: qa, right: qb } + } + } + } +} + +// BITWISE OPERATIONS ARE ONE FOLD, NOT THREE. The three connectives differ only in the two-bit +// decision at each place; the decomposition, the place accumulation and the bound are identical, so +// authoring them separately would be three copies of one loop that can drift apart. The identity +// a + b = (a xor b) + 2 * (a and b) would let two of the three be derived arithmetically from the +// third, which is correct and grounded but reads as a trick: the loop states what the operation IS. +type BitwiseOp + = BitAnd + | BitOr + | BitXor + +fn bitwise_place_bit(op: BitwiseOp, x: Int, y: Int) -> Int { + match op { + BitAnd => if x == 1 && y == 1 { 1 } else { 0 } + BitOr => if x == 1 || y == 1 { 1 } else { 0 } + BitXor => if x == y { 0 } else { 1 } + } +} + +fn bitwise_fold(op: BitwiseOp, a: Int, b: Int, remaining: Int, place: Int, acc: Int) -> Int { + if remaining <= 0 { + acc + } else { + bitwise_fold( + op: op, + a: a / 2, + b: b / 2, + remaining: remaining - 1, + place: place * 2, + acc: acc + (bitwise_place_bit(op: op, x: a % 2, y: b % 2) * place) + ) + } +} + +fn word_bitwise(op: BitwiseOp, a: Word, b: Word) -> WordResult { + match word_pair_qualified(a: a, b: b) { + WordPairRefused { cause: c } => WordRefused { cause: c } + WordPairReady { left: x, right: y } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + word_of_int( + width: r.width, + value: bitwise_fold(op: op, a: qualified_word_value(q: x), b: qualified_word_value(q: y), remaining: word_width_bits(w: r.width), place: 1, acc: 0) + ) + } + } +} + +fn word_and(a: Word, b: Word) -> WordResult { + word_bitwise(op: BitAnd, a: a, b: b) +} + +fn word_or(a: Word, b: Word) -> WordResult { + word_bitwise(op: BitOr, a: a, b: b) +} + +fn word_xor(a: Word, b: Word) -> WordResult { + word_bitwise(op: BitXor, a: a, b: b) +} + +// Complement is the ones-complement within the width, which is the modulus minus one minus the +// value. It needs no bit walk: every place flips, and flipping every place of a residue below 2^w +// is exactly subtracting it from the all-ones value. +fn word_not(a: Word) -> WordResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordRefused { cause: c } + QualifiedWordReady { qualified: x } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + word_of_int(width: r.width, value: r.modulus - 1 - qualified_word_value(q: x)) + } + } +} + +// SHIFTS ARE TOTAL AND BOUNDED. An amount at or above the width is refused rather than answered +// with zero: in C it is undefined behaviour, in Rust it panics, and on x86 it silently masks the +// amount -- three different answers to one question, which is exactly the state a typed refusal +// exists to keep out of the model. Negative amounts are refused rather than reinterpreted as the +// opposite direction, because a shift that changes direction on the sign of its amount is two +// operations wearing one name. +// +// THE REDUCTION HAPPENS BEFORE THE MULTIPLICATION, NOT AFTER. Writing (value * 2^k) % modulus is +// the obvious form and it OVERFLOWS the i64 realization for a 32-bit word shifted left by 31 -- +// the product reaches 2^63 before the modulus is ever applied, so the check would be inspecting +// whatever the realization did about an overflow it had already suffered. Dropping the bits that +// the shift discards FIRST keeps every intermediate inside the width. +fn word_shift_left(a: Word, amount: Int) -> WordResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordRefused { cause: c } + QualifiedWordReady { qualified: x } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + if amount < 0 || amount >= word_width_bits(w: r.width) { + WordRefused { cause: ShiftAmountOutOfRange { width: r.width, amount: amount } } + } else { + match int_pow_bounded(base: 2, exp: amount) { + Absent => WordRefused { cause: WordWidthUnrealizable { width: r.width } } + Present { value: factor } => word_of_int(width: r.width, value: (qualified_word_value(q: x) % (r.modulus / factor)) * factor) + } + } + } + } +} + +fn word_shift_right(a: Word, amount: Int) -> WordResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordRefused { cause: c } + QualifiedWordReady { qualified: x } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + if amount < 0 || amount >= word_width_bits(w: r.width) { + WordRefused { cause: ShiftAmountOutOfRange { width: r.width, amount: amount } } + } else { + match int_pow_bounded(base: 2, exp: amount) { + Absent => WordRefused { cause: WordWidthUnrealizable { width: r.width } } + Present { value: factor } => word_of_int(width: r.width, value: qualified_word_value(q: x) / factor) + } + } + } + } +} + +// A rotation is the two shifts summed, and they are summed rather than OR-ed because the two +// results occupy disjoint places by construction -- no place can be set in both, so addition and +// disjunction agree and addition does not walk the bits. The zero amount is its own arm because +// the complementary shift would then be by the full width, which shifts refuse. +fn word_rotate_left(a: Word, amount: Int) -> WordResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordRefused { cause: c } + QualifiedWordReady { qualified: x } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + if amount < 0 || amount >= word_width_bits(w: r.width) { + WordRefused { cause: ShiftAmountOutOfRange { width: r.width, amount: amount } } + } else { + if amount == 0 { + WordReady { word: qualified_word_unwrap(q: x) } + } else { + match word_shift_left(a: qualified_word_unwrap(q: x), amount: amount) { + WordRefused { cause: c } => WordRefused { cause: c } + WordReady { word: high } => + match word_shift_right(a: qualified_word_unwrap(q: x), amount: word_width_bits(w: r.width) - amount) { + WordRefused { cause: c } => WordRefused { cause: c } + WordReady { word: low } => word_of_int(width: r.width, value: high.value + low.value) + } + } + } + } + } + } +} + +// THE WIDTH IS ESTABLISHED BEFORE THE AMOUNT, which is what the other three shift and rotate arms +// already did and this one did not: a Width64 rotate by 64 reported ShiftAmountOutOfRange, naming +// the amount, when the width itself is the thing that cannot exist. Two operations disagreeing +// about which refusal a caller sees for the same malformed call is a fork in the refusal +// vocabulary, and the narrower answer is the wrong one. +fn word_rotate_right(a: Word, amount: Int) -> WordResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => WordRefused { cause: c } + QualifiedWordReady { qualified: x } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + if amount < 0 || amount >= word_width_bits(w: r.width) { + WordRefused { cause: ShiftAmountOutOfRange { width: r.width, amount: amount } } + } else { + if amount == 0 { + WordReady { word: qualified_word_unwrap(q: x) } + } else { + word_rotate_left(a: qualified_word_unwrap(q: x), amount: word_width_bits(w: r.width) - amount) + } + } + } + } +} + +// WRAPPING IS THE DECLARED OVERFLOW RULE OF THESE OPERATIONS, NOT A REALIZATION ACCIDENT. +// std.integer's IntegerOverflowSemantics names ReturnWrapping as one rule among raising and +// undefined; these functions ARE that rule applied at the declared width, and a caller that wants +// the crossing reported instead uses word_carrying_add, which returns the carry as a value. +fn word_wrapping_add(a: Word, b: Word) -> WordResult { + match word_pair_qualified(a: a, b: b) { + WordPairRefused { cause: c } => WordRefused { cause: c } + WordPairReady { left: x, right: y } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => word_of_int(width: r.width, value: (qualified_word_value(q: x) + qualified_word_value(q: y)) % r.modulus) + } + } +} + +fn word_wrapping_subtract(a: Word, b: Word) -> WordResult { + match word_pair_qualified(a: a, b: b) { + WordPairRefused { cause: c } => WordRefused { cause: c } + WordPairReady { left: x, right: y } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => word_of_int(width: r.width, value: (qualified_word_value(q: x) - qualified_word_value(q: y) + r.modulus) % r.modulus) + } + } +} + +// THE PRODUCT IS SPLIT BECAUSE THE PRODUCT DOES NOT FIT. Two 32-bit residues multiply to 64 bits, +// which the i64 realization cannot hold, so the obvious (a * b) % m is an overflow inspected after +// the fact rather than a check. Splitting the left operand at half the width makes both partial +// products at most bits + bits/2 wide, and reducing the high partial product before scaling it +// keeps the scaled term inside the width. Every width here is even, so the half is exact. +fn word_wrapping_multiply(a: Word, b: Word) -> WordResult { + match word_pair_qualified(a: a, b: b) { + WordPairRefused { cause: c } => WordRefused { cause: c } + WordPairReady { left: x, right: y } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + match word_half_radix(w: r.width) { + Absent => WordRefused { cause: WordWidthUnrealizable { width: r.width } } + Present { value: half } => { + let xv = qualified_word_value(q: x) + let yv = qualified_word_value(q: y) + let low_term = ((xv % half) * yv) % r.modulus + let high_term = (((xv / half) * yv) % half) * half + word_of_int(width: r.width, value: (low_term + high_term) % r.modulus) + } + } + } + } +} + +fn word_carrying_add(a: Word, b: Word) -> CarryingSumResult { + match word_pair_qualified(a: a, b: b) { + WordPairRefused { cause: c } => CarryingSumRefused { cause: c } + WordPairReady { left: x, right: y } => + match word_realizable_width(w: qualified_word_width(q: x)) { + RealizableWidthRefused { cause: c } => CarryingSumRefused { cause: c } + RealizableWidthReady { realizable: r } => { + let total = qualified_word_value(q: x) + qualified_word_value(q: y) + match word_of_int(width: r.width, value: total % r.modulus) { + WordRefused { cause: c } => CarryingSumRefused { cause: c } + WordReady { word: sum } => CarryingSumReady { result: CarryingSum { sum: sum, carry: total >= r.modulus } } + } + } + } + } +} + +// AN OCTET IS A WIDTH-8 WORD, NOT A BARE Int. The whole point of this module is that a width is a +// fact the value carries; handing back List from a conversion would put the width back into a +// caller's convention at exactly the seam -- packing and unpacking -- where getting it wrong is +// invisible. extdeps.network.ipv4's `Octet = Int where range(0, 255)` is a network-layer row and is +// left alone: minting a third spelling of the same concept here would be the nicknaming +// DESIGN section 3 forbids, and reusing a network row as the substrate's byte would be worse. +fn octet_bit_width() -> Int { + bits_per_byte() +} + +// AN OCTET'S RADIX IS THE Width8 MODULUS. It was a separate int_pow_bounded walk, paid by every +// packing and unpacking call, to arrive at a number this module already answers. That is the same +// closed-set recomputation review 68053 named at word_modulus, one function along, and it is fixed +// by REUSE rather than by a second constant: nothing new is introduced here, so nothing new can go +// stale. octet_radix_is_the_width8_modulus_holds is its executing check. +fn octet_radix() -> Int? { + word_modulus(w: Width8) +} + +fn word_octet_count(w: WordWidth) -> Int { + word_width_bits(w: w) / octet_bit_width() +} + +// THIS FUNCTION MAY MINT QualifiedWord BECAUSE IT ESTABLISHES THE FACT ITSELF: value % radix is +// below radix by construction, and radix is the Width8 modulus, so each member inhabits Width8 +// without anything needing to check it afterwards. That is the only admissible reason to construct +// the carrier outside word_qualified -- the proof is discharged here, not assumed. +fn octets_little_endian_accumulate(value: Int, remaining: Int, radix: Int, acc: List) -> List { + if remaining <= 0 { + acc + } else { + octets_little_endian_accumulate( + value: value / radix, + remaining: remaining - 1, + radix: radix, + acc: acc |> list_push(QualifiedWord { word: Word { width: Width8, value: value % radix } }) + ) + } +} + +// AN UNREPRESENTABLE CAPACITY IS NOT A REFUSAL, AND THE DIFFERENCE IS THE WHOLE POINT OF ASKING +// SEPARATELY. A field of eight octets holds up to 2^64 values, which the Int realization cannot +// count to; treating that as "the value does not fit" would refuse every eight-octet length field, +// which is exactly what SHA-2 message padding renders. When the capacity exceeds what an Int can +// represent, every nonnegative Int is BELOW it by construction, so the honest answer is that it +// fits -- an absent capacity here is ignorance about the bound, not an answer about the value, and +// the two are only interchangeable in the direction that happens to be safe. +// AN ABSENT CAPACITY HAS TWO CAUSES AND ONLY ONE OF THEM IS SAFE TO READ AS "IT FITS". The +// annotation below already said an absent capacity is ignorance about the bound rather than an +// answer about the value -- and this function then treated EVERY absent capacity as "does not +// exceed". int_pow_bounded answers Absent both when the power overflows the Int bound (where every +// representable value genuinely is below it) and when the EXPONENT IS NEGATIVE, which is not a +// statement about capacity at all. So count = -1 fell through to an accumulator that stops at +// remaining <= 0 and returned OctetsReady [] -- a successful empty rendering of a nonsense request, +// which is the fabricated plausible output DESIGN section 5 forbids, produced by the exact +// conflation the neighbouring annotation warned about. The count is now decided on its own terms +// BEFORE the capacity is asked, so the remaining Absent has only the one meaning the reading +// assumes. +fn int_exceeds_octet_capacity(value: Int, count: Int, radix: Int) -> Bool { + match int_pow_bounded(base: radix, exp: count) { + Absent => false + Present { value: capacity } => value >= capacity + } +} + +// THE ACCUMULATOR APPENDS AND THE BIG-ENDIAN ORDER IS A REVERSE, rather than the natural-reading +// form that prepends each octet onto the front of the accumulator. list_push extends its LEFT +// operand, so appending clones one element per step while prepending clones the whole accumulated +// list per step -- the quadratic shape std.nat nat_range_accumulate records at the same grain. +fn int_to_octets(value: Int, count: Int, endianness: Endianness) -> OctetsResult { + match octet_radix() { + Absent => OctetsRefused { cause: WordWidthUnrealizable { width: Width8 } } + Present { value: radix } => + if count < 0 { + OctetsRefused { cause: OctetCountOutOfRange { observed: count } } + } else if value < 0 || int_exceeds_octet_capacity(value: value, count: count, radix: radix) { + OctetsRefused { cause: IntegerDoesNotFitOctets { value: value, octets: count } } + } else { + let little = octets_little_endian_accumulate(value: value, remaining: count, radix: radix, acc: []) + match endianness { + LittleEndian => OctetsReady { octets: little } + BigEndian => OctetsReady { octets: reverse(little) } + } + } + } +} + +fn word_to_octets(a: Word, endianness: Endianness) -> OctetsResult { + match word_qualified(w: a) { + QualifiedWordRefused { cause: c } => OctetsRefused { cause: c } + QualifiedWordReady { qualified: x } => + int_to_octets(value: qualified_word_value(q: x), count: word_octet_count(w: qualified_word_width(q: x)), endianness: endianness) + } +} + +fn octets_big_endian_value(octets: List, radix: Int, acc: Int) -> Int { + match octets.first() { + Absent => acc + Present { value: head } => + octets_big_endian_value(octets: octets.skip(n: 1), radix: radix, acc: acc * radix + qualified_word_value(q: head)) + } +} + +// THE MEMBERS ARE QUALIFIED AND THE RESULT CARRIES THE PROOF. The first cut checked each member's +// WIDTH and trusted its VALUE, so word_from_octets(Width16, [1, 256]) packed to 512 -- an answer +// assembled from an octet that cannot exist, in range for the target width, so nothing downstream +// fired. Width agreement is not inhabitance. This now returns the QUALIFIED members rather than a +// yes/no, so the caller carries the established octets forward instead of re-reading the raw list. +type QualifiedOctetsResult + = QualifiedOctetsReady { octets: List } + | QualifiedOctetsRefused { cause: WordRefusal } + +fn octets_qualified(octets: List, remaining: List) -> QualifiedOctetsResult { + match remaining.first() { + Absent => QualifiedOctetsReady { octets: octets } + Present { value: head } => + if word_width_bits(w: head.width) != octet_bit_width() { + QualifiedOctetsRefused { cause: OctetWidthMismatch { observed: head.width } } + } else { + match word_qualified(w: head) { + QualifiedWordRefused { cause: c } => QualifiedOctetsRefused { cause: c } + QualifiedWordReady { qualified: q } => + octets_qualified(octets: octets |> list_push(q), remaining: remaining.skip(n: 1)) + } + } + } +} + +// The count check is EXACT, not a lower bound. A packing that accepted more octets than the width +// holds would silently drop the excess, and one that accepted fewer would silently zero-extend -- +// two different fabricated answers to the same malformed input. The per-octet width check is what +// makes the List argument mean what its type says: a caller can still build a Word record +// directly, so the shape is checked at the boundary that consumes it. +// THE WIDTH IS ESTABLISHED BEFORE ANY OCTET IS ACCUMULATED, AND THE HELPER CANNOT BE REACHED +// WITHOUT IT. +// +// This was the one exported operation that did arithmetic before guarding on its own width: it +// guarded on octet_radix, which asks about Width8 and therefore always answers, so a Width64 call +// passed the count and per-octet checks and then accumulated eight octets to as much as 2^64 - 1 +// in the Int the seed realizes as i64, with word_of_int refusing only afterwards -- a refusal +// inspecting a number the realization had already wrapped on. +// +// The first repair put the guard in the public wrapper and split the body into a helper named +// "_realizable". That name asserted a property nothing enforced: .dag has no module-private, so the +// helper was itself a callable boundary and `word_from_octets_realizable(Width64, ...)` walked +// straight back into the overflow. The helper now takes RealizableWidth and List, +// so reaching it without both proofs does not typecheck. +fn word_from_octets_realizable(width: RealizableWidth, octets: List, endianness: Endianness) -> WordResult { + let expected = word_octet_count(w: width.width) + let observed = list_length(items: octets) + if observed != expected { + WordRefused { cause: OctetCountMismatch { width: width.width, expected: expected, observed: observed } } + } else { + match octet_radix() { + Absent => WordRefused { cause: WordWidthUnrealizable { width: Width8 } } + Present { value: radix } => { + let ordered = match endianness { + BigEndian => octets + LittleEndian => reverse(octets) + } + word_of_int(width: width.width, value: octets_big_endian_value(octets: ordered, radix: radix, acc: 0)) + } + } + } +} + +// The public entry takes what a caller actually has -- a plain WordWidth and plain Words -- and +// establishes both proofs ONCE before handing the carriers down. This is the only place the two +// qualifications happen for this route, which is what makes the helper's signature a wall rather +// than a second checkpoint. +fn word_from_octets(width: WordWidth, octets: List, endianness: Endianness) -> WordResult { + match word_realizable_width(w: width) { + RealizableWidthRefused { cause: c } => WordRefused { cause: c } + RealizableWidthReady { realizable: r } => + match octets_qualified(octets: [], remaining: octets) { + QualifiedOctetsRefused { cause: c } => WordRefused { cause: c } + QualifiedOctetsReady { octets: qualified } => + word_from_octets_realizable(width: r, octets: qualified, endianness: endianness) + } + } +} + +// THE PROJECTION TAKES THE CARRIER, SO THE REFUSAL ARM IT NEEDED IS GONE. +// +// octet_int_values mapped o.value over raw members with no qualification and no refusal arm, on the +// base64 decode production route. The first repair gave it a typed refusal and re-checked its +// members -- which is validation multiplied by helper count, the shape this carrier exists to +// replace. Taking List makes the bad call fail to typecheck, so there is nothing +// left to refuse: the result is a plain List again, and it is honest this time because every +// member arrived with its proof attached rather than being re-inspected here. +fn octet_int_values(octets: List) -> List { + octets |> map(o => qualified_word_value(q: o)) +} + +// THE DECLARATIONS THIS MODULE LANDS AHEAD OF THEIR CONSUMERS, AS ROWS RATHER THAN AS PROSE. +// +// DESIGN section 3c admits exactly three states for a new declaration: consumed by execution here, +// consumed by a named later change with the trigger stated beside it, or dangling -- and only the +// third is red. The operations below are the second state, and the first cut of this module put +// that claim in a `//` block naming SHA-256 and P-256. Section 4c rules that an annotation is never +// evidence a machine claim holds, because no Accepted program can read one, so a frontier stated in +// prose is indistinguishable from a dangling declaration to everything except a human reader who +// happens to look. +// +// DECLARING THE ROWS IS HALF OF IT; BEING FOLDED IS THE OTHER HALF, AND THE FIRST CUT OF THIS +// ROSTER HAD ONLY THE FIRST. It asserted in prose that gunbc.dissolution_census reads these rows +// while the census folded one roster this was not a member of, so the expiry of every row below +// was computed by nothing -- an inert lens, and the same 4c violation this roster exists to +// correct, committed in the sentence claiming to correct it (review 68088). Membership is +// gunbc.census_closure_frontier census_closure_frontier_row_groups, which this roster is now +// enrolled in; that enrolment, not this annotation, is what makes the expiry a computed fact. +// +// EVERY ROW IS UNBOUND, AND THE REASON IS A GATE, NOT A PREFERENCE. std.dissolution +// bound_dissolution takes a DeclarationRef, and a DeclarationRef is a CITATION: the required +// declarations phase resolves it against THE TREE IT RUNS IN and refuses CITED-MODULE-ABSENT when +// the module is not there. extdeps.crypto.sha2 exists on gunbc#11647 and nowhere else, so binding +// these four rows to its symbols refused the whole parse phase -- "the symbol exists on a branch" +// is not a fact this tree can check, and seeing it on a branch is exactly what made the citation +// look safe. DeclarationAppears is still the right shape for a forward reference to a declaration +// in a module that ALREADY EXISTS; it is the absent MODULE that cannot be cited. The consuming +// symbols are named in prose in each description instead, where they are a reader's pointer rather +// than a resolvable reference this tree would have to honour. Where the consuming change is named but +// has authored no declaration to point at, the row is unbound and says so -- a forward reference to +// a name nobody has written would be a citation that can never resolve, which is worse than an +// honest description (DESIGN section 3: cite the symbol, not the position, and do not cite what +// does not exist). +// +// WHAT IS NOT HERE IS AS DELIBERATE AS WHAT IS. word_rotate_left carries no row because +// word_rotate_right consumes it inside this module -- it is executed, not awaited. word_zero and +// word_equal were DELETED rather than given rows: no change named either one, and section 3c's +// remedy for a declaration with no consumer at all is to remove it, not to describe it. They cost +// one line each to reintroduce beside the first caller that wants them. +data machine_word_consumer_frontier_rows: List = [ + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_wrapping_add"), + reason: "SHA-256 T1/T2, the message schedule and the feed-forward are additions modulo 2^32; the consumer is extdeps.crypto.sha2 sha256_add_all on gunbc#11647, ~1,000 calls per compression block.", + dissolution: unbound_dissolution(description: "dissolve-on: extdeps.crypto.sha2 sha256_add_all (gunbc#11647) calls this operation. UNBOUND rather than a DeclarationAppears citation because extdeps.crypto.sha2 does not exist in THIS tree -- the citation gate resolves against the tree it runs in, not against any branch, and a DeclarationRef to an absent module is refused as CITED-MODULE-ABSENT.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_rotate_right"), + reason: "SHA-256 Sigma0/Sigma1 rotate three times each and sigma0/sigma1 twice each; the consumer is extdeps.crypto.sha2 sha256_sigma on gunbc#11647, the one fold all four go through.", + dissolution: unbound_dissolution(description: "dissolve-on: extdeps.crypto.sha2 sha256_sigma (gunbc#11647) calls this operation. UNBOUND rather than a DeclarationAppears citation because extdeps.crypto.sha2 does not exist in THIS tree -- the citation gate resolves against the tree it runs in, not against any branch, and a DeclarationRef to an absent module is refused as CITED-MODULE-ABSENT.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_xor"), + reason: "Every SHA-256 Sigma/sigma term and the Ch/Maj mixing are exclusive-or; the consumer is extdeps.crypto.sha2 sha256_xor3 on gunbc#11647.", + dissolution: unbound_dissolution(description: "dissolve-on: extdeps.crypto.sha2 sha256_xor3 (gunbc#11647) calls this operation. UNBOUND rather than a DeclarationAppears citation because extdeps.crypto.sha2 does not exist in THIS tree -- the citation gate resolves against the tree it runs in, not against any branch, and a DeclarationRef to an absent module is refused as CITED-MODULE-ABSENT.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_not"), + reason: "SHA-256 Ch complements its selector word; the consumer is extdeps.crypto.sha2 sha256_ch on gunbc#11647, the only consumer of complement in that algorithm.", + dissolution: unbound_dissolution(description: "dissolve-on: extdeps.crypto.sha2 sha256_ch (gunbc#11647) calls this operation. UNBOUND rather than a DeclarationAppears citation because extdeps.crypto.sha2 does not exist in THIS tree -- the citation gate resolves against the tree it runs in, not against any branch, and a DeclarationRef to an absent module is refused as CITED-MODULE-ABSENT.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_wrapping_multiply"), + reason: "The FNV-1a kernel CONTENT-HASH-0 (gunbc#11637) models is a wrapping multiply against a prime, which is why the split-product form exists here at all. It is UNBOUND rather than bound to a symbol because that lane has authored no declaration to cite, and because FNV runs at Width64, which this substrate refuses until the multi-limb carrier lands -- so this row is retired by the FNV kernel consuming this function, not by the carrier alone.", + dissolution: unbound_dissolution(description: "dissolve-on: the FNV-1a kernel in CONTENT-HASH-0 (gunbc#11637) calls word_wrapping_multiply. Not discharged by the multi-limb carrier landing, which is a precondition rather than the consumer.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_wrapping_subtract"), + reason: "Multi-limb subtraction borrows, which is this operation at limb width. UNBOUND: the limb carrier is this module's own next cut and has authored no declaration to cite.", + dissolution: unbound_dissolution(description: "dissolve-on: the multi-limb magnitude carrier in std.machine_word calls word_wrapping_subtract for limb borrow. If that carrier lands without consuming it, this declaration is deleted rather than re-described.") + ), + frontier_row_decl( + ref: decl_ref(module_path: "std.machine_word", decl_name: "word_carrying_add"), + reason: "Multi-limb addition propagates carry between limbs, which is what makes the carry an answer rather than a discarded overflow; CarryingSum and CarryingSumResult exist only to give it one. UNBOUND for the same reason as the borrow.", + dissolution: unbound_dissolution(description: "dissolve-on: the multi-limb magnitude carrier in std.machine_word calls word_carrying_add to propagate carry between limbs. If that carrier lands without consuming it, this declaration and CarryingSum/CarryingSumResult are deleted rather than re-described.") + ), +] diff --git a/dag/std/octet_span.dag b/dag/std/octet_span.dag new file mode 100644 index 00000000000..26541ef1e7c --- /dev/null +++ b/dag/std/octet_span.dag @@ -0,0 +1,167 @@ +module std.octet_span + +import std.integer { UInt8 } +import std.machine_word { + Word, WordWidth, Width8, Width16, Width32, WordResult, WordReady, WordRefused, + word_of_int, word_from_octets, word_shift_right, word_and, +} +import extdeps.toolchain.architecture_profile { BigEndian } + +// THE ONE BYTE-OFFSET AUTHORITY FOR OCTET PARSERS (gunbc#11629). +// +// Every binary parser in the encoding program -- CBOR, DER, X.509, App Attest authenticator data -- +// reads one input List and names the part it read by a half-open [start, end) span over that +// SAME input. A parser never carries a copied sub-list plus a private offset convention, because two +// conventions for "where is this field" is the positional fork the brief forbids: a refusal must be +// located in the caller's input, and a later consumer must be able to re-read a field's exact bytes +// (a certificate's signed TBS bytes, an attestation's authData) without re-deriving where it was. +// +// Truncation is the only way a read can fail here, and it is refused by name with the offset, the +// octets needed and the octets present. Interpreting octets as integers or bit fields is not done +// here with arithmetic: it goes through std.machine_word, which owns width and bit operations +// (NUMERIC-BIT-0, gunbc#11627), so no parser open-codes a shift or a mask. + +type OctetSpan { + start: Int + end: Int +} + +type OctetReadRefusal + = OctetInputTruncated { at: Int, needed: Int, available: Int } + | OctetUnsignedTooWide { at: Int, octets: Int } + | OctetWordRefused { at: Int } + +type OctetUnsignedRead + = OctetUnsignedReady { value: Int, end: Int } + | OctetUnsignedRefused { cause: OctetReadRefusal } + +type OctetSpanRead + = OctetSpanReady { span: OctetSpan } + | OctetSpanRefused { cause: OctetReadRefusal } + +fn octet_span_length(span: OctetSpan) -> Int { + span.end - span.start +} + +fn octet_span_octets(input: List, span: OctetSpan) -> List { + input.skip(n: span.start).take(n: span.end - span.start) +} + +fn octet_span_equals(input: List, a: OctetSpan, b: OctetSpan) -> Bool { + octet_span_length(span: a) == octet_span_length(span: b) + && octet_span_octets(input: input, span: a) == octet_span_octets(input: input, span: b) +} + +fn octet_span_is(input: List, span: OctetSpan, expected: List) -> Bool { + octet_span_octets(input: input, span: span) == expected +} + +// A span of `length` octets starting at `at`, refused when the input does not hold that many. +fn octet_span_read(input: List, at: Int, length: Int) -> OctetSpanRead { + let available = count(input) - at + if at < 0 || length < 0 || available < length { + OctetSpanRefused { cause: OctetInputTruncated { at: at, needed: length, available: available } } + } else { + OctetSpanReady { span: OctetSpan { start: at, end: at + length } } + } +} + +fn octet_at(input: List, at: Int) -> UInt8? { + if at < 0 { none } else { input |> get(at) } +} + +// THE READ A PARSER USES INSIDE A FIELD. octet_at knows only the input, so a reader that indexes +// into an element's content with it silently reads the NEXT element when the content is shorter +// than it assumed -- an empty BIT STRING's missing unused-bits octet, or an empty KeyUsage's +// missing first octet, became whatever byte followed (review 68531). This read is bounded by the +// span it is reading, and an offset outside that span is absent rather than a neighbour's byte. +fn octet_in_span(input: List, span: OctetSpan, at: Int) -> UInt8? { + if at < span.start || at >= span.end { none } else { octet_at(input: input, at: at) } +} + +fn octet_word(octet: UInt8) -> WordResult { + word_of_int(width: Width8, value: octet + 0) +} + +// The octet's bits [shift, shift + width) as a small unsigned value: a right shift then a mask, both +// performed by std.machine_word at width 8. +fn octet_bit_field(octet: UInt8, shift: Int, mask: Int) -> Int? { + match octet_word(octet: octet) { + WordRefused { cause: _ } => none + WordReady { word: w } => + match word_shift_right(a: w, amount: shift) { + WordRefused { cause: _ } => none + WordReady { word: shifted } => + match word_of_int(width: Width8, value: mask) { + WordRefused { cause: _ } => none + WordReady { word: m } => + match word_and(a: shifted, b: m) { + WordRefused { cause: _ } => none + WordReady { word: field } => Present { value: field.value } + } + } + } + } +} + +fn octet_bit_is_set(octet: UInt8, bit: Int) -> Bool { + match octet_bit_field(octet: octet, shift: bit, mask: 1) { + Present { value: v } => v == 1 + Absent => false + } +} + +// The word width that holds `count` octets, when std.machine_word realizes one. Three octets are +// read as a 32-bit word behind one leading zero octet, the same packing std.encoding base64 uses. +fn octet_unsigned_width(octets: Int) -> WordWidth? { + if octets == 1 { + Present { value: Width8 } + } else if octets == 2 { + Present { value: Width16 } + } else if octets == 3 || octets == 4 { + Present { value: Width32 } + } else { + none + } +} + +fn octet_words(octets: List) -> List? { + fold(octets, init: Present { value: [] }, f: (acc, octet) => + match acc { + Absent => none + Present { value: words } => + match octet_word(octet: octet) { + WordRefused { cause: _ } => none + WordReady { word: w } => Present { value: words |> list_push(w) } + } + }) +} + +data octet_zero_pad: List = [0] + +data octet_no_pad: List = [] + +fn octet_zero_padding(octets: Int) -> List { + if octets == 3 { octet_zero_pad } else { octet_no_pad } +} + +// `octets` octets at `at`, big-endian, as an unsigned integer. Widths std.machine_word does not +// realize refuse by name rather than being computed some other way. +fn octet_read_unsigned_be(input: List, at: Int, octets: Int) -> OctetUnsignedRead { + match octet_span_read(input: input, at: at, length: octets) { + OctetSpanRefused { cause: c } => OctetUnsignedRefused { cause: c } + OctetSpanReady { span: span } => + match octet_unsigned_width(octets: octets) { + Absent => OctetUnsignedRefused { cause: OctetUnsignedTooWide { at: at, octets: octets } } + Present { value: width } => + match octet_words(octets: append(octet_zero_padding(octets: octets), items: octet_span_octets(input: input, span: span))) { + Absent => OctetUnsignedRefused { cause: OctetWordRefused { at: at } } + Present { value: words } => + match word_from_octets(width: width, octets: words, endianness: BigEndian) { + WordRefused { cause: _ } => OctetUnsignedRefused { cause: OctetWordRefused { at: at } } + WordReady { word: w } => OctetUnsignedReady { value: w.value, end: span.end } + } + } + } + } +} diff --git a/dag/test/claim/app_attest_parse_witness_test.dag b/dag/test/claim/app_attest_parse_witness_test.dag new file mode 100644 index 00000000000..642fe829625 --- /dev/null +++ b/dag/test/claim/app_attest_parse_witness_test.dag @@ -0,0 +1,317 @@ +module test.claim.app_attest_parse_witness_test + +import std.logic { Bool } +import std.types { String, NonEmptyStr, Timestamp, Int, List } +import std.integer { UInt8 } +import std.encoding { base64_decode, base64_encode, Standard } +import std.octet_span { OctetSpan, octet_span_octets } +import extdeps.ietf.cbor { CborTrailingInput, CborDuplicateMapKey } +import extdeps.itu.der { DerTrailingInput } +import extdeps.ietf.x509 { + X509Read, X509Ready, X509Refused, X509Malformed, X509Expired, X509NotYetValid, + x509_certificate, +} +import extdeps.apple.app_attest { + AttestKeyId, AppAttestDevelopment, AppAttestProduction, + AttestationVerification, AttestationVerified, AttestationRefused, + AttestationMalformed, AttestationChainUntrusted, AttestationEnvironmentUnexpected, AttestationCredentialIdMismatch, + AttestationValidationCategoryAbsent, AttestationVerificationUnrealized, AttestationFormatUnexpected, + AssertionVerification, AssertionRefused, AssertionMalformed, AssertionVerificationUnrealized, + AppAttestCborRefused, AppAttestUnknownField, AppAttestBase64Invalid, + AppAttestEcdsaSignatureVerification, AppAttestSha256Digest, + LaunchExtensionsRequired, LaunchExtensionsOptional, AppAttestLaunchExtensionPolicy, + AppAttestAttestationReady, AppAttestAttestationRefused, AppAttestEnvironment, + app_attest_attestation_object, app_attest_verify, app_attest_verify_assertion, app_attest_environment_of, + AppAttestAssertionReady, AppAttestAssertionRefused, app_attest_assertion_object, +} +import extdeps.crypto.signature { VerifyingKey, EcdsaP256Sha256, Sec1Uncompressed } +import gunbc.auth.approval_device_redemption { + EnrolmentChallenge, EnrolmentSlotStanding, EnrolmentCodeUnspent, + EnrolmentAdmitted, EnrolmentRefused, EnrolmentAttestationRefused, EnrolmentObservationTimeUnreadable, + ios_enrolment_admission, +} +import gunbc.auth.approval_decision_store { approval_operator_login } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// THE ORACLE IS A GENUINE DEVICE OBJECT, NOT THIS DECODER'S OWN OUTPUT. The attestation and +// assertion below were produced by DCAppAttestService on an iPhone (iOS 14.4, development +// environment, 2021-01-23) and are published under Apache-2.0 by github.com/veehaitch/devicecheck-appattest +// (src/test/resources/ios-14.4.yaml); they are carried here byte for byte from gunbc#11592's +// app_attest_witness_test (swift-ibex-621), whose chain verifies to the pinned Apple root under +// `openssl verify -attime 1611404013`. The expected field values were read independently of this +// decoder (openssl x509 -text and a direct byte read): leaf valid 2021-01-22T12:13:35Z to +// 2021-01-25T12:13:35Z, CA 1 with basicConstraints CA:TRUE pathlen:0, only basicConstraints and +// keyUsage critical, authenticator-data flags 0x40, counter 0, AAGUID "appattestdevelop", +// credential id equal to the decoded key id. +// +// The adversarial controls mutate THESE bytes, so each refusal is the genuine object failing one +// property. They are also the route's bypass discriminator: a hand-written offset walk over the +// same bytes reads the same authData and certificates, and would not refuse a duplicate key, an +// unknown key, trailing CBOR, or a certificate with trailing bytes. +data genuine_attestation: NonEmptyStr = "o2NmbXRvYXBwbGUtYXBwYXR0ZXN0Z2F0dFN0bXSiY3g1Y4JZAvkwggL1MIICe6ADAgECAgYBdy8p90gwCgYIKoZIzj0EAwIwTzEjMCEGA1UEAwwaQXBwbGUgQXBwIEF0dGVzdGF0aW9uIENBIDExEzARBgNVBAoMCkFwcGxlIEluYy4xEzARBgNVBAgMCkNhbGlmb3JuaWEwHhcNMjEwMTIyMTIxMzM1WhcNMjEwMTI1MTIxMzM1WjCBkTFJMEcGA1UEAwxANjI2NmM5M2I4Yzc5OWM0MWQ0YmU3NzI5ZjczNzU2Yjk1NjYzMzQxMTBjODA5OWY3NzFkNDkzYTAwNWQwN2I3MzEaMBgGA1UECwwRQUFBIENlcnRpZmljYXRpb24xEzARBgNVBAoMCkFwcGxlIEluYy4xEzARBgNVBAgMCkNhbGlmb3JuaWEwWTATBgcqhkjOPQIBBggqhkjOPQMBBwNCAASIwDShkKp9vFoGFQHGVCgDlCWCGYs/HMVGc8o7mtILQVKCZ6VPX9ugRp+vtGu2mQo5a/BPlKSdQyDIHHqyQKOYo4H/MIH8MAwGA1UdEwEB/wQCMAAwDgYDVR0PAQH/BAQDAgTwMIGLBgkqhkiG92NkCAUEfjB8pAMCAQq/iTADAgEBv4kxAwIBAL+JMgMCAQC/iTMDAgEBv4k0MwQxNk1VUkw4VEE1Ny5kZS52aW5jZW50LWhhdXBlcnQuYXBwbGUtYXBwYXR0ZXN0LXBvY6UGBAQgc2tzv4k2AwIBBb+JNwMCAQC/iTkDAgEAv4k6AwIBADAZBgkqhkiG92NkCAcEDDAKv4p4BgQEMTQuNDAzBgkqhkiG92NkCAIEJjAkoSIEIJiaPSUYoXwlnO9VFNRc5s3SNR9j2KApAZckQkeewkQ+MAoGCCqGSM49BAMCA2gAMGUCMGgTpXoTOAhh7XJ4V/W7dVrodoibZVQLQ2+z4d3D0cTnlqYe7se50V/rBM5FSBEMwAIxAN04wxPlelL+QyuFR3qk8ZZ4CsZTHFyzSlE8a0Kd4zvYnS8+taIoED9GwrUi96TmgFkCRzCCAkMwggHIoAMCAQICEAm6xeG8QBrZ1FOVvDgaCFQwCgYIKoZIzj0EAwMwUjEmMCQGA1UEAwwdQXBwbGUgQXBwIEF0dGVzdGF0aW9uIFJvb3QgQ0ExEzARBgNVBAoMCkFwcGxlIEluYy4xEzARBgNVBAgMCkNhbGlmb3JuaWEwHhcNMjAwMzE4MTgzOTU1WhcNMzAwMzEzMDAwMDAwWjBPMSMwIQYDVQQDDBpBcHBsZSBBcHAgQXR0ZXN0YXRpb24gQ0EgMTETMBEGA1UECgwKQXBwbGUgSW5jLjETMBEGA1UECAwKQ2FsaWZvcm5pYTB2MBAGByqGSM49AgEGBSuBBAAiA2IABK5bN6B3TXmyNY9A59HyJibxwl/vF4At6rOCalmHT/jSrRUleJqiZgQZEki2PLlnBp6Y02O9XjcPv6COMp6Ac6mF53Ruo1mi9m8p2zKvRV4hFljVZ6+eJn6yYU3CGmbOmaNmMGQwEgYDVR0TAQH/BAgwBgEB/wIBADAfBgNVHSMEGDAWgBSskRBTM72+aEH/pwyp5frq5eWKoTAdBgNVHQ4EFgQUPuNdHAQZqcm0MfiEdNbh4Vdy45swDgYDVR0PAQH/BAQDAgEGMAoGCCqGSM49BAMDA2kAMGYCMQC7voiNc40FAs+8/WZtCVdQNbzWhyw/hDBJJint0fkU6HmZHJrota7406hUM/e2DQYCMQCrOO3QzIHtAKRSw7pE+ZNjZVP+zCl/LrTfn16+WkrKtplcS4IN+QQ4b3gHu1iUObdncmVjZWlwdFkOdzCABgkqhkiG9w0BBwKggDCAAgEBMQ8wDQYJYIZIAWUDBAIBBQAwgAYJKoZIhvcNAQcBoIAkgASCA+gxggQzMDkCAQICAQEEMTZNVVJMOFRBNTcuZGUudmluY2VudC1oYXVwZXJ0LmFwcGxlLWFwcGF0dGVzdC1wb2MwggMDAgEDAgEBBIIC+TCCAvUwggJ7oAMCAQICBgF3Lyn3SDAKBggqhkjOPQQDAjBPMSMwIQYDVQQDDBpBcHBsZSBBcHAgQXR0ZXN0YXRpb24gQ0EgMTETMBEGA1UECgwKQXBwbGUgSW5jLjETMBEGA1UECAwKQ2FsaWZvcm5pYTAeFw0yMTAxMjIxMjEzMzVaFw0yMTAxMjUxMjEzMzVaMIGRMUkwRwYDVQQDDEA2MjY2YzkzYjhjNzk5YzQxZDRiZTc3MjlmNzM3NTZiOTU2NjMzNDExMGM4MDk5Zjc3MWQ0OTNhMDA1ZDA3YjczMRowGAYDVQQLDBFBQUEgQ2VydGlmaWNhdGlvbjETMBEGA1UECgwKQXBwbGUgSW5jLjETMBEGA1UECAwKQ2FsaWZvcm5pYTBZMBMGByqGSM49AgEGCCqGSM49AwEHA0IABIjANKGQqn28WgYVAcZUKAOUJYIZiz8cxUZzyjua0gtBUoJnpU9f26BGn6+0a7aZCjlr8E+UpJ1DIMgcerJAo5ijgf8wgfwwDAYDVR0TAQH/BAIwADAOBgNVHQ8BAf8EBAMCBPAwgYsGCSqGSIb3Y2QIBQR+MHykAwIBCr+JMAMCAQG/iTEDAgEAv4kyAwIBAL+JMwMCAQG/iTQzBDE2TVVSTDhUQTU3LmRlLnZpbmNlbnQtaGF1cGVydC5hcHBsZS1hcHBhdHRlc3QtcG9jpQYEBCBza3O/iTYDAgEFv4k3AwIBAL+JOQMCAQC/iToDAgEAMBkGCSqGSIb3Y2QIBwQMMAq/ingGBAQxNC40MDMGCSqGSIb3Y2QIAgQmMCShIgQgmJo9JRihfCWc71UU1FzmzdI1H2PYoCkBlyRCR57CRD4wCgYIKoZIzj0EAwIDaAAwZQIwaBOlehM4CGHtcnhX9bt1Wuh2iJtlVAtDb7Ph3cPRxOeWph7ux7nRX+sEzkVIEQzAAjEA3TjDE+V6Uv5DK4VHeqTxlngKxlMcXLNKUTxrQp3jO9idLz61oigQP0bCtSL3pOaAMCgCAQQCAQEEIIvmXMpRWtCXyVOWfRjWNdht14oULtPQd1Jr7RHGvsZ7MGACAQUCAQEEWGFQNVM5VWZ5MDkyY0tsYVJZa2t1VHZRQVR4L1IzQjlTd3FIcjZLNkZYYUFXc3pyVCsyeGtBZ0tNRWZsMjZQWFpwblZZYVl6M3JKaTNkSUFxRVpldWJRPT0wDgIBBgIBAQQGQVRURVNUMA8CAQcCBE8BAQQHc2FuZGJveDAgAgEMAgEBBBgyMDIxLTAxLTIzVDEyOjEzOjM1LjgwMVowIAIBFQIBAQQYMjAyMS0wNC0yM1QxMjoxMzozNS44MDFaAAAAAAAAoIAwggOtMIIDVKADAgECAhBZM1at5VmCz0RCN6zfRRtTMAoGCCqGSM49BAMCMHwxMDAuBgNVBAMMJ0FwcGxlIEFwcGxpY2F0aW9uIEludGVncmF0aW9uIENBIDUgLSBHMTEmMCQGA1UECwwdQXBwbGUgQ2VydGlmaWNhdGlvbiBBdXRob3JpdHkxEzARBgNVBAoMCkFwcGxlIEluYy4xCzAJBgNVBAYTAlVTMB4XDTIwMDUxOTE3NDczMVoXDTIxMDYxODE3NDczMVowWjE2MDQGA1UEAwwtQXBwbGljYXRpb24gQXR0ZXN0YXRpb24gRnJhdWQgUmVjZWlwdCBTaWduaW5nMRMwEQYDVQQKDApBcHBsZSBJbmMuMQswCQYDVQQGEwJVUzBZMBMGByqGSM49AgEGCCqGSM49AwEHA0IABH/pFTRsw4p7mDyT0dBDX9ir2lZwBNMsWIZlUZV6tHj3yyr4ukX3+njqxixJ5PnNwIS1AxTxAjPam3b6RCoruHKjggHYMIIB1DAMBgNVHRMBAf8EAjAAMB8GA1UdIwQYMBaAFNkX/ktnkDhLkvTbztVXgBQLjz3JMEMGCCsGAQUFBwEBBDcwNTAzBggrBgEFBQcwAYYnaHR0cDovL29jc3AuYXBwbGUuY29tL29jc3AwMy1hYWljYTVnMTAxMIIBHAYDVR0gBIIBEzCCAQ8wggELBgkqhkiG92NkBQEwgf0wgcMGCCsGAQUFBwICMIG2DIGzUmVsaWFuY2Ugb24gdGhpcyBjZXJ0aWZpY2F0ZSBieSBhbnkgcGFydHkgYXNzdW1lcyBhY2NlcHRhbmNlIG9mIHRoZSB0aGVuIGFwcGxpY2FibGUgc3RhbmRhcmQgdGVybXMgYW5kIGNvbmRpdGlvbnMgb2YgdXNlLCBjZXJ0aWZpY2F0ZSBwb2xpY3kgYW5kIGNlcnRpZmljYXRpb24gcHJhY3RpY2Ugc3RhdGVtZW50cy4wNQYIKwYBBQUHAgEWKWh0dHA6Ly93d3cuYXBwbGUuY29tL2NlcnRpZmljYXRlYXV0aG9yaXR5MB0GA1UdDgQWBBRpHscPR+zjjd11N0Tz6eFabBBWJTAOBgNVHQ8BAf8EBAMCB4AwDwYJKoZIhvdjZAwPBAIFADAKBggqhkjOPQQDAgNHADBEAiAlGBZcXimcWfaFOa1d25n2Nz72Ds0IRan9dxrWJC0sIgIgXSqbKl+ro2OBZY0YQPevSAvXa6GU2DQgh/TWk1u1G64wggL5MIICf6ADAgECAhBW+4PUK/+NwzeZI7Varm69MAoGCCqGSM49BAMDMGcxGzAZBgNVBAMMEkFwcGxlIFJvb3QgQ0EgLSBHMzEmMCQGA1UECwwdQXBwbGUgQ2VydGlmaWNhdGlvbiBBdXRob3JpdHkxEzARBgNVBAoMCkFwcGxlIEluYy4xCzAJBgNVBAYTAlVTMB4XDTE5MDMyMjE3NTMzM1oXDTM0MDMyMjAwMDAwMFowfDEwMC4GA1UEAwwnQXBwbGUgQXBwbGljYXRpb24gSW50ZWdyYXRpb24gQ0EgNSAtIEcxMSYwJAYDVQQLDB1BcHBsZSBDZXJ0aWZpY2F0aW9uIEF1dGhvcml0eTETMBEGA1UECgwKQXBwbGUgSW5jLjELMAkGA1UEBhMCVVMwWTATBgcqhkjOPQIBBggqhkjOPQMBBwNCAASSzmO9fYaxqygKOxzhr/sElICRrPYx36bLKDVvREvhIeVX3RKNjbqCfJW+Sfq+M8quzQQZ8S9DJfr0vrPLg366o4H3MIH0MA8GA1UdEwEB/wQFMAMBAf8wHwYDVR0jBBgwFoAUu7DeoVgziJqkipnevr3rr9rLJKswRgYIKwYBBQUHAQEEOjA4MDYGCCsGAQUFBzABhipodHRwOi8vb2NzcC5hcHBsZS5jb20vb2NzcDAzLWFwcGxlcm9vdGNhZzMwNwYDVR0fBDAwLjAsoCqgKIYmaHR0cDovL2NybC5hcHBsZS5jb20vYXBwbGVyb290Y2FnMy5jcmwwHQYDVR0OBBYEFNkX/ktnkDhLkvTbztVXgBQLjz3JMA4GA1UdDwEB/wQEAwIBBjAQBgoqhkiG92NkBgIDBAIFADAKBggqhkjOPQQDAwNoADBlAjEAjW+mn6Hg5OxbTnOKkn89eFOYj/TaH1gew3VK/jioTCqDGhqqDaZkbeG5k+jRVUztAjBnOyy04eg3B3fL1ex2qBo6VTs/NWrIxeaSsOFhvoBJaeRfK6ls4RECqsxh2Ti3c0owggJDMIIByaADAgECAggtxfyI0sVLlTAKBggqhkjOPQQDAzBnMRswGQYDVQQDDBJBcHBsZSBSb290IENBIC0gRzMxJjAkBgNVBAsMHUFwcGxlIENlcnRpZmljYXRpb24gQXV0aG9yaXR5MRMwEQYDVQQKDApBcHBsZSBJbmMuMQswCQYDVQQGEwJVUzAeFw0xNDA0MzAxODE5MDZaFw0zOTA0MzAxODE5MDZaMGcxGzAZBgNVBAMMEkFwcGxlIFJvb3QgQ0EgLSBHMzEmMCQGA1UECwwdQXBwbGUgQ2VydGlmaWNhdGlvbiBBdXRob3JpdHkxEzARBgNVBAoMCkFwcGxlIEluYy4xCzAJBgNVBAYTAlVTMHYwEAYHKoZIzj0CAQYFK4EEACIDYgAEmOkvPUBypO2TInKBExzdEJXxxaNOcdwUFtkO5aYFKndke19OONO7HES1f/UftjJiXcnphFtPME8RWgD9WFgMpfUPLE0HRxN12peXl28xXO0rnXsgO9i5VNlemaQ6UQoxo0IwQDAdBgNVHQ4EFgQUu7DeoVgziJqkipnevr3rr9rLJKswDwYDVR0TAQH/BAUwAwEB/zAOBgNVHQ8BAf8EBAMCAQYwCgYIKoZIzj0EAwMDaAAwZQIxAIPpwcQWXhpdNBjZ7e/0bA4ARku437JGEcUP/eZ6jKGma87CA9Sc9ZPGdLhq36ojFQIwbWaKEMrUDdRPzY1DPrSKY6UzbuNt2he3ZB/IUyb5iGJ0OQsXW8tRqAzoGAPnorIoAAAxgfwwgfkCAQEwgZAwfDEwMC4GA1UEAwwnQXBwbGUgQXBwbGljYXRpb24gSW50ZWdyYXRpb24gQ0EgNSAtIEcxMSYwJAYDVQQLDB1BcHBsZSBDZXJ0aWZpY2F0aW9uIEF1dGhvcml0eTETMBEGA1UECgwKQXBwbGUgSW5jLjELMAkGA1UEBhMCVVMCEFkzVq3lWYLPREI3rN9FG1MwDQYJYIZIAWUDBAIBBQAwCgYIKoZIzj0EAwIERjBEAiBV14tWoThpbegi8yPQdRABtinRx/gy16V7AG7FJPqzKAIgAYAmJLoa7APuQm8/NilVHa9Z0KnkIPyCPfZUloW84rQAAAAAAABoYXV0aERhdGFYpEVlEup+JpR2q5Pht5cWhVkv9z+JSsDsL9VICKCL+2yPQAAAAABhcHBhdHRlc3RkZXZlbG9wACBiZsk7jHmcQdS+dyn3N1a5VmM0EQyAmfdx1JOgBdB7c6UBAgMmIAEhWCCIwDShkKp9vFoGFQHGVCgDlCWCGYs/HMVGc8o7mtILQSJYIFKCZ6VPX9ugRp+vtGu2mQo5a/BPlKSdQyDIHHqyQKOY" +data genuine_assertion: NonEmptyStr = "omlzaWduYXR1cmVYRjBEAiBJ6BT/QR689UKy84YyN3RDydYD9KVQ2BTRK+x1i8ezqAIgGM7BsZbSuF6TjmK6xtOFekyVyjf8akGvp5qFRGm9LTxxYXV0aGVudGljYXRvckRhdGFYJUVlEup+JpR2q5Pht5cWhVkv9z+JSsDsL9VICKCL+2yPQAAAAAE=" +data genuine_key_id: AttestKeyId = "YmbJO4x5nEHUvncp9zdWuVZjNBEMgJn3cdSToAXQe3M=" as AttestKeyId +data genuine_client_data: NonEmptyStr = "wurzelpfropf" +data captured_at: Int = 1611404013 +data genuine_point: NonEmptyStr = "BIjANKGQqn28WgYVAcZUKAOUJYIZiz8cxUZzyjua0gtBUoJnpU9f26BGn6-0a7aZCjlr8E-UpJ1DIMgcerJAo5g" + +data genuine_observed_at: Timestamp = "2021-01-23T12:13:33Z" +data admitted_categories: List = [2, 3] + +fn genuine_octets() -> List { + match base64_decode(s: genuine_attestation as String, variant: Standard) { + Present { value: o } => o + Absent => [] + } +} + +fn reencode(octets: List) -> NonEmptyStr { + match base64_encode(octets: octets, variant: Standard) { + Present { value: s } => s as NonEmptyStr + Absent => "!" as NonEmptyStr + } +} + +fn verify_genuine(environment: AppAttestEnvironment, policy: AppAttestLaunchExtensionPolicy, key_id: AttestKeyId, now: Int) -> AttestationVerification { + app_attest_verify(environment: environment, policy: policy, admitted_categories: admitted_categories, attestation_b64: genuine_attestation, key_id: key_id, now_epoch: now) +} + +fn verify_bytes(octets: List) -> AttestationVerification { + app_attest_verify(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, admitted_categories: admitted_categories, attestation_b64: reencode(octets: octets), key_id: genuine_key_id, now_epoch: captured_at) +} + +// ── The genuine object decodes to the independently read values ───────────────────────────── + +test fn the_genuine_attestation_decodes_to_its_independently_read_fields() -> Bool { + let input = genuine_octets() + match app_attest_attestation_object(input: input) { + AppAttestAttestationRefused { cause: _ } => false + AppAttestAttestationReady { value: obj } => + count(obj.certificates) == 2 + && obj.auth_data.counter == 0 + && match obj.auth_data.extensions { Absent => true Present { value: _ } => false } + && match obj.auth_data.credential { + Absent => false + Present { value: c } => + match app_attest_environment_of(input: input, aaguid: c.aaguid) { + Present { value: AppAttestDevelopment } => true + _ => false + } + && match base64_decode(s: genuine_key_id as String, variant: Standard) { + Present { value: k } => octet_span_octets(input: input, span: c.credential_id) == k + Absent => false + } + } + } +} + +// The leaf certificate's subject public key IS the credential key the authenticator data carries: +// 0x04 || x || y from the COSE key equals the SEC1 point in the certificate. +test fn the_leaf_certificate_key_is_the_attested_credential_key() -> Bool { + let input = genuine_octets() + match app_attest_attestation_object(input: input) { + AppAttestAttestationRefused { cause: _ } => false + AppAttestAttestationReady { value: obj } => + match obj.auth_data.credential { + Absent => false + Present { value: c } => + match obj.certificates.first() { + Absent => false + Present { value: leaf_span } => { + let leaf = octet_span_octets(input: input, span: leaf_span) + match x509_certificate(input: leaf, span: OctetSpan { start: 0, end: count(leaf) }) { + X509Refused { cause: _ } => false + X509Ready { certificate: cert } => + octet_span_octets(input: leaf, span: cert.public_key.point) + == append(append([4], items: octet_span_octets(input: input, span: c.x)), items: octet_span_octets(input: input, span: c.y)) + && cert.not_before == 1611317615 + && cert.not_after == 1611576815 + } + } + } + } + } +} + +// ── The verifier: every decidable step runs, and it never answers Verified ────────────────── + +// Under a policy requiring the launch extensions, the pre-iOS-17 genuine object is refused at step +// 9, which is only reached after the chain structure (1), counter (6), environment (7) and +// credential id (8) all passed on genuine bytes. +test fn the_genuine_attestation_passes_the_decidable_steps_and_stops_at_the_absent_category() -> Bool { + match verify_genuine(environment: AppAttestDevelopment, policy: LaunchExtensionsRequired, key_id: genuine_key_id, now: captured_at) { + AttestationRefused { cause: AttestationValidationCategoryAbsent } => true + _ => false + } +} + +// With the extensions optional, every decidable step passes and the verifier refuses at the ECDSA +// frontier. It does NOT answer AttestationVerified: no signature was checked. +test fn a_genuine_attestation_refuses_at_the_ecdsa_frontier_and_is_never_verified() -> Bool { + match verify_genuine(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, key_id: genuine_key_id, now: captured_at) { + AttestationRefused { cause: AttestationVerificationUnrealized { capability: AppAttestEcdsaSignatureVerification } } => true + _ => false + } +} + +test fn a_development_attestation_is_refused_where_production_is_required() -> Bool { + match verify_genuine(environment: AppAttestProduction, policy: LaunchExtensionsOptional, key_id: genuine_key_id, now: captured_at) { + AttestationRefused { cause: AttestationEnvironmentUnexpected { expected: _ } } => true + _ => false + } +} + +test fn the_wrong_key_id_is_refused_at_the_credential_id() -> Bool { + match verify_genuine(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, key_id: "AAAAO4x5nEHUvncp9zdWuVZjNBEMgJn3cdSToAXQe3M=" as AttestKeyId, now: captured_at) { + AttestationRefused { cause: AttestationCredentialIdMismatch { declared: _ } } => true + _ => false + } +} + +test fn the_genuine_chain_is_refused_after_its_leaf_expires() -> Bool { + match verify_genuine(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, key_id: genuine_key_id, now: 1790000000) { + AttestationRefused { cause: AttestationChainUntrusted { cause: X509Expired { depth: d, not_after: t } } } => d == 0 && t == 1611576815 + _ => false + } +} + +test fn the_genuine_chain_is_refused_before_its_leaf_is_valid() -> Bool { + match verify_genuine(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, key_id: genuine_key_id, now: 1600000000) { + AttestationRefused { cause: AttestationChainUntrusted { cause: X509NotYetValid { depth: d, not_before: _ } } } => d == 0 + _ => false + } +} + +// ── Adversarial controls over the genuine bytes (and the route's bypass discriminator) ────── + +test fn trailing_cbor_after_the_attestation_is_refused() -> Bool { + match verify_bytes(octets: append(genuine_octets(), items: [0])) { + AttestationRefused { cause: AttestationMalformed { cause: AppAttestCborRefused { cause: CborTrailingInput { at: _, remaining: r } } } } => r == 1 + _ => false + } +} + +// The top-level map header 0xA3 (three entries) becomes 0xA4, and a second "fmt" entry is appended. +test fn a_duplicate_top_level_key_is_refused() -> Bool { + let dup: List = [99, 102, 109, 116, 97, 120] + match verify_bytes(octets: append(append([164], items: genuine_octets().skip(n: 1)), items: dup)) { + AttestationRefused { cause: AttestationMalformed { cause: AppAttestCborRefused { cause: CborDuplicateMapKey { at: _ } } } } => true + _ => false + } +} + +test fn an_unknown_top_level_key_is_refused() -> Bool { + let unknown: List = [99, 122, 122, 122, 0] + match verify_bytes(octets: append(append([164], items: genuine_octets().skip(n: 1)), items: unknown)) { + AttestationRefused { cause: AttestationMalformed { cause: AppAttestUnknownField } } => true + _ => false + } +} + +test fn a_certificate_with_trailing_bytes_is_refused() -> Bool { + let input = genuine_octets() + match app_attest_attestation_object(input: input) { + AppAttestAttestationRefused { cause: _ } => false + AppAttestAttestationReady { value: obj } => + match obj.certificates.first() { + Absent => false + Present { value: leaf_span } => { + let padded = append(octet_span_octets(input: input, span: leaf_span), items: [0]) + match x509_certificate(input: padded, span: OctetSpan { start: 0, end: count(padded) }) { + X509Refused { cause: X509Malformed { cause: DerTrailingInput { at: _, remaining: r } } } => r == 1 + _ => false + } + } + } + } +} + +test fn text_that_is_not_base64_is_refused() -> Bool { + match app_attest_verify(environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, admitted_categories: admitted_categories, attestation_b64: "not*base64", key_id: genuine_key_id, now_epoch: captured_at) { + AttestationRefused { cause: AttestationMalformed { cause: AppAttestBase64Invalid } } => true + _ => false + } +} + +// ── Assertions ─────────────────────────────────────────────────────────────────────────────── + +test fn the_genuine_assertion_decodes_and_refuses_at_the_sha256_frontier() -> Bool { + match app_attest_verify_assertion(assertion_b64: genuine_assertion) { + AssertionRefused { cause: AssertionVerificationUnrealized { capability: AppAttestSha256Digest } } => true + _ => false + } +} + +// Read independently: the genuine assertion's authenticator data is 37 octets, flags 0x40, counter 1. +test fn the_genuine_assertion_decodes_to_counter_one() -> Bool { + match base64_decode(s: genuine_assertion as String, variant: Standard) { + Absent => false + Present { value: octets } => + match app_attest_assertion_object(input: octets) { + AppAttestAssertionReady { value: a } => a.auth_data.counter == 1 && a.auth_data.whole.end - a.auth_data.whole.start == 37 + AppAttestAssertionRefused { cause: _ } => false + } + } +} + +test fn an_assertion_with_trailing_cbor_is_refused() -> Bool { + match base64_decode(s: genuine_assertion as String, variant: Standard) { + Absent => false + Present { value: octets } => + match app_attest_verify_assertion(assertion_b64: reencode(octets: append(octets, items: [0]))) { + AssertionRefused { cause: AssertionMalformed { cause: AppAttestCborRefused { cause: CborTrailingInput { at: _, remaining: _ } } } } => true + _ => false + } + } +} + +// ── The route: the enrolment parse stage runs the modeled decoder ─────────────────────────── + +data decision_key: VerifyingKey = VerifyingKey { suite: EcdsaP256Sha256, encoding: Sec1Uncompressed, point_b64url: "BKEYA" } + +fn live_slot() -> EnrolmentSlotStanding { + EnrolmentCodeUnspent { + challenge: EnrolmentChallenge { code: "482913", issued_to_login: approval_operator_login, issued_at: "2021-01-23T12:10:00Z", expires_at: "2021-01-23T12:20:00Z" } + } +} + +// The genuine attestation reaches the route, decodes, passes every decidable step, and the route +// REFUSES the enrolment at the ECDSA frontier. It is never admitted. +test fn the_enrolment_route_refuses_a_genuine_attestation_at_the_ecdsa_frontier() -> Bool { + match ios_enrolment_admission( + slot: live_slot(), decision_key: decision_key, attestation_b64: genuine_attestation, key_id: genuine_key_id, + environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, admitted_categories: admitted_categories, + observed_at: genuine_observed_at, + ) { + EnrolmentRefused { cause: EnrolmentAttestationRefused { cause: AttestationVerificationUnrealized { capability: AppAttestEcdsaSignatureVerification } } } => true + _ => false + } +} + +// THE ROUTE'S BYPASS DISCRIMINATOR: a duplicate key the modeled CBOR decoder refuses reaches the +// route as that decoder's typed cause. A route that walked the bytes by hand would not see it. +test fn the_enrolment_route_refuses_a_duplicate_key_through_the_modeled_decoder() -> Bool { + let dup: List = [99, 102, 109, 116, 97, 120] + match ios_enrolment_admission( + slot: live_slot(), decision_key: decision_key, + attestation_b64: reencode(octets: append(append([164], items: genuine_octets().skip(n: 1)), items: dup)), + key_id: genuine_key_id, environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, + admitted_categories: admitted_categories, observed_at: genuine_observed_at, + ) { + EnrolmentRefused { cause: EnrolmentAttestationRefused { cause: AttestationMalformed { cause: AppAttestCborRefused { cause: CborDuplicateMapKey { at: _ } } } } } => true + _ => false + } +} + +test fn the_enrolment_route_refuses_an_unreadable_observation_time() -> Bool { + match ios_enrolment_admission( + slot: live_slot(), decision_key: decision_key, attestation_b64: genuine_attestation, key_id: genuine_key_id, + environment: AppAttestDevelopment, policy: LaunchExtensionsOptional, admitted_categories: admitted_categories, + observed_at: "2021-01-23 12:13:33", + ) { + EnrolmentRefused { cause: EnrolmentObservationTimeUnreadable { observed_at: _ } } => true + _ => false + } +} diff --git a/dag/test/claim/base64_rfc4648_witness_test.dag b/dag/test/claim/base64_rfc4648_witness_test.dag index 24c1720482e..a8e4ca3fb28 100644 --- a/dag/test/claim/base64_rfc4648_witness_test.dag +++ b/dag/test/claim/base64_rfc4648_witness_test.dag @@ -3,8 +3,21 @@ module test.claim.base64_rfc4648_witness data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly +// base64_encode gained a refusal channel when NUMERIC-BIT-0 (gunbc#11627) switched its packing to +// std.machine_word: an octet outside the byte range used to be multiplied into a plausible wrong +// string, and now refuses. This projection discharges that channel with a sentinel that no valid +// encoding can produce, so a refusal reds a golden vector rather than being read as an empty +// string -- "" is base64_encode's answer for the empty input and is therefore not available as a +// failure marker. The refusal itself is claimed directly in machine_word_witness_test. fn b64_std_of_utf8(s: String) -> String { - base64_encode(octets: bytes_octets(b: utf8_encode_bytes(s: s)), variant: Standard) + base64_encode_or_refused(octets: bytes_octets(b: utf8_encode_bytes(s: s)), variant: Standard) +} + +fn base64_encode_or_refused(octets: List, variant: Base64Variant) -> String { + match base64_encode(octets: octets, variant: variant) { + Present { value: encoded } => encoded + Absent => "REFUSED" + } } data url_witness_octets: List = [251, 255, 191] @@ -20,7 +33,7 @@ test fn utf8_total_direction_holds() -> Bool { test fn base64_octet_roundtrip_holds() -> Bool { let o = bytes_octets(b: utf8_encode_bytes(s: "foobar")) - match base64_decode(s: base64_encode(octets: o, variant: Standard), variant: Standard) { + match base64_decode(s: base64_encode_or_refused(octets: o, variant: Standard), variant: Standard) { Present { value: d } => d == o Absent => false } @@ -73,13 +86,43 @@ test fn base64_rfc4648_golden_vectors_holds() -> Bool { } test fn base64url_alphabet_golden_holds() -> Bool { - base64_encode(octets: url_witness_octets, variant: Standard) == "+/+/" - && base64_encode(octets: url_witness_octets, variant: UrlSafe) == "-_-_" + base64_encode_or_refused(octets: url_witness_octets, variant: Standard) == "+/+/" + && base64_encode_or_refused(octets: url_witness_octets, variant: UrlSafe) == "-_-_" } test fn base64url_roundtrip_holds() -> Bool { - match base64_decode(s: base64_encode(octets: url_witness_octets, variant: UrlSafe), variant: UrlSafe) { + match base64_decode(s: base64_encode_or_refused(octets: url_witness_octets, variant: UrlSafe), variant: UrlSafe) { Present { value: d } => d == url_witness_octets Absent => false } } + +// THE OCTET ADMISSION CONTROL FOR utf8_decode_octets, and the input that discriminates. +// +// This fold read each member through base64_octet_int, the `b + 0` identity NUMERIC-BIT-0 deleted; +// it now admits through base64_octet_word, which refuses a value outside the byte range. The two +// agree on 256 -- the old path reached utf8_step and refused there anyway -- so 256 proves nothing. +// A NEGATIVE member is the discriminator: the old identity handed -1 straight to utf8_step, where +// `o < 128` is TRUE, so it was decoded as an ASCII scalar and appended to the output as a code +// point of -1. Admission refuses it instead. Reverting to the identity turns this Absent into a +// Present carrying that fabricated scalar. +test fn utf8_decode_octets_refuses_a_negative_octet_holds() -> Bool { + match utf8_decode_octets(octets: [0 - 1]) { + Absent => true + Present { value: _ } => false + } +} + +test fn utf8_decode_octets_still_decodes_ascii_holds() -> Bool { + match utf8_decode_octets(octets: [102, 111, 111]) { + Present { value: cps } => cps == [102, 111, 111] + Absent => false + } +} + +test fn utf8_decode_octets_still_refuses_a_bad_lead_holds() -> Bool { + match utf8_decode_octets(octets: [255]) { + Absent => true + Present { value: _ } => false + } +} diff --git a/dag/test/claim/cbor_rfc8949_witness_test.dag b/dag/test/claim/cbor_rfc8949_witness_test.dag new file mode 100644 index 00000000000..2ff0614b2b2 --- /dev/null +++ b/dag/test/claim/cbor_rfc8949_witness_test.dag @@ -0,0 +1,200 @@ +module test.claim.cbor_rfc8949_witness_test + +import std.integer { UInt8 } +import std.octet_span { OctetSpan, octet_span_octets } +import extdeps.ietf.cbor { + CborItem, CborEntry, CborUnsigned, CborNegative, CborBytes, CborText, CborArray, CborMap, CborTagged, + CborFalse, CborTrue, CborNull, + CborDecode, CborDecoded, CborRefused, + CborTruncated, CborReservedAdditionalInfo, CborIndefiniteLengthUnsupported, CborNoncanonicalArgument, + CborArgumentTooWide, CborSimpleValueUnsupported, CborDuplicateMapKey, CborTrailingInput, CborNestingExhausted, + cbor_decode, cbor_map_text_value, cbor_map_int_value, cbor_int_value, +} +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// Fixed vectors are RFC 8949 Appendix A ("Examples of Encoded CBOR Data Items"), independent of +// this decoder. The refusals are one adversarial input per named departure from the deterministic +// encoding, each chosen so the only reason to refuse is the property under test. + +fn decodes_unsigned(input: List, expected: Int) -> Bool { + match cbor_decode(input: input) { + CborDecoded { item: CborUnsigned { value: v } } => v == expected + _ => false + } +} + +fn decodes_int(input: List, expected: Int) -> Bool { + match cbor_decode(input: input) { + CborDecoded { item: item } => + match cbor_int_value(item: item) { + Present { value: v } => v == expected + Absent => false + } + CborRefused { cause: _ } => false + } +} + +test fn rfc8949_unsigned_vectors() -> Bool { + decodes_unsigned(input: [0], expected: 0) + && decodes_unsigned(input: [23], expected: 23) + && decodes_unsigned(input: [24, 24], expected: 24) + && decodes_unsigned(input: [24, 100], expected: 100) + && decodes_unsigned(input: [25, 3, 232], expected: 1000) + && decodes_unsigned(input: [26, 0, 15, 66, 64], expected: 1000000) +} + +test fn rfc8949_negative_vectors() -> Bool { + decodes_int(input: [32], expected: 0 - 1) + && decodes_int(input: [41], expected: 0 - 10) + && decodes_int(input: [56, 99], expected: 0 - 100) + && decodes_int(input: [57, 3, 231], expected: 0 - 1000) +} + +test fn rfc8949_byte_and_text_strings_are_spans_of_the_input() -> Bool { + let bytes_input: List = [68, 1, 2, 3, 4] + let text_input: List = [100, 73, 69, 84, 70] + let bytes_ok = match cbor_decode(input: bytes_input) { + CborDecoded { item: CborBytes { span: s } } => octet_span_octets(input: bytes_input, span: s) == [1, 2, 3, 4] + _ => false + } + let text_ok = match cbor_decode(input: text_input) { + CborDecoded { item: CborText { span: s } } => octet_span_octets(input: text_input, span: s) == [73, 69, 84, 70] + _ => false + } + let empty_ok = match cbor_decode(input: [64]) { + CborDecoded { item: CborBytes { span: s } } => s.start == 1 && s.end == 1 + _ => false + } + bytes_ok && text_ok && empty_ok +} + +test fn rfc8949_arrays_nest() -> Bool { + match cbor_decode(input: [131, 1, 130, 2, 3, 130, 4, 5]) { + CborDecoded { item: CborArray { items: items } } => + count(items) == 3 + && match items |> get(1) { + Present { value: CborArray { items: inner } } => count(inner) == 2 + _ => false + } + _ => false + } +} + +test fn rfc8949_maps_read_by_integer_and_text_key() -> Bool { + let int_map: List = [162, 1, 2, 3, 4] + let text_map: List = [162, 97, 97, 1, 97, 98, 130, 2, 3] + let by_int = match cbor_decode(input: int_map) { + CborDecoded { item: CborMap { entries: es } } => + match cbor_map_int_value(entries: es, label: 3) { + Present { value: CborUnsigned { value: v } } => v == 4 + _ => false + } + _ => false + } + let by_text = match cbor_decode(input: text_map) { + CborDecoded { item: CborMap { entries: es } } => + match cbor_map_text_value(input: text_map, entries: es, key: [98]) { + Present { value: CborArray { items: xs } } => count(xs) == 2 + _ => false + } + _ => false + } + by_int && by_text +} + +test fn rfc8949_simple_values_and_tags() -> Bool { + let simple = match cbor_decode(input: [244]) { CborDecoded { item: CborFalse } => true _ => false } + && match cbor_decode(input: [245]) { CborDecoded { item: CborTrue } => true _ => false } + && match cbor_decode(input: [246]) { CborDecoded { item: CborNull } => true _ => false } + let tagged = match cbor_decode(input: [193, 26, 81, 75, 103, 176]) { + CborDecoded { item: CborTagged { tag: t, item: CborUnsigned { value: v } } } => t == 1 && v == 1363896240 + _ => false + } + simple && tagged +} + +test fn refuses_a_non_shortest_argument() -> Bool { + match cbor_decode(input: [24, 23]) { + CborRefused { cause: CborNoncanonicalArgument { at: a } } => a == 0 + _ => false + } +} + +test fn refuses_a_two_octet_argument_that_fits_one() -> Bool { + match cbor_decode(input: [25, 0, 255]) { + CborRefused { cause: CborNoncanonicalArgument { at: _ } } => true + _ => false + } +} + +test fn refuses_indefinite_length() -> Bool { + match cbor_decode(input: [95, 65, 1, 255]) { + CborRefused { cause: CborIndefiniteLengthUnsupported { at: a } } => a == 0 + _ => false + } +} + +test fn refuses_reserved_additional_information() -> Bool { + match cbor_decode(input: [28]) { + CborRefused { cause: CborReservedAdditionalInfo { at: _, info: i } } => i == 28 + _ => false + } +} + +test fn refuses_a_duplicate_map_key() -> Bool { + match cbor_decode(input: [162, 97, 97, 1, 97, 97, 2]) { + CborRefused { cause: CborDuplicateMapKey { at: a } } => a == 4 + _ => false + } +} + +test fn refuses_trailing_input() -> Bool { + match cbor_decode(input: [0, 0]) { + CborRefused { cause: CborTrailingInput { at: a, remaining: r } } => a == 1 && r == 1 + _ => false + } +} + +test fn refuses_a_truncated_string() -> Bool { + match cbor_decode(input: [68, 1, 2]) { + CborRefused { cause: CborTruncated { at: a, needed: n, available: v } } => a == 1 && n == 4 && v == 2 + _ => false + } +} + +test fn refuses_a_truncated_argument() -> Bool { + match cbor_decode(input: [25, 1]) { + CborRefused { cause: CborTruncated { at: _, needed: _, available: _ } } => true + _ => false + } +} + +test fn refuses_an_array_count_the_input_cannot_hold() -> Bool { + match cbor_decode(input: [152, 200, 0]) { + CborRefused { cause: CborTruncated { at: _, needed: n, available: _ } } => n == 200 + _ => false + } +} + +test fn refuses_floats_as_unsupported() -> Bool { + match cbor_decode(input: [249, 60, 0]) { + CborRefused { cause: CborSimpleValueUnsupported { at: _, info: i } } => i == 25 + _ => false + } +} + +test fn refuses_an_eight_octet_argument_as_too_wide() -> Bool { + match cbor_decode(input: [27, 0, 0, 0, 1, 0, 0, 0, 0]) { + CborRefused { cause: CborArgumentTooWide { at: _ } } => true + _ => false + } +} + +test fn refuses_nesting_past_the_bound() -> Bool { + match cbor_decode(input: [129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 129, 0]) { + CborRefused { cause: CborNestingExhausted { at: _ } } => true + _ => false + } +} diff --git a/dag/test/claim/der_x690_witness_test.dag b/dag/test/claim/der_x690_witness_test.dag new file mode 100644 index 00000000000..1ee0a09d3cc --- /dev/null +++ b/dag/test/claim/der_x690_witness_test.dag @@ -0,0 +1,229 @@ +module test.claim.der_x690_witness_test + +import std.logic { Bool } +import std.types { String, Int, List } +import std.integer { UInt8 } +import std.octet_span { OctetSpan, octet_span_octets } +import extdeps.itu.der { + DerElement, DerRead, DerReadReady, DerReadRefused, DerChildrenReady, DerChildrenRefused, + DerTruncated, DerHighTagNumberUnsupported, DerIndefiniteLength, DerNoncanonicalLength, DerTrailingInput, + DerNoncanonicalInteger, DerNoncanonicalBoolean, DerBitStringMalformed, DerObjectIdentifierMalformed, + DerObjectIdentifierReady, DerObjectIdentifierRefused, DerBooleanReady, DerBooleanRefused, + DerBitStringReady, DerBitStringRefused, DerContextSpecific, + der_read_element, der_read_exact, der_children, der_integer_content, der_boolean, der_bit_string, der_object_identifier, +} +import extdeps.ietf.x509 { X509Extension, x509_key_usage_permits_cert_sign } +import extdeps.time.posix_epoch { CivilDateTime, civil_epoch_seconds, days_from_civil } +import extdeps.time.rfc3339 { rfc3339_epoch_seconds } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// Fixed vectors: X.690 (02/2021) itself -- its 8.19.5 OID example {2 999 3} encodes as 06 03 88 37 +// 03 -- plus the RSA OID 1.2.840.113549 (06 06 2A 86 48 86 F7 0D), and one adversarial input per +// DER refusal, each differing from an accepted input only in the property under test. Epoch values +// are POSIX seconds cross-checked with `date -u -d`. + +fn zeros(n: Int, acc: List) -> List { + if n == 0 { acc } else { zeros(n: n - 1, acc: acc |> list_push(0)) } +} + +fn whole(input: List) -> OctetSpan { + OctetSpan { start: 0, end: count(input) } +} + +fn element(input: List) -> DerElement? { + match der_read_exact(input: input, span: whole(input: input)) { + DerReadReady { element: e } => Present { value: e } + DerReadRefused { cause: _ } => none + } +} + +fn arcs_of(input: List) -> List? { + match element(input: input) { + Absent => none + Present { value: e } => + match der_object_identifier(input: input, element: e) { + DerObjectIdentifierReady { arcs: a } => Present { value: a } + DerObjectIdentifierRefused { cause: _ } => none + } + } +} + +test fn reads_short_and_long_form_lengths() -> Bool { + let short: List = [4, 1, 7] + let long: List = append([4, 129, 128], items: zeros(n: 128, acc: [])) + match element(input: short) { + Present { value: e } => octet_span_octets(input: short, span: e.content) == [7] + Absent => false + } && match element(input: long) { + Present { value: e } => e.content.start == 3 && e.content.end == 131 + Absent => false + } +} + +test fn refuses_a_long_form_length_short_form_could_carry() -> Bool { + match der_read_element(input: [4, 129, 1, 7], at: 0) { + DerReadRefused { cause: DerNoncanonicalLength { at: a } } => a == 1 + _ => false + } +} + +test fn refuses_a_long_form_length_with_a_leading_zero_octet() -> Bool { + match der_read_element(input: append([4, 130, 0, 200], items: zeros(n: 200, acc: [])), at: 0) { + DerReadRefused { cause: DerNoncanonicalLength { at: _ } } => true + _ => false + } +} + +test fn refuses_the_indefinite_length_form() -> Bool { + match der_read_element(input: [48, 128, 0, 0], at: 0) { + DerReadRefused { cause: DerIndefiniteLength { at: _ } } => true + _ => false + } +} + +test fn refuses_a_content_longer_than_the_input() -> Bool { + match der_read_element(input: [4, 5, 1, 2], at: 0) { + DerReadRefused { cause: DerTruncated { at: _, needed: n, available: v } } => n == 5 && v == 2 + _ => false + } +} + +test fn refuses_trailing_octets_after_an_exact_element() -> Bool { + let input: List = [4, 1, 7, 0] + match der_read_exact(input: input, span: whole(input: input)) { + DerReadRefused { cause: DerTrailingInput { at: a, remaining: r } } => a == 3 && r == 1 + _ => false + } +} + +test fn refuses_the_high_tag_number_form() -> Bool { + match der_read_element(input: [159, 120, 1, 0], at: 0) { + DerReadRefused { cause: DerHighTagNumberUnsupported { at: _ } } => true + _ => false + } +} + +test fn reads_context_specific_constructed_tags() -> Bool { + match der_read_element(input: [163, 3, 2, 1, 5], at: 0) { + DerReadReady { element: e } => + e.tag == 3 && e.constructed && match e.class { DerContextSpecific => true _ => false } + _ => false + } +} + +test fn a_sequence_s_children_must_tile_its_content() -> Bool { + let ok: List = [48, 6, 2, 1, 1, 2, 1, 2] + let bad: List = [48, 5, 2, 1, 1, 2, 1, 2] + let ok_children = match element(input: ok) { + Present { value: e } => + match der_children(input: ok, parent: e) { + DerChildrenReady { children: cs } => count(cs) == 2 + DerChildrenRefused { cause: _ } => false + } + Absent => false + } + let bad_children = match der_read_element(input: bad, at: 0) { + DerReadReady { element: e } => + match der_children(input: bad, parent: e) { + DerChildrenRefused { cause: DerTruncated { at: _, needed: _, available: _ } } => true + _ => false + } + DerReadRefused { cause: _ } => false + } + ok_children && bad_children +} + +test fn integers_must_be_minimal() -> Bool { + let accepted = [[2, 1, 0], [2, 2, 0, 128], [2, 1, 127]] + let refused = [[2, 2, 0, 127], [2, 2, 255, 128], [2, 0]] + all(accepted, i => match der_read_element(input: i, at: 0) { + DerReadReady { element: e } => match der_integer_content(input: i, element: e) { DerReadReady { element: _ } => true _ => false } + DerReadRefused { cause: _ } => false + }) + && all(refused, i => match der_read_element(input: i, at: 0) { + DerReadReady { element: e } => match der_integer_content(input: i, element: e) { DerReadRefused { cause: DerNoncanonicalInteger { at: _ } } => true _ => false } + DerReadRefused { cause: _ } => false + }) +} + +test fn booleans_are_ff_or_00_only() -> Bool { + let t: List = [1, 1, 255] + let f: List = [1, 1, 0] + let bad: List = [1, 1, 1] + match element(input: t) { Present { value: e } => match der_boolean(input: t, element: e) { DerBooleanReady { value: v } => v _ => false } Absent => false } + && match element(input: f) { Present { value: e } => match der_boolean(input: f, element: e) { DerBooleanReady { value: v } => !v _ => false } Absent => false } + && match element(input: bad) { Present { value: e } => match der_boolean(input: bad, element: e) { DerBooleanRefused { cause: DerNoncanonicalBoolean { at: _ } } => true _ => false } Absent => false } +} + +test fn bit_strings_carry_their_unused_bit_count() -> Bool { + let ok: List = [3, 2, 7, 128] + let bad: List = [3, 1, 1] + match element(input: ok) { + Present { value: e } => match der_bit_string(input: ok, element: e) { DerBitStringReady { value: b } => b.unused_bits == 7 && octet_span_octets(input: ok, span: b.bits) == [128] _ => false } + Absent => false + } && match element(input: bad) { + Present { value: e } => match der_bit_string(input: bad, element: e) { DerBitStringRefused { cause: DerBitStringMalformed { at: _ } } => true _ => false } + Absent => false + } +} + +// review 68531: an EMPTY BIT STRING (03 00) has no unused-bits octet. It must refuse, not read the +// next element's first byte (05 here, which is <= 7) as its own. +test fn an_empty_bit_string_is_refused_and_never_reads_its_neighbour() -> Bool { + let input: List = [3, 0, 5, 0] + match der_read_element(input: input, at: 0) { + DerReadRefused { cause: _ } => false + DerReadReady { element: e } => + match der_bit_string(input: input, element: e) { + DerBitStringRefused { cause: DerBitStringMalformed { at: a } } => a == 0 + _ => false + } + } +} + +// review 68531: KeyUsage 03 01 00 names NO bits, so it does not permit keyCertSign -- even when the +// octet after it (04) has the keyCertSign bit set. The positive control 03 02 01 04 names it. +test fn an_empty_key_usage_does_not_grant_cert_sign_from_the_next_byte() -> Bool { + let empty: List = [3, 1, 0, 4] + let named: List = [3, 2, 1, 4] + !x509_key_usage_permits_cert_sign(input: empty, ext: X509Extension { oid: [2, 5, 29, 15], critical: true, value: OctetSpan { start: 0, end: 3 } }) + && x509_key_usage_permits_cert_sign(input: named, ext: X509Extension { oid: [2, 5, 29, 15], critical: true, value: OctetSpan { start: 0, end: 4 } }) +} + +test fn object_identifiers_decode_the_x690_example_and_a_multi_octet_arc() -> Bool { + arcs_of(input: [6, 3, 136, 55, 3]) == Present { value: [2, 999, 3] } + && arcs_of(input: [6, 6, 42, 134, 72, 134, 247, 13]) == Present { value: [1, 2, 840, 113549] } +} + +test fn object_identifiers_refuse_a_padded_or_unterminated_subidentifier() -> Bool { + let padded: List = [6, 2, 128, 1] + let unterminated: List = [6, 1, 134] + arcs_of(input: padded) == none && arcs_of(input: unterminated) == none +} + +// ── Calendar and RFC 3339 ───────────────────────────────────────────────────────────────────── + +test fn posix_epoch_matches_independent_dates() -> Bool { + days_from_civil(year: 1970, month: 1, day: 1) == 0 + && days_from_civil(year: 2000, month: 3, day: 1) == 11017 + && days_from_civil(year: 1969, month: 12, day: 31) == 0 - 1 + && civil_epoch_seconds(t: CivilDateTime { year: 2021, month: 1, day: 22, hour: 12, minute: 13, second: 35 }) == Present { value: 1611317615 } + && civil_epoch_seconds(t: CivilDateTime { year: 2045, month: 3, day: 15, hour: 0, minute: 0, second: 0 }) == Present { value: 2373148800 } +} + +test fn civil_dates_refuse_impossible_days_and_leap_seconds() -> Bool { + civil_epoch_seconds(t: CivilDateTime { year: 2024, month: 2, day: 29, hour: 0, minute: 0, second: 0 }) != none + && civil_epoch_seconds(t: CivilDateTime { year: 2023, month: 2, day: 29, hour: 0, minute: 0, second: 0 }) == none + && civil_epoch_seconds(t: CivilDateTime { year: 1900, month: 2, day: 29, hour: 0, minute: 0, second: 0 }) == none + && civil_epoch_seconds(t: CivilDateTime { year: 2016, month: 12, day: 31, hour: 23, minute: 59, second: 60 }) == none +} + +test fn rfc3339_canonical_instants_parse_and_others_refuse() -> Bool { + rfc3339_epoch_seconds(value: "2021-01-23T12:13:33Z") == Present { value: 1611404013 } + && rfc3339_epoch_seconds(value: "2021-01-23t12:13:33Z") == none + && rfc3339_epoch_seconds(value: "2021-01-23T12:13:33.5Z") == none + && rfc3339_epoch_seconds(value: "2021-01-23T12:13:33+00:00") == none + && rfc3339_epoch_seconds(value: "2021-02-30T00:00:00Z") == none +} diff --git a/dag/test/claim/machine_word_witness_test.dag b/dag/test/claim/machine_word_witness_test.dag new file mode 100644 index 00000000000..cf725ebe2b0 --- /dev/null +++ b/dag/test/claim/machine_word_witness_test.dag @@ -0,0 +1,684 @@ +module test.claim.machine_word_witness + + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// VECTORS, NOT MEASUREMENTS. Every expected value below is derived from the definition of the +// operation at the stated width -- a rotation is the two shifts summed, a big-endian packing is the +// positional radix-256 value, a wrapping add is the sum modulo 2^32 -- and NOT read back out of +// this implementation. A test whose oracle is the tree it measures collapses to measure() == +// measure(); these are the operations' own arithmetic, computed independently. +// +// THE MUTATION CONTROLS THE BRIEF NAMES ARE EACH PINNED IN BOTH DIRECTIONS, because a single-sided +// claim survives the mutation it exists to catch. Rotate direction: left and right of the SAME +// asymmetric word are both pinned, so swapping the two implementations reds both rather than +// permuting one green into another. Endianness: big and little of the same octets are both pinned, +// for the same reason. Carry: the crossing and the non-crossing case. Modular reduction: a sum that +// wraps and one that does not. +fn word32_or_zero(value: Int) -> Word { + match word_of_int(width: Width32, value: value) { + WordReady { word: w } => w + WordRefused { cause: _ } => Word { width: Width32, value: 0 } + } +} + +fn word32_value_or(result: WordResult, fallback: Int) -> Int { + match result { + WordReady { word: w } => w.value + WordRefused { cause: _ } => fallback + } +} + +// REFUSING IS NOT THE CLAIM; REFUSING FOR THE STATED REASON IS. A helper answering true for ANY +// cause was the one these claims used, and a claim built on it is satisfied by an operation that +// refuses for a reason the claim is not about -- a width mismatch standing in for an out-of-range value, or an unrealizable +// width standing in for an out-of-range amount. That is the shape review 68385 found in the +// typecheck control and review 68118 found in the packing guard, and I found it here by auditing +// my own claims for it rather than waiting for a sixth review to. These two name the cause each +// claim exists to pin; the any-cause helper had no consumer left afterwards and is deleted, which +// is the same section 3c remedy word_zero, word_equal and word_int_value got. +fn refused_value_out_of_range(result: WordResult) -> Bool { + match result { + WordRefused { cause: WordValueOutOfRange { width: _, value: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +fn refused_shift_amount(result: WordResult) -> Bool { + match result { + WordRefused { cause: ShiftAmountOutOfRange { width: _, amount: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn word_of_int_admits_the_top_of_the_range_holds() -> Bool { + word32_value_or(result: word_of_int(width: Width32, value: 4294967295), fallback: 0 - 1) == 4294967295 +} + +test fn word_of_int_refuses_one_past_the_range_holds() -> Bool { + match word_of_int(width: Width32, value: 4294967296) { + WordRefused { cause: WordValueOutOfRange { width: _, value: v } } => v == 4294967296 + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn word_of_int_refuses_a_negative_value_holds() -> Bool { + refused_value_out_of_range(result: word_of_int(width: Width32, value: 0 - 1)) +} + +// Width64 has no residue the Int realization can hold, so it refuses BY NAME rather than being +// absent from the width vocabulary. An operation that silently answered here would be the arm +// std.checked_arithmetic exists to prevent: the model's unbounded integer asserted about an i64. +test fn width64_refuses_as_unrealizable_holds() -> Bool { + match word_of_int(width: Width64, value: 0) { + WordRefused { cause: WordWidthUnrealizable { width: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn width8_and_width16_are_realizable_holds() -> Bool { + word32_value_or(result: word_of_int(width: Width8, value: 255), fallback: 0 - 1) == 255 + && refused_value_out_of_range(result: word_of_int(width: Width8, value: 256)) + && word32_value_or(result: word_of_int(width: Width16, value: 65535), fallback: 0 - 1) == 65535 + && refused_value_out_of_range(result: word_of_int(width: Width16, value: 65536)) +} + +// THE OPERANDS ARE TRANSCRIBED, SO THE TRANSCRIPTION IS CLAIMED RATHER THAN TRUSTED. +// +// .dag has no hexadecimal literal, so a bit-pattern operand has to be written as a ten-digit +// decimal, and that conversion is done by hand once and read by nobody afterwards. It went wrong +// here on the first cut: 0x0FF00FF0 was written 267391984, which is 0x0FF013F0, while the expected +// and/or/xor beside it had been computed from the pattern the author MEANT. The claim was false and +// the implementation was correct, which is the worse direction -- a red whose obvious reading is +// "the code is broken" and whose actual cause is the oracle. It was one digit. +// +// A comment stating the intended hex would not have caught it, because no machine reads a comment +// (DESIGN section 4c). What catches it is claiming the transcription against an operation that +// already has its own pinned vectors: a ten-digit decimal is unverifiable by eye, but the four +// octets it unpacks to are four two-or-three-digit numbers a reader can check against the hex in +// one glance. Mistype the decimal again and THIS claim reds and names the constant, instead of the +// connective claims reding and blaming the fold. +test fn bitwise_operand_transcription_holds() -> Bool { + octets_of(result: word_to_octets(a: word32_or_zero(value: 4042322160), endianness: BigEndian)) == [240, 240, 240, 240] + && octets_of(result: word_to_octets(a: word32_or_zero(value: 267390960), endianness: BigEndian)) == [15, 240, 15, 240] +} + +// THE THREE CONNECTIVES ARE THREE CLAIMS, NOT ONE CONJUNCTION. A conjunction of independent cases +// reports one verdict for three subjects: the first failing term hides the other two, and the whole +// set pays one budget. Splitting them loses no coverage and is what lets a red name its own subject. +// The narrow claims below it are the discriminators between the two ways a connective can be wrong: +// a wrong PLACE DECISION (bitwise_place_bit disagreeing with the connective) and a wrong PLACE +// ACCUMULATION (bitwise_fold assembling the decisions into the wrong number), which a claim over +// the composed operation alone cannot tell apart. +test fn bitwise_and_holds() -> Bool { + word32_value_or(result: word_and(a: word32_or_zero(value: 4042322160), b: word32_or_zero(value: 267390960)), fallback: 0 - 1) == 15728880 +} + +test fn bitwise_or_holds() -> Bool { + word32_value_or(result: word_or(a: word32_or_zero(value: 4042322160), b: word32_or_zero(value: 267390960)), fallback: 0 - 1) == 4293984240 +} + +test fn bitwise_xor_holds() -> Bool { + word32_value_or(result: word_xor(a: word32_or_zero(value: 4042322160), b: word32_or_zero(value: 267390960)), fallback: 0 - 1) == 4278255360 +} + +// Whether a wide connective REFUSES or merely answers wrongly is the discriminator between an +// accumulation that overflowed the width and a place decision that disagreed with the connective. +// A claim that only compares the value conflates them, because word32_value_or reports a refusal +// as its fallback and a fallback is indistinguishable from a wrong number. +test fn bitwise_and_answers_rather_than_refusing_holds() -> Bool { + match word_and(a: word32_or_zero(value: 4042322160), b: word32_or_zero(value: 267390960)) { + WordReady { word: _ } => true + WordRefused { cause: _ } => false + } +} + +test fn bitwise_place_decisions_hold() -> Bool { + bitwise_place_bit(op: BitAnd, x: 1, y: 1) == 1 + && bitwise_place_bit(op: BitAnd, x: 1, y: 0) == 0 + && bitwise_place_bit(op: BitOr, x: 1, y: 0) == 1 + && bitwise_place_bit(op: BitOr, x: 0, y: 0) == 0 + && bitwise_place_bit(op: BitXor, x: 1, y: 0) == 1 + && bitwise_place_bit(op: BitXor, x: 1, y: 1) == 0 +} + +test fn bitwise_fold_accumulates_places_holds() -> Bool { + bitwise_fold(op: BitXor, a: 3, b: 1, remaining: 2, place: 1, acc: 0) == 2 + && bitwise_fold(op: BitAnd, a: 3, b: 1, remaining: 2, place: 1, acc: 0) == 1 + && bitwise_fold(op: BitOr, a: 2, b: 1, remaining: 2, place: 1, acc: 0) == 3 + && bitwise_fold(op: BitXor, a: 8, b: 0, remaining: 4, place: 1, acc: 0) == 8 +} + +test fn bitwise_narrow_connectives_hold() -> Bool { + let one = word32_or_zero(value: 1) + let two = word32_or_zero(value: 2) + let three = word32_or_zero(value: 3) + word32_value_or(result: word_and(a: one, b: three), fallback: 0 - 1) == 1 + && word32_value_or(result: word_and(a: one, b: two), fallback: 0 - 1) == 0 + && word32_value_or(result: word_or(a: one, b: two), fallback: 0 - 1) == 3 + && word32_value_or(result: word_xor(a: three, b: one), fallback: 0 - 1) == 2 +} + +// The highest place a 32-bit fold reaches, isolated. The accumulation multiplies a place decision +// by a running place that doubles 32 times, so the top place is 2^31 and the running place reaches +// 2^32 after the last step -- the one value in the loop that is outside the width it is folding. +test fn bitwise_top_place_holds() -> Bool { + word32_value_or(result: word_or(a: word32_or_zero(value: 2147483648), b: word32_or_zero(value: 1)), fallback: 0 - 1) == 2147483649 + && word32_value_or(result: word_and(a: word32_or_zero(value: 2147483648), b: word32_or_zero(value: 4294967295)), fallback: 0 - 1) == 2147483648 +} + +test fn complement_of_zero_is_all_ones_holds() -> Bool { + word32_value_or(result: word_not(a: word32_or_zero(value: 0)), fallback: 0 - 1) == 4294967295 + && word32_value_or(result: word_not(a: word32_or_zero(value: 4294967295)), fallback: 0 - 1) == 0 +} + +test fn bitwise_refuses_a_width_mismatch_holds() -> Bool { + match word_and(a: word32_or_zero(value: 1), b: Word { width: Width8, value: 1 }) { + WordRefused { cause: WordWidthMismatch { left: _, right: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn shifts_hold() -> Bool { + let v = word32_or_zero(value: 305419896) + word32_value_or(result: word_shift_left(a: v, amount: 3), fallback: 0 - 1) == 2443359168 + && word32_value_or(result: word_shift_right(a: v, amount: 3), fallback: 0 - 1) == 38177487 +} + +// The left shift of a word whose high bits are set is where the obvious (value * 2^k) % modulus +// form overflows the i64 realization before any modulus is applied. 0xFFFFFFFF << 31 is that case. +test fn shift_left_at_the_top_of_the_width_holds() -> Bool { + word32_value_or(result: word_shift_left(a: word32_or_zero(value: 4294967295), amount: 31), fallback: 0 - 1) == 2147483648 +} + +test fn shift_refuses_out_of_range_amounts_holds() -> Bool { + let v = word32_or_zero(value: 1) + refused_shift_amount(result: word_shift_left(a: v, amount: 32)) + && refused_shift_amount(result: word_shift_right(a: v, amount: 32)) + && refused_shift_amount(result: word_shift_left(a: v, amount: 0 - 1)) + && refused_shift_amount(result: word_rotate_left(a: v, amount: 32)) +} + +test fn rotate_direction_is_pinned_both_ways_holds() -> Bool { + let v = word32_or_zero(value: 305419896) + word32_value_or(result: word_rotate_left(a: v, amount: 8), fallback: 0 - 1) == 878082066 + && word32_value_or(result: word_rotate_right(a: v, amount: 8), fallback: 0 - 1) == 2014458966 +} + +test fn rotate_by_zero_is_the_identity_holds() -> Bool { + let v = word32_or_zero(value: 305419896) + word32_value_or(result: word_rotate_left(a: v, amount: 0), fallback: 0 - 1) == 305419896 + && word32_value_or(result: word_rotate_right(a: v, amount: 0), fallback: 0 - 1) == 305419896 +} + +// The rotation amounts SHA-2 uses, pinned against the FIPS 180-4 definition of sigma0 evaluated on +// the algorithm's own first initial-hash word: rotr(7) xor rotr(18) xor shr(3). This is the exact +// shape CRYPTO-0 (gunbc#11628) consumes, established here so that lane inherits a pinned substrate +// rather than re-establishing it. +test fn sha2_small_sigma_zero_shape_holds() -> Bool { + let v = word32_or_zero(value: 1779033703) + match word_rotate_right(a: v, amount: 7) { + WordRefused { cause: _ } => false + WordReady { word: r7 } => + match word_rotate_right(a: v, amount: 18) { + WordRefused { cause: _ } => false + WordReady { word: r18 } => + match word_shift_right(a: v, amount: 3) { + WordRefused { cause: _ } => false + WordReady { word: s3 } => + match word_xor(a: r7, b: r18) { + WordRefused { cause: _ } => false + WordReady { word: x } => word32_value_or(result: word_xor(a: x, b: s3), fallback: 0 - 1) == 3121411458 + } + } + } + } +} + +test fn wrapping_add_reduces_modulo_the_width_holds() -> Bool { + let big = word32_or_zero(value: 4294967295) + let one = word32_or_zero(value: 1) + word32_value_or(result: word_wrapping_add(a: big, b: one), fallback: 0 - 1) == 0 + && word32_value_or(result: word_wrapping_add(a: one, b: one), fallback: 0 - 1) == 2 +} + +test fn wrapping_subtract_reduces_modulo_the_width_holds() -> Bool { + let zero = word32_or_zero(value: 0) + let one = word32_or_zero(value: 1) + word32_value_or(result: word_wrapping_subtract(a: zero, b: one), fallback: 0 - 1) == 4294967295 + && word32_value_or(result: word_wrapping_subtract(a: one, b: one), fallback: 0 - 1) == 0 +} + +// The FNV-1a 64 kernel CONTENT-HASH-0 (gunbc#11637) models runs at 64 bits, which this substrate +// refuses; the same multiplication at 32 bits is the operation it will consume once a limb carrier +// lands, and it is the case where the two 32-bit operands' product exceeds the i64 realization -- +// 0x811C9DC5 * 0x01000193 is a 56-bit product reduced to 32 bits. +test fn wrapping_multiply_exceeds_the_realization_product_holds() -> Bool { + let basis = word32_or_zero(value: 2166136261) + let prime = word32_or_zero(value: 16777619) + word32_value_or(result: word_wrapping_multiply(a: basis, b: prime), fallback: 0 - 1) == 84696351 +} + +test fn wrapping_multiply_by_one_is_the_identity_holds() -> Bool { + let v = word32_or_zero(value: 305419896) + word32_value_or(result: word_wrapping_multiply(a: v, b: word32_or_zero(value: 1)), fallback: 0 - 1) == 305419896 +} + +test fn carry_is_pinned_in_both_directions_holds() -> Bool { + match word_carrying_add(a: word32_or_zero(value: 4294967295), b: word32_or_zero(value: 1)) { + CarryingSumRefused { cause: _ } => false + CarryingSumReady { result: crossed } => + match word_carrying_add(a: word32_or_zero(value: 1), b: word32_or_zero(value: 1)) { + CarryingSumRefused { cause: _ } => false + CarryingSumReady { result: uncrossed } => + crossed.carry && crossed.sum.value == 0 && uncrossed.carry == false && uncrossed.sum.value == 2 + } + } +} + +fn octet_words(values: List) -> List { + values |> map(v => Word { width: Width8, value: v }) +} + +fn octets_of(result: OctetsResult) -> List { + match result { + OctetsReady { octets: octets } => octet_int_values(octets: octets) + OctetsRefused { cause: _ } => [] + } +} + +test fn endianness_is_pinned_both_ways_holds() -> Bool { + let octets = octet_words(values: [222, 173, 190, 239]) + word32_value_or(result: word_from_octets(width: Width32, octets: octets, endianness: BigEndian), fallback: 0 - 1) == 3735928559 + && word32_value_or(result: word_from_octets(width: Width32, octets: octets, endianness: LittleEndian), fallback: 0 - 1) == 4022250974 +} + +test fn word_to_octets_is_pinned_both_ways_holds() -> Bool { + let v = word32_or_zero(value: 3735928559) + octets_of(result: word_to_octets(a: v, endianness: BigEndian)) == [222, 173, 190, 239] + && octets_of(result: word_to_octets(a: v, endianness: LittleEndian)) == [239, 190, 173, 222] +} + +test fn octet_packing_round_trips_holds() -> Bool { + let v = word32_or_zero(value: 305419896) + match word_to_octets(a: v, endianness: BigEndian) { + OctetsRefused { cause: _ } => false + OctetsReady { octets: octets } => + word32_value_or(result: word_from_octets(width: Width32, octets: qualified_words_to_words(octets: octets), endianness: BigEndian), fallback: 0 - 1) == 305419896 + } +} + +test fn packing_refuses_the_wrong_octet_count_holds() -> Bool { + match word_from_octets(width: Width32, octets: octet_words(values: [1, 2, 3]), endianness: BigEndian) { + WordRefused { cause: OctetCountMismatch { width: _, expected: e, observed: o } } => e == 4 && o == 3 + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn packing_refuses_a_non_octet_member_holds() -> Bool { + let octets = [Word { width: Width8, value: 1 }, Word { width: Width8, value: 2 }, Word { width: Width32, value: 3 }, Word { width: Width8, value: 4 }] + match word_from_octets(width: Width32, octets: octets, endianness: BigEndian) { + WordRefused { cause: OctetWidthMismatch { observed: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +// The eight-octet big-endian length field SHA-2 padding renders. Its capacity is 2^64, which the +// Int realization cannot count to, and the refusal arm must NOT fire there: an unrepresentable +// bound is ignorance about the bound, not an answer about the value. The four-octet case is the +// same question where the capacity IS representable, so the two arms are both executed. +test fn length_field_rendering_holds() -> Bool { + octets_of(result: int_to_octets(value: 512, count: 8, endianness: BigEndian)) == [0, 0, 0, 0, 0, 0, 2, 0] + && octets_of(result: int_to_octets(value: 512, count: 4, endianness: BigEndian)) == [0, 0, 2, 0] + && octets_of(result: int_to_octets(value: 512, count: 4, endianness: LittleEndian)) == [0, 2, 0, 0] +} + +test fn length_field_refuses_a_value_past_its_capacity_holds() -> Bool { + match int_to_octets(value: 256, count: 1, endianness: BigEndian) { + OctetsRefused { cause: IntegerDoesNotFitOctets { value: v, octets: c } } => v == 256 && c == 1 + OctetsRefused { cause: _ } => false + OctetsReady { octets: _ } => false + } +} + +// THE BYPASS DISCRIMINATOR FOR THE SWITCHED CONSUMER, and why it is a refusal rather than an +// output comparison. std.encoding's base64 now routes its packing through this substrate, and on +// every VALID input the substrate route and the magic-literal route it replaced agree byte for +// byte -- that agreement is the receipt, and it is exactly why output equality cannot discriminate +// between them. They disagree on one thing: an octet outside the byte range. The literal route +// computed x * 65536 + y * 256 + z on it and produced a plausible wrong string with no error; the +// substrate route refuses at word_of_int because the width is a fact the value has to establish. +// So re-introducing the displaced arithmetic turns this Absent into a Present and reds the claim. +test fn base64_encode_refuses_an_out_of_range_octet_holds() -> Bool { + match base64_encode(octets: [256, 0, 0], variant: Standard) { + Absent => true + Present { value: _ } => false + } +} + +test fn base64_encode_still_admits_the_byte_range_holds() -> Bool { + match base64_encode(octets: [255, 0, 255], variant: Standard) { + Absent => false + Present { value: s } => s == "/wD/" + } +} + +// THE MODULUS TABLE IS MATERIALISED, SO ITS AGREEMENT WITH THE AUTHORITY IS EXECUTED. +// +// word_modulus answers from the closed four-member width set instead of walking int_pow_bounded on +// every operation. The objection to a literal table is that a second representation of a derived +// constant goes stale silently -- so this claim removes the silence: std.induction int_pow_bounded +// stays the authority for what 2^bits IS, and every member of the closed set is run against it +// here, INCLUDING Width64, where both must answer with nothing. A wrong number in the table reds +// this rather than waiting to be found by a consumer, and the Width64 arm is what stops the table +// from quietly gaining a value the carrier cannot hold. +fn modulus_agrees_at(w: WordWidth) -> Bool { + match word_modulus(w: w) { + Present { value: m } => + match int_pow_bounded(base: 2, exp: word_width_bits(w: w)) { + Present { value: derived } => m == derived + Absent => false + } + Absent => + match int_pow_bounded(base: 2, exp: word_width_bits(w: w)) { + Present { value: _ } => false + Absent => true + } + } +} + +test fn word_modulus_agrees_with_the_power_authority_holds() -> Bool { + modulus_agrees_at(w: Width8) + && modulus_agrees_at(w: Width16) + && modulus_agrees_at(w: Width32) + && modulus_agrees_at(w: Width64) +} + +// THE FRONTIER ROWS ARE READ, NOT MERELY DECLARED. A frontier row that nothing executes is the +// same dangling declaration it exists to excuse, one level up. These two claims are its consumer: +// the first establishes that every row names a declaration in the module that owns it, so a row +// cannot drift onto somebody else's surface; the second is an IDENTITY JOIN against the expected +// key set rather than a count, because a count agrees while membership differs. +fn frontier_subject_key(row: FrontierRow) -> String { + match row.subject { + DeclSubject { ref: r } => concat(r.module_path as String, concat(".", r.decl_name as String)) + PathSubject { path: p } => p + } +} + +test fn machine_word_frontier_rows_name_this_module_holds() -> Bool { + machine_word_consumer_frontier_rows |> all(row => + match row.subject { + DeclSubject { ref: r } => (r.module_path as String) == "std.machine_word" + PathSubject { path: _ } => false + }) +} + +test fn machine_word_frontier_covers_the_awaited_operations_holds() -> Bool { + let keys = machine_word_consumer_frontier_rows |> map(row => frontier_subject_key(row: row)) + let expected = [ + "std.machine_word.word_wrapping_add", + "std.machine_word.word_rotate_right", + "std.machine_word.word_xor", + "std.machine_word.word_not", + "std.machine_word.word_wrapping_multiply", + "std.machine_word.word_wrapping_subtract", + "std.machine_word.word_carrying_add" + ] + expected |> all(e => keys |> any(k => k == e)) + && keys |> all(k => expected |> any(e => e == k)) +} + +// THE SAME AGREEMENT CHECK FOR THE OTHER TWO CLOSED-SET CONSTANTS. Review 68053 named the modulus; +// the defect is the class, so the split point and the octet radix are derived once for the same +// reason and are checked the same way. The octet radix needs no agreement claim against +// int_pow_bounded because it introduces NO constant -- it reads the Width8 modulus, which is +// already checked -- so what is claimed here is the identity itself, which is the thing that would +// break if either side moved. +fn half_radix_agrees_at(w: WordWidth) -> Bool { + match word_half_radix(w: w) { + Present { value: h } => + match int_pow_bounded(base: 2, exp: word_width_bits(w: w) / 2) { + Present { value: derived } => h == derived + Absent => false + } + Absent => + match int_pow_bounded(base: 2, exp: word_width_bits(w: w) / 2) { + Present { value: _ } => false + Absent => true + } + } +} + +test fn word_half_radix_agrees_with_the_power_authority_holds() -> Bool { + half_radix_agrees_at(w: Width8) + && half_radix_agrees_at(w: Width16) + && half_radix_agrees_at(w: Width32) +} + +// Width64's half is 2^32, which IS representable, so the power authority answers where this module +// must not: a Width64 word has no residue the carrier can hold, and handing back a split point for +// one would be answering a question whose subject does not exist. The two therefore disagree here +// BY CONSTRUCTION, and that disagreement is claimed rather than left to look like an oversight. +test fn word_half_radix_refuses_width64_although_the_power_exists_holds() -> Bool { + match word_half_radix(w: Width64) { + Present { value: _ } => false + Absent => + match int_pow_bounded(base: 2, exp: 32) { + Present { value: p } => p == 4294967296 + Absent => false + } + } +} + +test fn octet_radix_is_the_width8_modulus_holds() -> Bool { + match octet_radix() { + Absent => false + Present { value: r } => + match word_modulus(w: Width8) { + Absent => false + Present { value: m } => r == m && r == 256 + } + } +} + +// ENROLMENT IS A DIFFERENT FACT FROM DECLARATION, AND ONLY THIS CLAIM ESTABLISHES IT. +// +// The two claims above assert that the frontier rows name this module and that their key set is the +// expected one -- that the DECLARATIONS exist. Neither touches whether anything folds them, and a +// roster nothing folds computes no expiry: when extdeps.crypto.sha2 sha256_add_all lands, a row +// outside the census is never reported as fired-still-present, so the trigger that is supposed to +// retire it cannot fire (review 68088). That is the inert-lens tier DESIGN section 6 names, and the +// first cut of this roster sat in it while asserting the opposite in prose. +// +// So this claim joins the rows against the census closure ITSELF rather than against a restatement +// of it, by subject key rather than by count -- a count agrees while membership differs. Dropping +// machine_word_consumer_frontier_rows from gunbc.census_closure_frontier +// census_closure_frontier_row_groups reds it, which is the mutation it exists to catch. +test fn machine_word_frontier_rows_are_enrolled_in_the_census_holds() -> Bool { + let census_keys = census_closure_frontier_rows() |> map(row => frontier_subject_key(row: row)) + machine_word_consumer_frontier_rows |> all(row => + census_keys |> any(k => k == frontier_subject_key(row: row))) +} + +// THE WIDTH64 ARMS OF THE PACKING OPERATIONS, WHICH HAD NO WITNESS AT ALL. +// +// Every other operation's Width64 refusal was claimed through word_of_int; the two packing entries +// were not, and word_from_octets was the one that computed before it refused -- eight octets +// accumulated to as much as 2^64 - 1 in the i64 the realization uses, and the refusal then +// inspected whatever that had become (review 68118). An unwitnessed arm is why that stood: nothing +// reds on a path no claim runs. These pin both directions of the packing boundary, and the +// from_octets arm is RED against the pre-fix code rather than merely green against the new code, +// because it is supplied the exact eight-octet input that made the accumulator overflow. +test fn packing_refuses_width64_before_accumulating_holds() -> Bool { + let all_ones = octet_words(values: [255, 255, 255, 255, 255, 255, 255, 255]) + match word_from_octets(width: Width64, octets: all_ones, endianness: BigEndian) { + WordRefused { cause: WordWidthUnrealizable { width: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +// A width that cannot exist is refused as such, not as a count disagreement -- the wider fact wins, +// and this claim is what keeps the refusal ORDER from silently inverting. +test fn packing_refuses_width64_ahead_of_the_count_check_holds() -> Bool { + match word_from_octets(width: Width64, octets: octet_words(values: [1, 2, 3]), endianness: BigEndian) { + WordRefused { cause: WordWidthUnrealizable { width: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn word_to_octets_refuses_width64_holds() -> Bool { + match word_to_octets(a: Word { width: Width64, value: 0 }, endianness: BigEndian) { + OctetsRefused { cause: WordWidthUnrealizable { width: _ } } => true + OctetsRefused { cause: _ } => false + OctetsReady { octets: _ } => false + } +} + +// THE PREMISE CONTROLS. Word is an ordinary record and .dag has no module-private construction, so +// a caller can write a word its own type says cannot exist. These supply exactly that and require a +// refusal naming the VALUE -- each is red against the pre-fix code, where the operation computed +// from the bad operand and answered successfully because its OUTPUT happened to land in range. +fn unqualified_width8_256() -> Word { + Word { width: Width8, value: 256 } +} + +test fn shift_refuses_an_unqualified_operand_holds() -> Bool { + match word_shift_right(a: unqualified_width8_256(), amount: 1) { + WordRefused { cause: WordValueOutOfRange { width: _, value: v } } => v == 256 + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +// One control per exported family, because the premise check is per-boundary: a repair applied to +// some entries and not others is exactly the state the first cut was in. +test fn every_exported_family_refuses_an_unqualified_operand_holds() -> Bool { + let bad = unqualified_width8_256() + let good = match word_of_int(width: Width8, value: 1) { + WordReady { word: w } => w + WordRefused { cause: _ } => Word { width: Width8, value: 0 } + } + refused_value_out_of_range(result: word_and(a: bad, b: good)) + && refused_value_out_of_range(result: word_or(a: good, b: bad)) + && refused_value_out_of_range(result: word_xor(a: bad, b: good)) + && refused_value_out_of_range(result: word_not(a: bad)) + && refused_value_out_of_range(result: word_shift_left(a: bad, amount: 1)) + && refused_value_out_of_range(result: word_rotate_left(a: bad, amount: 1)) + && refused_value_out_of_range(result: word_rotate_right(a: bad, amount: 1)) + && refused_value_out_of_range(result: word_wrapping_add(a: bad, b: good)) + && refused_value_out_of_range(result: word_wrapping_subtract(a: bad, b: good)) + && refused_value_out_of_range(result: word_wrapping_multiply(a: bad, b: good)) +} + +test fn carrying_add_refuses_an_unqualified_operand_holds() -> Bool { + match word_carrying_add(a: unqualified_width8_256(), b: unqualified_width8_256()) { + CarryingSumRefused { cause: WordValueOutOfRange { width: _, value: _ } } => true + CarryingSumRefused { cause: _ } => false + CarryingSumReady { result: _ } => false + } +} + +test fn to_octets_refuses_an_unqualified_operand_holds() -> Bool { + match word_to_octets(a: unqualified_width8_256(), endianness: BigEndian) { + OctetsRefused { cause: WordValueOutOfRange { width: _, value: _ } } => true + OctetsRefused { cause: _ } => false + OctetsReady { octets: _ } => false + } +} + +// The packing counterexample: both members have the right WIDTH and one has an impossible VALUE, +// and the packed result (512) is in range for Width16, so nothing downstream would have fired. +test fn packing_refuses_an_unqualified_member_holds() -> Bool { + let members = [Word { width: Width8, value: 1 }, Word { width: Width8, value: 256 }] + match word_from_octets(width: Width16, octets: members, endianness: BigEndian) { + WordRefused { cause: WordValueOutOfRange { width: _, value: v } } => v == 256 + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +// THE OCTET-COUNT TRIPLE. A negative count is not a small capacity, and reading it as one returned +// a successful empty rendering. The three cases together are what separate "refused as nonsense" +// from "rendered nothing because nothing fits" from "rendered nothing because nothing was asked". +test fn negative_octet_count_refuses_holds() -> Bool { + match int_to_octets(value: 0, count: 0 - 1, endianness: BigEndian) { + OctetsRefused { cause: OctetCountOutOfRange { observed: n } } => n == (0 - 1) + OctetsRefused { cause: _ } => false + OctetsReady { octets: _ } => false + } +} + +test fn zero_octet_count_renders_nothing_for_zero_holds() -> Bool { + match int_to_octets(value: 0, count: 0, endianness: BigEndian) { + OctetsReady { octets: o } => list_length(items: o) == 0 + OctetsRefused { cause: _ } => false + } +} + +test fn zero_octet_count_refuses_a_nonzero_value_holds() -> Bool { + match int_to_octets(value: 1, count: 0, endianness: BigEndian) { + OctetsRefused { cause: IntegerDoesNotFitOctets { value: v, octets: c } } => v == 1 && c == 0 + OctetsRefused { cause: _ } => false + OctetsReady { octets: _ } => false + } +} + +// THE REFUSAL ORDER, pinned so the four shift and rotate arms cannot drift apart again. A width +// that cannot exist is the wider fact; naming the amount instead answers a narrower question. +test fn rotate_right_refuses_width_before_amount_holds() -> Bool { + match word_rotate_right(a: Word { width: Width64, value: 0 }, amount: 64) { + WordRefused { cause: WordWidthUnrealizable { width: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn all_shift_and_rotate_arms_agree_on_refusal_order_holds() -> Bool { + let w64 = Word { width: Width64, value: 0 } + word_refuses_unrealizable(result: word_shift_left(a: w64, amount: 64)) + && word_refuses_unrealizable(result: word_shift_right(a: w64, amount: 64)) + && word_refuses_unrealizable(result: word_rotate_left(a: w64, amount: 64)) + && word_refuses_unrealizable(result: word_rotate_right(a: w64, amount: 64)) +} + +fn word_refuses_unrealizable(result: WordResult) -> Bool { + match result { + WordRefused { cause: WordWidthUnrealizable { width: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +// THE PROJECTION IS A BOUNDARY TOO. octet_int_values read o.value off every member without +// establishing any of them and had no refusal arm to report one -- [Word{Width8,256}] projected to +// [256], and std.encoding consumed that projection on the base64 decode route. Reading a field is +// where an uninhabitable word stops being a record and becomes a number a consumer will trust. +test fn octet_projection_refuses_an_unqualified_member_holds() -> Bool { + match word_from_octets(width: Width8, octets: [Word { width: Width8, value: 256 }], endianness: BigEndian) { + WordRefused { cause: WordValueOutOfRange { width: _, value: v } } => v == 256 + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn octet_projection_refuses_a_non_octet_member_holds() -> Bool { + match word_from_octets(width: Width8, octets: [Word { width: Width32, value: 1 }], endianness: BigEndian) { + WordRefused { cause: OctetWidthMismatch { observed: _ } } => true + WordRefused { cause: _ } => false + WordReady { word: _ } => false + } +} + +test fn octet_projection_passes_qualified_members_holds() -> Bool { + octets_of(result: word_to_octets(a: word32_or_zero(value: 255), endianness: BigEndian)) == [0, 0, 0, 255] +} diff --git a/dag/test/claim/random_bytes_csprng_witness_test.dag b/dag/test/claim/random_bytes_csprng_witness_test.dag index ff5a0c4cd6e..96c92a668fa 100644 --- a/dag/test/claim/random_bytes_csprng_witness_test.dag +++ b/dag/test/claim/random_bytes_csprng_witness_test.dag @@ -12,7 +12,10 @@ fn getrandom_octets(count: Int) -> List? { pattern mint_base64url_credential(byte_count: Int) -> { credential: String } { node cred = match getrandom_octets(count: byte_count) { - Present { value: bs } => base64_encode(octets: bs, variant: UrlSafe) + Present { value: bs } => match base64_encode(octets: bs, variant: UrlSafe) { + Present { value: encoded } => encoded + Absent => "" + } Absent => "" } return { credential: cred } diff --git a/docs/plans/blackjack-onboarding.md b/docs/plans/blackjack-onboarding.md index d33b3b8f8ee..f302abbed29 100644 --- a/docs/plans/blackjack-onboarding.md +++ b/docs/plans/blackjack-onboarding.md @@ -231,7 +231,7 @@ Anchor in the file: `ShuffleSeed`. Two pure functions and nothing else: a seed-t module examples.blackjack.shuffle import std.integer { UInt8 } -import std.encoding { base64_octet_int } +import std.encoding { base64_octet_word } import examples.blackjack.cards { Card } import examples.blackjack.round { Shoe } @@ -246,8 +246,9 @@ fn shuffle(deck: List, seed: ShuffleSeed) -> Shoe { … } fn next_seed(seed: ShuffleSeed) -> ShuffleSeed { … } // The bridge from the entropy boundary. The octets arrive as the List that -// std.encoding.base64_decode returns; base64_octet_int (same module) reads each one as an -// Int, and a fold combines them. Take the real decoded type here -- do not mint an Int list. +// std.encoding.base64_decode returns; base64_octet_word (same module) ADMITS each one through +// word_of_int at Width8, so an octet outside the byte range refuses rather than being renamed, +// and a fold combines them. Take the real decoded type here -- do not mint an Int list. fn seed_from_octets(octets: List) -> ShuffleSeed { … } ``` @@ -339,7 +340,7 @@ Four levels, and you will use all four. The question to ask before writing any t 1. **Pure unit tests** supply cards, hands and values directly. Most of your tests. 2. **State-transition tests** supply a complete `RoundState` and an action, and assert the exact next state or the exact refusal. One test per refusal arm. -3. **Boundary tests** supply the value an effectful producer *would* return — a `List` of octets (built with `std.encoding` `base64_octet_of_int`, the same constructor the decoder uses) handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer. +3. **Boundary tests** supply the value an effectful producer *would* return — a `List` of octets written directly, which is exactly the type `std.encoding` `base64_decode` returns, handed to `seed_from_octets`, a `ShuffleSeed` handed to `shuffle` — without calling the producer. 4. **One integration test** calls the real producer, `Urandom.ReadBytes`, and establishes only that its output inhabits the shape the boundary tests assumed (the right number of octets, decodable). It does not assert that a random shoe has any particular order. Level 3 without level 4 is the trap DESIGN §3 names: a suite that is fast, green, and proves no program, because every boundary was supplied and none was ever executed. Level 4 is what turns your supplied inputs from hypotheses into readings. Keep it to one test, keep it narrow, and know that it is *wet* — it shells out — so it runs with `--wet` locally and is the one that can fail for reasons that are not yours. @@ -350,7 +351,7 @@ Every test you write must be one you can make go **red** by breaking the code it ## 6. The randomness boundary -Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and reads each octet with `base64_octet_int` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes. +Only after deterministic rounds run from hand-ordered shoes do you connect entropy — and even then, the connection is one function call in one test. `dag/test/claim/random_bytes_csprng_witness_test.dag` is the in-tree exemplar: it calls `Urandom.ReadBytes(count: 16).octets_b64`, base64-decodes it with `std.encoding` `base64_decode` to `List?`, and asserts the count. Your integration test does the same, matches the `Present` arm (the `Absent` arm is a refusal of the test, not a skip), hands that `List` to `seed_from_octets` unchanged — it takes the decoder's type, and admits each octet with `base64_octet_word` — then `shuffle`, and asserts that the result is a 52-card shoe containing each card exactly once. That last assertion is a property of `shuffle`, not of the entropy; it is here because it is the one place the whole route executes. The seed is the replay handle. Every `SimulatedRound` carries the seed its shoe was built from, so a surprising row in a 10,000-round simulation is reproduced by one call to `play_round` with that seed — no reruns, no logging, no luck.