diff --git a/Cargo.lock b/Cargo.lock index 887507694ec..04becd66dc8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -189,7 +189,6 @@ checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" dependencies = [ "block-buffer", "crypto-common", - "subtle", ] [[package]] @@ -273,15 +272,6 @@ version = "0.4.3" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" -[[package]] -name = "hmac" -version = "0.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6c49c37c09c17a53d937dfbb742eb3a961d65a994e6bcdcf37e7399d0cc8ab5e" -dependencies = [ - "digest", -] - [[package]] name = "icu_collections" version = "2.2.0" @@ -857,7 +847,6 @@ version = "0.1.0" dependencies = [ "clap", "hex", - "hmac", "im", "lazy_static", "libc", diff --git a/Cargo.toml b/Cargo.toml index 692be250c34..4921245f578 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -44,7 +44,6 @@ sha2 = "0.10" # repo-wide crypto upgrade. RustCrypto provides Hmac together with verify_slice, which # compares in constant time -- the operation gunbc.auth.approval_capability requires and the reason # no accessor in extdeps.crypto.mac yields a computed tag for a caller to compare itself. -hmac = "0.12" hex = "0.4" glob = "0.3" ureq = "2" diff --git a/dag/extdeps/cloud/gcp/secret_manager.dag b/dag/extdeps/cloud/gcp/secret_manager.dag index 5b660d95f61..4a1809cfe4f 100644 --- a/dag/extdeps/cloud/gcp/secret_manager.dag +++ b/dag/extdeps/cloud/gcp/secret_manager.dag @@ -1,7 +1,8 @@ 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.machine_word { QualifiedOctetsReady, QualifiedOctetsRefused } +import std.encoding { Standard, base64_decode, base64_encode, base64_octets, utf8_decode_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 +200,22 @@ 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( - octets: bytes_octets(b: utf8_encode_bytes(s: credential as String)), - variant: Standard - ) + match base64_octets(values: bytes_octets(b: utf8_encode_bytes(s: credential as String))) { + QualifiedOctetsReady { octets: qualified } => base64_encode(octets: qualified, variant: Standard) + QualifiedOctetsRefused { cause: _ } => pure_dag_seam_unreachable_string() + } } fn decode_sm_access_version_payload_wire(data_b64: String) -> SmAccessVersionPayloadDecodeOutcome { diff --git a/dag/extdeps/crypto/mac.dag b/dag/extdeps/crypto/mac.dag index 16ae34af8b6..6c58fbb52af 100644 --- a/dag/extdeps/crypto/mac.dag +++ b/dag/extdeps/crypto/mac.dag @@ -4,11 +4,20 @@ import std.types { NonEmptyStr, String, Secret, Int } import std.logic { Bool } import std.measure { ByteSize, byte_size, byte_size_count } +import std.error_primitives { Result, Ok, Err } +import std.integer { UInt8 } +import std.machine_word { + Word, Width8, WordResult, WordReady, WordRefused, WordRefusal, + word_of_int, word_xor, word_or, +} +import std.encoding { Utf8EncodeRefusal, utf8_encode_octets } +import extdeps.numeric.base16 { base16_decode_lower, base16_encode_lower } +import extdeps.crypto.sha2 { Sha256Refusal, sha256_octets, sha256_block_octets, sha256_digest_octets } import extdeps.external_authority { ExternalAuthority } import extdeps.uri { Uri, Https } -// HMAC per RFC 2104, keyed-hashing for message authentication. The anchor is the specification and -// not the crate, because the crate is one realization of it and this module owns the SHAPE. +// HMAC per RFC 2104, keyed-hashing for message authentication. The anchor is the specification: +// this module owns the SHAPE and, since CRYPTO-0 (gunbc#11628), the computation as well. data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { uri: Uri { scheme: Https @@ -16,18 +25,19 @@ data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { } } -// THIS MODULE DOES NOT COMPUTE ANYTHING, AND THAT IS THE POINT. +// THIS MODULE COMPUTES HMAC IN .dag, AND WHAT IT STILL REFUSES TO HAND OUT. // -// A MAC is the one primitive where authoring the algorithm is the failure. DESIGN §5 already says -// the substrate should carry structure rather than re-coin it, and the standing instruction on this -// work was explicit: bind an ESTABLISHED implementation, never invent a construction. So what lives -// here is the interface, the algorithm identity, the key identity, and the refusal vocabulary -- -// the facts a caller must state. The bytes are produced by extdeps.rust.crate_hmac's realization. +// An earlier revision computed nothing here and bound RustCrypto's Hmac through two v1 +// interpreter primitives, on the reasoning that authoring a MAC is the failure. The operator ruling +// behind PRIMITIVE-EGRESS-0 (gunbc#11626) reverses that for pure computation: an algorithm the +// substrate can express is MODELED, and a host library is at most an independent test oracle. +// Authoring is not inventing -- this is RFC 2104 §2 transcribed over the FIPS 180-4 SHA-256 in +// extdeps.crypto.sha2, and it is held to the RFC 4231 vectors, not to the crate it replaced. // -// The neighbouring module extdeps.crypto.hash models SHA-256 as a DIGEST VALUE and verifies through -// a shelled sha256sum; it deliberately does not produce one either. This is the same boundary drawn -// one step further out: a Digest is a fact you can carry, a MAC is a fact you can only check. -data mac_is_interface_only_note: NonEmptyStr = "extdeps.crypto.mac declares the MAC contract and never implements it. Verification is performed by the bound realization's constant-time comparison, which is the operation RFC 2104 §6 and every established implementation expose for this purpose; a caller that extracts tag bytes and compares them with ordinary equality has reintroduced the timing oracle the library exists to close, so no accessor here yields the computed tag." +// What survives from the old boundary is the part that was never about who computes: no function +// here returns the tag computed during VERIFICATION, so no caller can compare one with an ordinary +// early-exit equality. mac_verify compares inside this module, over every octet, with no early exit. +data mac_is_interface_only_note: NonEmptyStr = "extdeps.crypto.mac computes HMAC-SHA-256 in .dag and still yields no verification-side tag: mac_verify compares the computed and presented tags itself, accumulating the XOR of every octet pair before deciding, so the work does not depend on where the first difference is. That full-scan shape is the modeled half of constant-time comparison; a realization must preserve it (no short-circuit), which is a realization obligation this module cannot observe." // ONE FIXED SUITE, NAMED. An algorithm field that a message can choose is the algorithm-confusion // hole: the verifier must decide the suite from its own configuration, never from the input it is @@ -36,7 +46,7 @@ data mac_is_interface_only_note: NonEmptyStr = "extdeps.crypto.mac declares the type MacSuite = | HmacSha256 -data hmac_sha256_authority_note: NonEmptyStr = "HMAC-SHA-256: HMAC (RFC 2104) instantiated with SHA-256 (FIPS 180-4, cited by extdeps.crypto.hash). The tag is 32 octets. RustCrypto's `hmac` crate provides this as Hmac together with verify_slice, which performs the comparison in constant time." +data hmac_sha256_authority_note: NonEmptyStr = "HMAC-SHA-256: HMAC (RFC 2104) instantiated with SHA-256 (FIPS 180-4, cited by extdeps.crypto.hash). The tag is 32 octets. Computed by hmac_sha256_octets below over extdeps.crypto.sha2; no host library is on this route." fn mac_suite_name(s: MacSuite) -> NonEmptyStr { match s { @@ -93,8 +103,8 @@ data symmetric_verification_is_issuance_note: NonEmptyStr = "With HMAC the verif // MacKeys lives inside the broker. // // This does NOT reopen the timing oracle mac_is_interface_only_note closes. That note is about a -// VERIFIER comparing a computed tag itself; mac_verify still hands its comparison to the bound -// implementation and still yields no tag. A MacTag is what an issuer transmits, and nothing in this +// VERIFIER comparing a computed tag itself; mac_verify still performs its comparison internally +// and still yields no tag. A MacTag is what an issuer transmits, and nothing in this // module compares one. // // The tag names the key and suite it was produced under so an issuer cannot place it in an envelope @@ -106,22 +116,153 @@ type MacTag { hex: NonEmptyStr } -// Issuance refuses rather than fabricating. The only malformed input the bound implementation can -// see is key material that is not hex -- there is then no key, so there is no tag to report. +// Issuance refuses rather than fabricating. Key material that is not hex means there is no key, so +// there is no tag to report. MacComputationRefused carries the located cause of any other refusal +// of the computation -- a message with no UTF-8 encoding, or a substrate refusal inside SHA-256 -- +// none of which a well-formed call reaches, and each of which is a defect worth naming. type MacSigning = MacSigned { tag: MacTag } | MacKeyMaterialNotHex { key_id: MacKeyId } + | MacComputationRefused { key_id: MacKeyId, cause: HmacRefusal } + +// ── HMAC-SHA-256, RFC 2104 §2 ──────────────────────────────────────────────────────────────── +// HMAC(K, m) = H((K0 ⊕ opad) ‖ H((K0 ⊕ ipad) ‖ m)), with B and L read from extdeps.crypto.sha2. +// K0 is K zero-padded to B octets, or H(K) zero-padded when K is longer than B (§2 step 1; the +// RFC 4231 §4.7 vector exercises that arm). ipad is 0x36 (54) and opad 0x5c (92) repeated B times; +// each octet XOR is a std.machine_word operation at Width8. +type HmacRefusal + = HmacKeyNotHex + | HmacMessageNotEncodable { cause: Utf8EncodeRefusal } + | HmacDigestRefused { cause: Sha256Refusal } + | HmacOctetRefused { cause: WordRefusal } + +data hmac_inner_pad_octet: Int = 54 +data hmac_outer_pad_octet: Int = 92 + +fn hmac_zero_extend(octets: List, count: Int) -> List { + if list_length(items: octets) >= count { octets } else { hmac_zero_extend(octets: octets |> list_push(0), count: count) } +} + +fn hmac_block_key(key: List) -> Result, HmacRefusal> { + if list_length(items: key) > sha256_block_octets() { + match sha256_octets(message: key) { + Err { value: e } => Err { value: HmacDigestRefused { cause: e } } + Ok { value: hk } => Ok { value: hmac_zero_extend(octets: hk, count: sha256_block_octets()) } + } + } else { + Ok { value: hmac_zero_extend(octets: key, count: sha256_block_octets()) } + } +} + +fn hmac_octet_word(o: Int) -> Result { + match word_of_int(width: Width8, value: o) { + WordReady { word: w } => Ok { value: w } + WordRefused { cause: c } => Err { value: HmacOctetRefused { cause: c } } + } +} + +fn hmac_xor_pad(key: List, pad: Word, acc: List) -> Result, HmacRefusal> { + match key.first() { + Absent => Ok { value: acc } + Present { value: k } => + match hmac_octet_word(o: k) { + Err { value: e } => Err { value: e } + Ok { value: kw } => + match word_xor(a: kw, b: pad) { + WordRefused { cause: c } => Err { value: HmacOctetRefused { cause: c } } + WordReady { word: x } => hmac_xor_pad(key: key.skip(n: 1), pad: pad, acc: acc |> list_push(x.value)) + } + } + } +} -// `hmac_sha256_hex` is the issuing twin of hmac_sha256_verify_hex: the same RustCrypto Hmac, -// the same hex key spelling, absent (never a tag) on a non-hex key. The suite match is total so a -// second MacSuite arm cannot be signed by the HMAC-SHA-256 implementation without an authored arm. +fn hmac_sha256_octets(key: List, message: List) -> Result, HmacRefusal> { + match hmac_block_key(key: key) { + Err { value: e } => Err { value: e } + Ok { value: k0 } => + match hmac_octet_word(o: hmac_inner_pad_octet) { + Err { value: e } => Err { value: e } + Ok { value: ipad } => + match hmac_octet_word(o: hmac_outer_pad_octet) { + Err { value: e } => Err { value: e } + Ok { value: opad } => + match hmac_xor_pad(key: k0, pad: ipad, acc: []) { + Err { value: e } => Err { value: e } + Ok { value: inner_key } => + match hmac_xor_pad(key: k0, pad: opad, acc: []) { + Err { value: e } => Err { value: e } + Ok { value: outer_key } => + match sha256_octets(message: concat(inner_key, message)) { + Err { value: e } => Err { value: HmacDigestRefused { cause: e } } + Ok { value: inner } => + match sha256_octets(message: concat(outer_key, inner)) { + Err { value: e } => Err { value: HmacDigestRefused { cause: e } } + Ok { value: tag } => Ok { value: tag } + } + } + } + } + } + } + } +} + +// The corpus's spelling of a MAC call: key material as lowercase hex (the keyring's form), the +// message as a String taken as its UTF-8 octets. A key that is not lowercase hex refuses; it is +// never reinterpreted as text. Issuance and verification both go through here, so the two cannot +// disagree about the key spelling or the message octets. +fn hmac_sha256_of_hex_key(key_hex: String, message: String) -> Result, HmacRefusal> { + match base16_decode_lower(hex: key_hex) { + Absent => Err { value: HmacKeyNotHex } + Present { value: key } => + match utf8_encode_octets(s: message) { + Err { value: e } => Err { value: HmacMessageNotEncodable { cause: e } } + Ok { value: m } => hmac_sha256_octets(key: key, message: m) + } + } +} + +// FULL-SCAN TAG COMPARISON. The OR of the XOR of every octet pair is accumulated before anything is +// decided, so the work is the same whether the tags differ in the first octet or the last -- the +// modeled half of constant-time comparison. Lengths are checked before this, in the open: a tag's +// length is the suite's public L. +fn hmac_tag_difference(a: List, b: List, acc: Word) -> Result { + match a.first() { + Absent => Ok { value: acc } + Present { value: x } => + match b.first() { + Absent => Ok { value: acc } + Present { value: y } => + match hmac_octet_word(o: x) { + Err { value: e } => Err { value: e } + Ok { value: xw } => + match hmac_octet_word(o: y) { + Err { value: e } => Err { value: e } + Ok { value: yw } => + match word_xor(a: xw, b: yw) { + WordRefused { cause: c } => Err { value: HmacOctetRefused { cause: c } } + WordReady { word: d } => + match word_or(a: acc, b: d) { + WordRefused { cause: c } => Err { value: HmacOctetRefused { cause: c } } + WordReady { word: next } => hmac_tag_difference(a: a.skip(n: 1), b: b.skip(n: 1), acc: next) + } + } + } + } + } + } +} + +// The suite match is total so a second MacSuite arm cannot be signed by the HMAC-SHA-256 +// computation without an authored arm. fn mac_sign(key: MacKey, message: NonEmptyStr) -> MacSigning { match key.suite { HmacSha256 => - match hmac_sha256_hex(key.material as String, message as String) { - Absent => MacKeyMaterialNotHex { key_id: key.id } - Present { value: hex } => - MacSigned { tag: MacTag { key_id: key.id, suite: key.suite, hex: hex as NonEmptyStr } } + match hmac_sha256_of_hex_key(key_hex: key.material as String, message: message as String) { + Err { value: HmacKeyNotHex } => MacKeyMaterialNotHex { key_id: key.id } + Err { value: e } => MacComputationRefused { key_id: key.id, cause: e } + Ok { value: tag } => + MacSigned { tag: MacTag { key_id: key.id, suite: key.suite, hex: base16_encode_lower(octets: tag) as NonEmptyStr } } } } } @@ -159,12 +300,15 @@ type MacVerification | MacKeyRetired { key_id: MacKeyId, retired_at: NonEmptyStr } | MacSuiteMismatch { expected: MacSuite, key_suite: MacSuite } | MacTagMalformed { octets_declared: Int, octets_expected: Int } + | MacTagNotHex { key_id: MacKeyId } + | MacKeyMaterialMalformed { key_id: MacKeyId } + | MacVerificationRefused { key_id: MacKeyId, cause: HmacRefusal } // ── The realization seam ───────────────────────────────────────────────────────────────────── // VerifiedMessage is sole_constructor, so nothing outside this module can mint one -- which is the // point, and which also means this module must expose the ONE way evidence comes into existence. -// This is it: the bound implementation performs the constant-time comparison over (key, message, -// tag) and reports its verdict here, and the evidence is assembled around THE MESSAGE IT WAS GIVEN. +// This is it: mac_verify performs the full-scan comparison over (key, message, tag) and reports its +// verdict here, and the evidence is assembled around THE MESSAGE IT WAS GIVEN. // // What that makes structural, and what it does not: // @@ -172,11 +316,11 @@ type MacVerification // MacVerified and then decide what it authenticated, because the message is a parameter of the // only constructor. That is the substitution this seam closes. // -// NOT structural -- that the implementation actually ran HMAC over those bytes. A caller passing -// `true` here is asserting the comparison succeeded, and this module cannot check that. The -// realization is the trusted party for that half, exactly as it is for any host effect, and it -// is why this function is named for the boundary it sits on rather than being spelled as an -// ordinary constructor a caller might reach for casually. +// NOT structural -- that HMAC actually ran over those bytes. A caller passing `true` here is +// asserting the comparison succeeded, and this function cannot check that. mac_verify is the +// production caller; the others are witnesses supplying a verdict at this boundary (DESIGN §3, +// a witness discriminates at one interface), paired with the round-trip witness that runs +// mac_verify for real. // // A verdict of false becomes MacTagMismatch rather than a bare absence, because "the tag did not // verify" is the incident worth naming. @@ -195,44 +339,53 @@ fn mac_verification_from_implementation( } } -// ── The bound implementation ───────────────────────────────────────────────────────────────── -// THE ONE FUNCTION THAT ACTUALLY VERIFIES, and it is where this module stops being an interface. -// `hmac_sha256_verify_hex` is a host primitive backed by RustCrypto's Hmac and its -// `verify_slice`, which compares in CONSTANT TIME. That is not an optimization detail: an ordinary -// equality over MAC bytes leaks, through timing, how many leading bytes of a forged tag were -// correct, which reduces forging a 32-byte tag from infeasible to a few thousand requests. It is -// the reason nothing in this module hands a caller a computed tag to compare for itself. -// -// It is a host primitive rather than a shell transport because every shell spelling of HMAC puts -// the KEY IN THE ARGV, which gunbc.credential_argv_exposure forbids -- and with a symmetric MAC -// the verification key is the signing key, so a leaked key forges approvals rather than merely -// reading them. +// ── Verification ───────────────────────────────────────────────────────────────────────────── +// THE ONE FUNCTION THAT ACTUALLY VERIFIES: it recomputes the tag over the key and the exact message +// it was given, and compares full-scan (hmac_tag_difference) -- an early-exit equality over MAC +// octets leaks through timing how many leading octets of a forged tag were right, which is why no +// function here hands a caller the computed tag to compare for itself. // -// Hex rather than base64 for key and tag: the corpus already models digests as lowercase hex -// (extdeps.crypto.hash Digest.hex), and hex has exactly one spelling per value where base64 has -// several -- a decoder accepting more spellings than it should is how one envelope acquires two -// representations, which is the ambiguity the signing input was shaped to avoid. +// Hex rather than base64 for key and tag: the corpus models digests as lowercase hex +// (extdeps.crypto.hash Digest.hex), and hex has exactly one spelling per value. // -// Every malformed input answers false rather than raising, and the refusal a caller sees is -// MacTagMismatch in all of those cases. A caller cannot distinguish a bad key encoding from a -// wrong tag, which is correct: both mean the same thing to the only consumer -- this message is -// not authenticated -- and reporting which would tell a prober whether their key guess was -// well-formed. +// Every refusal is TYPED rather than collapsed into a mismatch (gunbc#11628: malformed input is +// never `false` when it is undecodable). A presented tag that is not lowercase hex is MacTagNotHex; +// one of the wrong length is MacTagMalformed; key material that is not hex is +// MacKeyMaterialMalformed. The key is the verifier's own configuration, never attacker input, so +// naming its malformation tells a prober nothing; the two tag refusals describe only what the +// prober sent. Only a well-formed tag that differs is MacTagMismatch. fn mac_verify( key: MacKey, message: NonEmptyStr, tag_hex: NonEmptyStr, ) -> MacVerification { - mac_verification_from_implementation( - key_id: key.id, - suite: key.suite, - message: message, - implementation_verified: hmac_sha256_verify_hex( - key.material as String, - message as String, - tag_hex as String, - ), - ) + match base16_decode_lower(hex: tag_hex as String) { + Absent => MacTagNotHex { key_id: key.id } + Present { value: presented } => + if list_length(items: presented) != sha256_digest_octets() { + MacTagMalformed { octets_declared: list_length(items: presented), octets_expected: sha256_digest_octets() } + } else { + match hmac_sha256_of_hex_key(key_hex: key.material as String, message: message as String) { + Err { value: HmacKeyNotHex } => MacKeyMaterialMalformed { key_id: key.id } + Err { value: e } => MacVerificationRefused { key_id: key.id, cause: e } + Ok { value: computed } => + match hmac_octet_word(o: 0) { + Err { value: e } => MacVerificationRefused { key_id: key.id, cause: e } + Ok { value: zero } => + match hmac_tag_difference(a: computed, b: presented, acc: zero) { + Err { value: e } => MacVerificationRefused { key_id: key.id, cause: e } + Ok { value: difference } => + mac_verification_from_implementation( + key_id: key.id, + suite: key.suite, + message: message, + implementation_verified: difference.value == 0, + ) + } + } + } + } + } } fn mac_verification_ok(v: MacVerification) -> Bool { @@ -243,6 +396,9 @@ fn mac_verification_ok(v: MacVerification) -> Bool { MacKeyRetired { key_id: _, retired_at: _ } => false MacSuiteMismatch { expected: _, key_suite: _ } => false MacTagMalformed { octets_declared: _, octets_expected: _ } => false + MacTagNotHex { key_id: _ } => false + MacKeyMaterialMalformed { key_id: _ } => false + MacVerificationRefused { key_id: _, cause: _ } => false } } @@ -264,5 +420,8 @@ fn mac_verification_reason(v: MacVerification) -> String { concat("mac suite mismatch: verifier expects ", concat(mac_suite_name(s: e) as String, concat(", key declares ", mac_suite_name(s: g) as String))) MacTagMalformed { octets_declared: d, octets_expected: x } => concat("mac tag length is wrong: declared ", concat(to_string(n: d), concat(" octets, expected ", to_string(n: x)))) + MacTagNotHex { key_id: k } => concat("mac tag is not lowercase hex, presented against key ", k as String) + MacKeyMaterialMalformed { key_id: k } => concat("mac key material is not lowercase hex for key ", k as String) + MacVerificationRefused { key_id: k, cause: _ } => concat("mac computation refused under key ", k as String) } } diff --git a/dag/extdeps/crypto/sha2.dag b/dag/extdeps/crypto/sha2.dag new file mode 100644 index 00000000000..29408652c6d --- /dev/null +++ b/dag/extdeps/crypto/sha2.dag @@ -0,0 +1,486 @@ +module extdeps.crypto.sha2 + +import std.error_primitives { Result, Ok, Err } +import std.integer { UInt8 } +import std.machine_word { + Word, Width8, Width32, + WordResult, WordReady, WordRefused, WordRefusal, + OctetsResult, OctetsReady, OctetsRefused, + word_of_int, word_and, word_xor, word_not, + word_shift_right, word_rotate_right, word_wrapping_add, + word_to_octets, word_from_octets, int_to_octets, octet_int_values, +} +import extdeps.toolchain.architecture_profile { BigEndian } +import extdeps.numeric.base16 { base16_decode_lower } +import extdeps.external_authority { ExternalAuthority } +import extdeps.uri { Uri, Https } + +// SHA-256 AS AN ALGORITHM, per FIPS 180-4 §4.1.2 (functions), §4.2.2 (constants), §5.1.1 +// (padding), §5.3.3 (initial value) and §6.2 (computation). extdeps.crypto.hash cites the same +// standard for the DIGEST VALUE a pin carries; this module is the computation that produces one. +// Every operation below is a std.machine_word operation at Width32: there is no bit primitive +// underneath and no host routine beside it, so what this file says SHA-256 is, is what runs. +data extdeps_external_authority_anchor: ExternalAuthority = ExternalAuthority { + uri: Uri { + scheme: Https + locator: "csrc.nist.gov/pubs/fips/180-4/upd1/final" + } +} + +// Every way the computation can fail to produce a digest. A word refusal is carried with its cause +// rather than flattened, because it can only arise from a defect in this module or the substrate +// (every word is constructed at Width32 from checked octets), and a defect should arrive located. +type Sha256Refusal + = Sha256WordRefused { cause: WordRefusal } + | Sha256ConstantNotHex { hex: String } + | Sha256OctetOutOfRange { value: Int } + | Sha256ScheduleLengthMismatch { round_constants: Int, schedule_words: Int } + | Sha256BlockMisaligned { octets: Int } + +fn sha256_lift(r: WordResult) -> Result { + match r { + WordReady { word: w } => Ok { value: w } + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + } +} + +// ── Constants, spelled as FIPS 180-4 prints them ──────────────────────────────────────────── +// The corpus has no hexadecimal integer literal, and transcribing these into decimal would make +// every row unreadable against the standard it is copied from. So they are the standard's own +// lowercase hex, decoded through the one base16 codec and packed big-endian through the substrate, +// and a malformed row refuses (Sha256ConstantNotHex) rather than becoming a plausible word. + +// §5.3.3: the first 32 bits of the fractional parts of the square roots of the first 8 primes. +data sha256_initial_hash_hex: List = [ + "6a09e667", "bb67ae85", "3c6ef372", "a54ff53a", + "510e527f", "9b05688c", "1f83d9ab", "5be0cd19", +] + +// §4.2.2: the first 32 bits of the fractional parts of the cube roots of the first 64 primes. +data sha256_round_constant_hex: List = [ + "428a2f98", "71374491", "b5c0fbcf", "e9b5dba5", "3956c25b", "59f111f1", "923f82a4", "ab1c5ed5", + "d807aa98", "12835b01", "243185be", "550c7dc3", "72be5d74", "80deb1fe", "9bdc06a7", "c19bf174", + "e49b69c1", "efbe4786", "0fc19dc6", "240ca1cc", "2de92c6f", "4a7484aa", "5cb0a9dc", "76f988da", + "983e5152", "a831c66d", "b00327c8", "bf597fc7", "c6e00bf3", "d5a79147", "06ca6351", "14292967", + "27b70a85", "2e1b2138", "4d2c6dfc", "53380d13", "650a7354", "766a0abb", "81c2c92e", "92722c85", + "a2bfe8a1", "a81a664b", "c24b8b70", "c76c51a3", "d192e819", "d6990624", "f40e3585", "106aa070", + "19a4c116", "1e376c08", "2748774c", "34b0bcb5", "391c0cb3", "4ed8aa4a", "5b9cca4f", "682e6ff3", + "748f82ee", "78a5636f", "84c87814", "8cc70208", "90befffa", "a4506ceb", "bef9a3f7", "c67178f2", +] + +// Octets arrive as plain integers (UInt8 is Compose>, and base16 decodes to +// it); the substrate's packing takes Width8 words, so each octet is admitted at Width8 first and an +// out-of-range integer refuses there rather than being reduced. +fn sha256_octet_words(octets: List, acc: List) -> Result, Sha256Refusal> { + match octets.first() { + Absent => Ok { value: acc } + Present { value: o } => + match word_of_int(width: Width8, value: o) { + WordRefused { cause: _ } => Err { value: Sha256OctetOutOfRange { value: o } } + WordReady { word: w } => sha256_octet_words(octets: octets.skip(n: 1), acc: acc |> list_push(w)) + } + } +} + +// Big-endian packing of whole 4-octet groups into Width32 words (§3.1 item 2: SHA-256 is +// big-endian). A trailing partial group refuses rather than being padded -- padding is §5.1.1's +// job and happens once, before this is ever called. +fn sha256_words_of_octets(octets: List, acc: List) -> Result, Sha256Refusal> { + let n = list_length(items: octets) + if n == 0 { + Ok { value: acc } + } else { + if n < 4 { + Err { value: Sha256BlockMisaligned { octets: n } } + } else { + match sha256_octet_words(octets: octets.take(n: 4), acc: []) { + Err { value: e } => Err { value: e } + Ok { value: group } => + match sha256_lift(r: word_from_octets(width: Width32, octets: group, endianness: BigEndian)) { + Err { value: e } => Err { value: e } + Ok { value: w } => sha256_words_of_octets(octets: octets.skip(n: 4), acc: acc |> list_push(w)) + } + } + } + } +} + +fn sha256_words_of_hex(rows: List, acc: List) -> Result, Sha256Refusal> { + match rows.first() { + Absent => Ok { value: acc } + Present { value: hex } => + match base16_decode_lower(hex: hex) { + Absent => Err { value: Sha256ConstantNotHex { hex: hex } } + Present { value: octets } => + match sha256_words_of_octets(octets: octets, acc: []) { + Err { value: e } => Err { value: e } + Ok { value: ws } => + if list_length(items: ws) != 1 { + Err { value: Sha256ConstantNotHex { hex: hex } } + } else { + sha256_words_of_hex(rows: rows.skip(n: 1), acc: concat(acc, ws)) + } + } + } + } +} + +// ── §4.1.2 functions ──────────────────────────────────────────────────────────────────────── +// The four sigma functions are one shape -- three terms of x, XORed -- differing only in the +// three amounts and in whether the third term is a rotation (the two upper-case Σ) or a plain +// shift (the two lower-case σ). One function with the distinction TYPED, rather than four copies. +type Sha256ThirdTerm + = ThirdRotates + | ThirdShifts + +fn sha256_xor3(a: Word, b: Word, c: Word) -> WordResult { + match word_xor(a: a, b: b) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: ab } => word_xor(a: ab, b: c) + } +} + +fn sha256_third(x: Word, amount: Int, third: Sha256ThirdTerm) -> WordResult { + match third { + ThirdRotates => word_rotate_right(a: x, amount: amount) + ThirdShifts => word_shift_right(a: x, amount: amount) + } +} + +fn sha256_sigma(x: Word, p: Int, q: Int, r: Int, third: Sha256ThirdTerm) -> WordResult { + match word_rotate_right(a: x, amount: p) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xp } => + match word_rotate_right(a: x, amount: q) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xq } => + match sha256_third(x: x, amount: r, third: third) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xr } => sha256_xor3(a: xp, b: xq, c: xr) + } + } + } +} + +// (4.4)-(4.7). +fn sha256_big_sigma_0(x: Word) -> WordResult { sha256_sigma(x: x, p: 2, q: 13, r: 22, third: ThirdRotates) } +fn sha256_big_sigma_1(x: Word) -> WordResult { sha256_sigma(x: x, p: 6, q: 11, r: 25, third: ThirdRotates) } +fn sha256_small_sigma_0(x: Word) -> WordResult { sha256_sigma(x: x, p: 7, q: 18, r: 3, third: ThirdShifts) } +fn sha256_small_sigma_1(x: Word) -> WordResult { sha256_sigma(x: x, p: 17, q: 19, r: 10, third: ThirdShifts) } + +// (4.2) Ch(x, y, z) = (x ∧ y) ⊕ (¬x ∧ z). +fn sha256_ch(x: Word, y: Word, z: Word) -> WordResult { + match word_and(a: x, b: y) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xy } => + match word_not(a: x) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: nx } => + match word_and(a: nx, b: z) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: nxz } => word_xor(a: xy, b: nxz) + } + } + } +} + +// (4.3) Maj(x, y, z) = (x ∧ y) ⊕ (x ∧ z) ⊕ (y ∧ z). +fn sha256_maj(x: Word, y: Word, z: Word) -> WordResult { + match word_and(a: x, b: y) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xy } => + match word_and(a: x, b: z) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: xz } => + match word_and(a: y, b: z) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: yz } => sha256_xor3(a: xy, b: xz, c: yz) + } + } + } +} + +// Addition modulo 2^32 over several terms, as §6.2.2 writes every multi-term sum. +fn sha256_add_all(terms: List, acc: Word) -> WordResult { + match terms.first() { + Absent => WordReady { word: acc } + Present { value: t } => + match word_wrapping_add(a: acc, b: t) { + WordRefused { cause: e } => WordRefused { cause: e } + WordReady { word: s } => sha256_add_all(terms: terms.skip(n: 1), acc: s) + } + } +} + +// ── §5.1.1 padding ────────────────────────────────────────────────────────────────────────── +// Append the bit "1" (the octet 0x80, since the message is whole octets), then k zero bits with +// ℓ + 1 + k ≡ 448 (mod 512), then ℓ as a 64-bit big-endian integer. In octets: zeros until the +// length is 56 mod 64, then eight octets. The length field is rendered from an ordinary Int by +// std.machine_word int_to_octets, which is how a 64-bit field is served without a Width64 word. +fn sha256_zero_octets(count: Int, acc: List) -> List { + if count <= 0 { acc } else { sha256_zero_octets(count: count - 1, acc: acc |> list_push(0)) } +} + +fn sha256_pad(message: List) -> Result, Sha256Refusal> { + let n = list_length(items: message) + let marked = message |> list_push(128) + let zeros = (119 - (n % 64)) % 64 + match int_to_octets(value: n * 8, count: 8, endianness: BigEndian) { + OctetsRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + OctetsReady { octets: length_field } => + Ok { value: concat(sha256_zero_octets(count: zeros, acc: marked), octet_int_values(octets: length_field)) } + } +} + +// ── §6.2.2 step 1: the message schedule ───────────────────────────────────────────────────── +// W_t = M_t for 0 ≤ t ≤ 15, and σ1(W_{t-2}) + W_{t-7} + σ0(W_{t-15}) + W_{t-16} for 16 ≤ t ≤ 63. +fn sha256_schedule_at(ws: List, index: Int) -> Result { + match get(xs: ws, index: index) { + Present { value: w } => Ok { value: w } + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 64, schedule_words: list_length(items: ws) } } + } +} + +fn sha256_schedule_extend(ws: List, t: Int) -> Result, Sha256Refusal> { + if t >= 64 { + Ok { value: ws } + } else { + match sha256_schedule_at(ws: ws, index: t - 2) { + Err { value: e } => Err { value: e } + Ok { value: w2 } => + match sha256_schedule_at(ws: ws, index: t - 7) { + Err { value: e } => Err { value: e } + Ok { value: w7 } => + match sha256_schedule_at(ws: ws, index: t - 15) { + Err { value: e } => Err { value: e } + Ok { value: w15 } => + match sha256_schedule_at(ws: ws, index: t - 16) { + Err { value: e } => Err { value: e } + Ok { value: w16 } => + match sha256_small_sigma_1(x: w2) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: s1 } => + match sha256_small_sigma_0(x: w15) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: s0 } => + match sha256_add_all(terms: [w7, s0, w16], acc: s1) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: wt } => sha256_schedule_extend(ws: ws |> list_push(wt), t: t + 1) + } + } + } + } + } + } + } + } +} + +// ── §6.2.2 steps 2-4: the compression ─────────────────────────────────────────────────────── +type Sha256Working { + a: Word + b: Word + c: Word + d: Word + e: Word + f: Word + g: Word + h: Word +} + +// One round: T1 = h + Σ1(e) + Ch(e,f,g) + K_t + W_t; T2 = Σ0(a) + Maj(a,b,c); then the eight +// registers shift down with a ← T1 + T2 and e ← d + T1. +fn sha256_round_step(s: Sha256Working, k: Word, w: Word) -> Result { + match sha256_big_sigma_1(x: s.e) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: s1 } => + match sha256_ch(x: s.e, y: s.f, z: s.g) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: ch } => + match sha256_add_all(terms: [s1, ch, k, w], acc: s.h) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: t1 } => + match sha256_big_sigma_0(x: s.a) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: s0 } => + match sha256_maj(x: s.a, y: s.b, z: s.c) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: mj } => + match sha256_add_all(terms: [s0, mj], acc: t1) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: next_a } => + match word_wrapping_add(a: s.d, b: t1) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: next_e } => + Ok { + value: Sha256Working { + a: next_a, b: s.a, c: s.b, d: s.c, + e: next_e, f: s.e, g: s.f, h: s.g, + } + } + } + } + } + } + } + } + } +} + +fn sha256_rounds(s: Sha256Working, ks: List, ws: List) -> Result { + match ks.first() { + Absent => Ok { value: s } + Present { value: k } => + match ws.first() { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: list_length(items: ks), schedule_words: 0 } } + Present { value: w } => + match sha256_round_step(s: s, k: k, w: w) { + Err { value: e } => Err { value: e } + Ok { value: next } => sha256_rounds(s: next, ks: ks.skip(n: 1), ws: ws.skip(n: 1)) + } + } + } +} + +fn sha256_working_of(h: List) -> Result { + if list_length(items: h) != 8 { + Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: list_length(items: h) } } + } else { + match get(xs: h, index: 0) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 0 } } + Present { value: a } => + match get(xs: h, index: 1) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 1 } } + Present { value: b } => + match get(xs: h, index: 2) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 2 } } + Present { value: c } => + match get(xs: h, index: 3) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 3 } } + Present { value: d } => + match get(xs: h, index: 4) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 4 } } + Present { value: e } => + match get(xs: h, index: 5) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 5 } } + Present { value: f } => + match get(xs: h, index: 6) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 6 } } + Present { value: g } => + match get(xs: h, index: 7) { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: 7 } } + Present { value: hh } => + Ok { value: Sha256Working { a: a, b: b, c: c, d: d, e: e, f: f, g: g, h: hh } } + } + } + } + } + } + } + } + } + } +} + +// Step 4: H_i ← working_i + H_i, as one fold over the eight registers in order. +fn sha256_feed_forward(s: Sha256Working, h: List) -> Result, Sha256Refusal> { + sha256_pairwise_add(xs: [s.a, s.b, s.c, s.d, s.e, s.f, s.g, s.h], ys: h, acc: []) +} + +fn sha256_pairwise_add(xs: List, ys: List, acc: List) -> Result, Sha256Refusal> { + match xs.first() { + Absent => Ok { value: acc } + Present { value: x } => + match ys.first() { + Absent => Err { value: Sha256ScheduleLengthMismatch { round_constants: 8, schedule_words: list_length(items: acc) } } + Present { value: y } => + match word_wrapping_add(a: x, b: y) { + WordRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + WordReady { word: z } => sha256_pairwise_add(xs: xs.skip(n: 1), ys: ys.skip(n: 1), acc: acc |> list_push(z)) + } + } + } +} + +fn sha256_block(h: List, ks: List, block: List) -> Result, Sha256Refusal> { + match sha256_words_of_octets(octets: block, acc: []) { + Err { value: e } => Err { value: e } + Ok { value: m } => + match sha256_schedule_extend(ws: m, t: 16) { + Err { value: e } => Err { value: e } + Ok { value: ws } => + if list_length(items: ws) != list_length(items: ks) { + Err { value: Sha256ScheduleLengthMismatch { round_constants: list_length(items: ks), schedule_words: list_length(items: ws) } } + } else { + match sha256_working_of(h: h) { + Err { value: e } => Err { value: e } + Ok { value: start } => + match sha256_rounds(s: start, ks: ks, ws: ws) { + Err { value: e } => Err { value: e } + Ok { value: done } => sha256_feed_forward(s: done, h: h) + } + } + } + } + } +} + +fn sha256_blocks(h: List, ks: List, padded: List) -> Result, Sha256Refusal> { + let n = list_length(items: padded) + if n == 0 { + Ok { value: h } + } else { + if n < 64 { + Err { value: Sha256BlockMisaligned { octets: n } } + } else { + match sha256_block(h: h, ks: ks, block: padded.take(n: 64)) { + Err { value: e } => Err { value: e } + Ok { value: next } => sha256_blocks(h: next, ks: ks, padded: padded.skip(n: 64)) + } + } + } +} + +fn sha256_render(h: List, acc: List) -> Result, Sha256Refusal> { + match h.first() { + Absent => Ok { value: acc } + Present { value: w } => + match word_to_octets(a: w, endianness: BigEndian) { + OctetsRefused { cause: c } => Err { value: Sha256WordRefused { cause: c } } + OctetsReady { octets: os } => sha256_render(h: h.skip(n: 1), acc: concat(acc, octet_int_values(octets: os))) + } + } +} + +// THE CONSTANT TABLES AS WORDS, DERIVED ONCE. They are facts of the standard, not of any message, +// so they are established once at module scope and every digest reads the same value (DESIGN §2: +// a fact established once is never rebuilt per consumer). Decoding them inside sha256_octets +// re-derived all 72 words on every call -- twice per HMAC. A malformed row still refuses: the +// Result is the row's value, and every digest carries the refusal forward. +data sha256_initial_hash_words: Result, Sha256Refusal> = sha256_words_of_hex(rows: sha256_initial_hash_hex, acc: []) +data sha256_round_constant_words: Result, Sha256Refusal> = sha256_words_of_hex(rows: sha256_round_constant_hex, acc: []) + +// THE DIGEST: the 32 octets H_0 ‖ … ‖ H_7 of the final hash value, big-endian. +fn sha256_octets(message: List) -> Result, Sha256Refusal> { + match sha256_initial_hash_words { + Err { value: e } => Err { value: e } + Ok { value: h0 } => + match sha256_round_constant_words { + Err { value: e } => Err { value: e } + Ok { value: ks } => + match sha256_pad(message: message) { + Err { value: e } => Err { value: e } + Ok { value: padded } => + match sha256_blocks(h: h0, ks: ks, padded: padded) { + Err { value: e } => Err { value: e } + Ok { value: h } => sha256_render(h: h, acc: []) + } + } + } + } +} + +// The two SHA-256 parameters HMAC (RFC 2104 §2) needs: the block size B and the output size L, in +// octets. They are this module's facts, so HMAC reads them here rather than restating 64 and 32. +fn sha256_block_octets() -> Int { 64 } +fn sha256_digest_octets() -> Int { 32 } diff --git a/dag/extdeps/npm.dag b/dag/extdeps/npm.dag index 1d5c9cb76de..7b0c99a244f 100644 --- a/dag/extdeps/npm.dag +++ b/dag/extdeps/npm.dag @@ -3,7 +3,8 @@ module extdeps.npm import std.types { NonEmptyStr, String, Bool, List, Int } import std.workspace_artifact { WorkspaceFootprint, WorkspaceArtifact, CitedUpstream, RegenerableFromSource } import std.integer { UInt8 } -import std.encoding { base64_decode, base64_encode, Standard } +import std.machine_word { QualifiedOctetsReady, QualifiedOctetsRefused } +import std.encoding { base64_decode, base64_encode, base64_octets, Standard } import std.content_hash { ContentHash, Sha512Digest, @@ -266,7 +267,10 @@ fn npm_registry_integrity_from_decode( } fn npm_sri_base64_payload_is_canonical(encoded: String, octets: List) -> Bool { - encoded == base64_encode(octets: octets, variant: Standard) + match base64_octets(values: octets) { + QualifiedOctetsRefused { cause: _ } => false + QualifiedOctetsReady { octets: qualified } => encoded == base64_encode(octets: qualified, variant: Standard) + } } fn npm_decode_integrity_expression(expression: String) -> NpmIntegrityDecode { diff --git a/dag/gunbc/auth/approval_capability.dag b/dag/gunbc/auth/approval_capability.dag index 2d9dfdcbc2d..849be22bf67 100644 --- a/dag/gunbc/auth/approval_capability.dag +++ b/dag/gunbc/auth/approval_capability.dag @@ -3,11 +3,12 @@ module gunbc.auth.approval_capability import std.types { NonEmptyStr, String, Int, Timestamp } import std.logic { Bool } import std.scoped_authorization { AttemptIdentity } -import std.encoding { base64_encode, base64_decode, UrlSafe } +import std.machine_word { QualifiedOctetsReady, QualifiedOctetsRefused } +import std.encoding { base64_encode, base64_octets, base64_decode, UrlSafe } import extdeps.numeric.base16 { base16_encode_lower, base16_decode_lower } import extdeps.crypto.mac { MacSuite, MacKeyId, MacKey, MacVerification, MacVerified, VerifiedMessage, - MacSigning, MacSigned, MacKeyMaterialNotHex, + MacSigning, MacSigned, MacKeyMaterialNotHex, MacComputationRefused, HmacRefusal, mac_verification_reason, mac_suite_name, mac_sign, } @@ -172,12 +173,16 @@ fn approval_capability_signing_input(c: ApprovalCapabilityClaims) -> NonEmptyStr // would refuse as CapabilityKeyIdDisagrees; minting it is an issuer bug, // and the place to report it is here, before it reaches an operator. // non-hex key material -- no key, no tag (extdeps.crypto.mac MacKeyMaterialNotHex). +// the HMAC computation refused -- carried with its located cause (extdeps.crypto.mac +// MacComputationRefused); unreachable for a well-formed key and message. // a tag that is not lowercase hex -- the bound implementation broke its own contract; named as // such rather than folded into a cause that did not happen. type CapabilityIssuanceRefusal = IssuanceKeyIdDisagrees { claimed: MacKeyId, signing_key: MacKeyId } | IssuanceKeyMaterialNotHex { key_id: MacKeyId } | IssuanceImplementationTagNotHex { key_id: MacKeyId } + | IssuanceImplementationTagNotOctets { key_id: MacKeyId } + | IssuanceComputationRefused { key_id: MacKeyId, cause: HmacRefusal } type CapabilityIssuance = CapabilityIssued { capability: ApprovalCapability } @@ -192,15 +197,21 @@ fn issue_capability(claims: ApprovalCapabilityClaims, key: MacKey) -> Capability match mac_sign(key: key, message: approval_capability_signing_input(c: claims)) { MacKeyMaterialNotHex { key_id: k } => CapabilityIssuanceRefused { cause: IssuanceKeyMaterialNotHex { key_id: k } } + MacComputationRefused { key_id: k, cause: c } => + CapabilityIssuanceRefused { cause: IssuanceComputationRefused { key_id: k, cause: c } } MacSigned { tag: t } => 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_octets(values: octets) { + QualifiedOctetsRefused { cause: _ } => CapabilityIssuanceRefused { cause: IssuanceImplementationTagNotOctets { key_id: t.key_id } } + QualifiedOctetsReady { octets: qualified } => + CapabilityIssued { + capability: ApprovalCapability { + claims: claims, + tag_b64url: base64_encode(octets: qualified, variant: UrlSafe) as NonEmptyStr, + } + } } } } @@ -216,10 +227,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_octets(values: octets) { + QualifiedOctetsRefused { cause: _ } => none + QualifiedOctetsReady { octets: qualified } => + if base64_encode(octets: qualified, variant: UrlSafe) != presented || octets == [] { + none + } else { + Present { value: base16_encode_lower(octets: octets) as NonEmptyStr } + } } } } diff --git a/dag/gunbc/auth/approval_device_wire.dag b/dag/gunbc/auth/approval_device_wire.dag index 173790862f4..a5240ec4d5c 100644 --- a/dag/gunbc/auth/approval_device_wire.dag +++ b/dag/gunbc/auth/approval_device_wire.dag @@ -11,8 +11,9 @@ import extdeps.google.fcm { FcmProjectId, FcmRegistrationToken } 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.machine_word { QualifiedOctetsReady, QualifiedOctetsRefused } +import std.encoding { base64_encode, base64_octets, base64_decode, UrlSafe, utf8_decode_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 +827,26 @@ 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-" +// THE OCTETS ARE ADMITTED ONCE, AND THE ENCODER IS TOTAL AGAIN. +// +// This call site is why base64_encode stopped being total in the first place and why it is total +// once more. When the encoder returned String?, this line joined the Optional straight into the +// path and rendered "id-Present \{ value: ZXNj... \}" into a route identity -- silently, because +// join accepted an Optional member with no type error. One caller that did not handle an arm undid +// the whole channel, which is what makes a widened return type the wrong shape: it is defeated +// wherever it is not matched. +// +// The refusal now lives where the octet is MADE. base64_octets admits the UTF-8 bytes into the +// qualified carrier once; past it an octet cannot be out of range by type, so the encoder is total +// and this function keeps the contract its own annotation declares above -- total, injective, never +// refused. The refusal arm here is unreachable for the same reason it always was (these are the +// UTF-8 encoding of a String), and it diverges rather than fabricating a path. 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_octets(values: bytes_octets(b: utf8_encode_bytes(s: s as String))) { + QualifiedOctetsReady { octets: qualified } => + join([path_segment_prefix, base64_encode(octets: qualified, variant: UrlSafe)], "") as NonEmptyStr + QualifiedOctetsRefused { cause: _ } => 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/auth/approval_mac_key_provision.dag b/dag/gunbc/auth/approval_mac_key_provision.dag index 8bf72b75e8c..f5931c08871 100644 --- a/dag/gunbc/auth/approval_mac_key_provision.dag +++ b/dag/gunbc/auth/approval_mac_key_provision.dag @@ -47,7 +47,7 @@ import gunbc.auth.approval_request_submission { approval_submission_mac_key_secr // nothing here runs past one. // // THE MATERIAL IS 32 OCTETS FROM /dev/urandom RENDERED AS 64 LOWER HEX -- the spelling -// extdeps.crypto.mac hmac_sha256_hex takes as key material -- and it never reaches argv or a log: +// extdeps.crypto.mac mac_sign takes as key material -- and it never reaches argv or a log: // the actuator's snapshot writes it 0600 into a run-owned directory, digests the FILE, and the // version is verified by reading back the store. What this run prints is the version and the // digest prefix, which is what the SecretRef rows pin. diff --git a/dag/gunbc/auth/approval_request_client.dag b/dag/gunbc/auth/approval_request_client.dag index cafb82c65a7..6bf1febe6ef 100644 --- a/dag/gunbc/auth/approval_request_client.dag +++ b/dag/gunbc/auth/approval_request_client.dag @@ -3,7 +3,7 @@ module gunbc.auth.approval_request_client import std.types { Bool, NonEmptyStr, String, Timestamp, Secret } import std.scoped_authorization { AuthorizationRequest } import extdeps.crypto.mac { - MacKey, MacSigned, MacKeyMaterialNotHex, HmacSha256, MacKeyId, + MacKey, MacSigned, MacKeyMaterialNotHex, MacComputationRefused, HmacRefusal, HmacSha256, MacKeyId, } import gunbc.auth.approval_status_wire { FiledApprovalStatus, StatusNotFiled, StatusPending, StatusApproved, StatusDenied, StatusUnreadable, @@ -59,6 +59,7 @@ fn stored_request_from_authorization( type SubmissionMac = SubmissionMacReady { tag_hex: NonEmptyStr } | SubmissionMacKeyNotHex { key_id: MacKeyId } + | SubmissionMacComputationRefused { key_id: MacKeyId, cause: HmacRefusal } fn sign_stored_request(key_material: String, request: StoredApprovalRequest) -> SubmissionMac { let key = MacKey { @@ -68,6 +69,7 @@ fn sign_stored_request(key_material: String, request: StoredApprovalRequest) -> } match sign_submission(key: key, request: request) { MacKeyMaterialNotHex { key_id: k } => SubmissionMacKeyNotHex { key_id: k } + MacComputationRefused { key_id: k, cause: c } => SubmissionMacComputationRefused { key_id: k, cause: c } MacSigned { tag: t } => SubmissionMacReady { tag_hex: t.hex } } } diff --git a/dag/gunbc/auth/approval_request_submission.dag b/dag/gunbc/auth/approval_request_submission.dag index cfb7cd58492..0d34ea315ec 100644 --- a/dag/gunbc/auth/approval_request_submission.dag +++ b/dag/gunbc/auth/approval_request_submission.dag @@ -3,7 +3,7 @@ module gunbc.auth.approval_request_submission import std.types { Bool, Int, NonEmptyStr, String, Secret, HttpStatus } import std.dissolution { DissolutionCondition, unbound_dissolution } import extdeps.filesystem.filesystem_io { Filesystem, FilesystemExactPathRead, FilesystemExactPathAbsent, FilesystemExactPathUnreadable, FilesystemExactPathKindUnrecognized, filesystem_exact_read } -import extdeps.crypto.mac { MacKey, MacKeyId, MacSigning, MacSigned, MacKeyMaterialNotHex, MacVerification, MacVerified, mac_sign, mac_verify, mac_verification_reason } +import extdeps.crypto.mac { MacKey, MacKeyId, MacSigning, MacSigned, MacKeyMaterialNotHex, MacComputationRefused, MacVerification, MacVerified, mac_sign, mac_verify, mac_verification_reason } import extdeps.languages.json.emit { JsonValue, JsonString, serialize_json, json_object, json_kv, json_string } import extdeps.languages.json.parse { JsonDocumentParsed, JsonDocumentUnreadable, JsonMemberFound, JsonMemberAbsent, JsonMemberDuplicated, JsonMemberNotAnObject, parse_json_document, json_object_unique_member } import extdeps.ntfy.ntfy { NtfyMessage, NtfyPublishOutcome, NtfyPublished, NtfyPublishRefused, NtfyPublishUnreached, NtfyPublishUndecodable, ntfy_publish_outcome_of, ntfy_priority_wire, ntfy_cache_wire } @@ -206,12 +206,18 @@ type LinkIssuance = LinksIssued { approve: NonEmptyStr, deny: NonEmptyStr } | LinksNotIssued { key_id: MacKeyId } +// A signing refusal of either kind -- key material that is not hex, or the HMAC computation refusing +// (extdeps.crypto.mac MacComputationRefused, unreachable for a well-formed key) -- means no link +// exists under that key, which is exactly what LinksNotIssued reports; the typed cause stays on the +// MacSigning value that produced it. fn issue_links(capability_key: MacKey, base: NonEmptyStr, request: StoredApprovalRequest) -> LinkIssuance { match mac_sign(key: capability_key, message: approval_capability_signing_input(c: claims_for(request: request, decision: ProposeApprove))) { MacKeyMaterialNotHex { key_id: k } => LinksNotIssued { key_id: k } + MacComputationRefused { key_id: k, cause: _ } => LinksNotIssued { key_id: k } MacSigned { tag: approve_tag } => match mac_sign(key: capability_key, message: approval_capability_signing_input(c: claims_for(request: request, decision: ProposeDeny))) { MacKeyMaterialNotHex { key_id: k } => LinksNotIssued { key_id: k } + MacComputationRefused { key_id: k, cause: _ } => LinksNotIssued { key_id: k } MacSigned { tag: deny_tag } => LinksIssued { approve: approval_link(base: base, request: request, decision: ProposeApprove, tag_hex: approve_tag.hex), deny: approval_link(base: base, request: request, decision: ProposeDeny, tag_hex: deny_tag.hex), diff --git a/dag/gunbc/census_closure_frontier.dag b/dag/gunbc/census_closure_frontier.dag index 572251f1b38..2975cedee0b 100644 --- a/dag/gunbc/census_closure_frontier.dag +++ b/dag/gunbc/census_closure_frontier.dag @@ -61,6 +61,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 } @@ -133,6 +134,7 @@ fn census_closure_frontier_row_groups() -> List> { arm_ci_seller_census_later_consumer_frontier_rows, runner_canary_executed_evidence_frontier, network_boot_manifest_broker_frontier_rows, + machine_word_consumer_frontier_rows, ] } diff --git a/dag/gunbc/instruments/approval_store_live_probe.dag b/dag/gunbc/instruments/approval_store_live_probe.dag index 170647032ac..8344e88e603 100644 --- a/dag/gunbc/instruments/approval_store_live_probe.dag +++ b/dag/gunbc/instruments/approval_store_live_probe.dag @@ -4,7 +4,7 @@ import std.types { Bool, NonEmptyStr, String, Timestamp, POST, Secret } import std.process { ProcessExit, ExitSuccess, exit_failure } import std.content_hash { ContentHash, Sha256Hash, Sha256Digest } import std.scoped_authorization { AttemptIdentity, AuthorizationRequest, AuthorizationGranted, AuthorizationDenied, AuthorizationPending } -import extdeps.crypto.mac { MacKey, HmacSha256, MacSigned, MacKeyMaterialNotHex } +import extdeps.crypto.mac { MacKey, HmacSha256, MacSigned, MacKeyMaterialNotHex, MacComputationRefused } import extdeps.tailscale.identity { tailnet_identity_of } import gunbc.auth.approval_capability { ProposeApprove, ProposeDeny } import gunbc.auth.approval_broker { BrokerApproved, BrokerDenied } @@ -184,6 +184,7 @@ fn probe_request_other_bytes() -> StoredApprovalRequest { fn probe_submit(root: NonEmptyStr, signer: MacKey, request: StoredApprovalRequest) -> ProbeSubmitStanding { match sign_submission(key: signer, request: request) { MacKeyMaterialNotHex { key_id: _ } => ProbeOther { reason: "unsigned" } + MacComputationRefused { key_id: _, cause: _ } => ProbeOther { reason: "signing computation refused" } MacSigned { tag: t } => { let outcome = submit_parsed_submission( root: root, diff --git a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag index 461425ee683..b55e90ea8d9 100644 --- a/dag/gunbc/machine_intake/mtcollins1_boot_run.dag +++ b/dag/gunbc/machine_intake/mtcollins1_boot_run.dag @@ -31,7 +31,7 @@ import gunbc.auth.approval_request_client { stored_request_from_authorization, sign_stored_request, approval_submit_url, approval_status_url, approval_poll_standing, - SubmissionMacReady, SubmissionMacKeyNotHex, + SubmissionMacReady, SubmissionMacKeyNotHex, SubmissionMacComputationRefused, PollStillPending, } import gunbc.auth.approval_status_wire { @@ -678,6 +678,8 @@ fn mtcollins1_boot_wet_on_srv1() -> ProcessExit match sign_stored_request(key_material: trim(s: key_read.content), request: stored) { SubmissionMacKeyNotHex { key_id: k } => exit_failure(reason: concat("mtcollins1 boot: submission MAC key is not hex: ", k as String)) + SubmissionMacComputationRefused { key_id: k, cause: _ } => + exit_failure(reason: concat("mtcollins1 boot: submission MAC computation refused under key ", k as String)) SubmissionMacReady { tag_hex: tag } => { let tmp = actions_variable_trimmed(name: github_runner_temp_variable_name as NonEmptyStr) if tmp == "" { diff --git a/dag/gunbc/network_boot_manifest_broker.dag b/dag/gunbc/network_boot_manifest_broker.dag index acd131c28b9..eaa26d5a6e1 100644 --- a/dag/gunbc/network_boot_manifest_broker.dag +++ b/dag/gunbc/network_boot_manifest_broker.dag @@ -25,10 +25,15 @@ import extdeps.crypto.mac { MacKeyRetired, MacSuiteMismatch, MacTagMalformed, + MacTagNotHex, + MacKeyMaterialMalformed, + MacVerificationRefused, VerifiedMessage, MacSigning, MacSigned, MacKeyMaterialNotHex, + MacComputationRefused, + HmacRefusal, mac_sign, mac_verify, } @@ -80,6 +85,7 @@ type SignedBootManifestTicket { type BootManifestIssuanceRefusal = ManifestIssuanceKeyIdDisagrees { claimed: MacKeyId, signing_key: MacKeyId } | ManifestIssuanceKeyMaterialNotHex { key_id: MacKeyId } + | ManifestIssuanceComputationRefused { key_id: MacKeyId, cause: HmacRefusal } | ManifestIssuanceWindowInverted { not_before: EpochMs, expiry: EpochMs } | ManifestIssuanceTrustUnestablished | ManifestIssuanceDhcpArchUnpublished @@ -231,6 +237,8 @@ fn issue_signed_boot_manifest_under_trust(identity: SignedBootManifestIdentity, match mac_sign(key: key, message: message) { MacKeyMaterialNotHex { key_id: k } => BootManifestIssuanceRefused { cause: ManifestIssuanceKeyMaterialNotHex { key_id: k } } + MacComputationRefused { key_id: k, cause: c } => + BootManifestIssuanceRefused { cause: ManifestIssuanceComputationRefused { key_id: k, cause: c } } MacSigned { tag: t } => BootManifestIssued { ticket: SignedBootManifestTicket { identity: identity, tag_hex: t.hex }, @@ -280,6 +288,9 @@ fn verify_signed_boot_manifest_under_trust( MacSuiteMismatch { expected: _, key_suite: _ } => refused(class: ManifestVerificationSuite) MacKeyUnknown { key_id: _ } => refused(class: ManifestVerificationSigningKey) MacKeyRetired { key_id: _, retired_at: _ } => refused(class: ManifestVerificationSigningKey) + MacTagNotHex { key_id: _ } => refused(class: ManifestVerificationMac) + MacKeyMaterialMalformed { key_id: _ } => refused(class: ManifestVerificationSigningKey) + MacVerificationRefused { key_id: _, cause: _ } => refused(class: ManifestVerificationMac) } } diff --git a/dag/gunbc/plans/blackjack_onboarding.dag b/dag/gunbc/plans/blackjack_onboarding.dag index 98a2226a143..3a17d31196e 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_decode }\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, already admitted as octets by the decoder, and a fold\n// combines them. Take the real decoded type here -- do not mint an Int list, and do not re-admit\n// what the decoder has already established.\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 folds over those octets — 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/gunbc/v1/v1_interpreter_primitive_surface.dag b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag index 8b2a1f920e7..286cc105df7 100644 --- a/dag/gunbc/v1/v1_interpreter_primitive_surface.dag +++ b/dag/gunbc/v1/v1_interpreter_primitive_surface.dag @@ -488,24 +488,6 @@ fn v1_interpreter_authored_roster_arms() -> List 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..1e4e735213d 100644 --- a/dag/std/encoding.dag +++ b/dag/std/encoding.dag @@ -3,9 +3,17 @@ module std.encoding import std.algebra { BoundedLattice } import std.types { Bytes } import std.integer { UInt8 } -import std.bytes { pure_dag_seam_unreachable } +import std.machine_word { Word, Width8, Width32, WordResult, WordReady, WordRefused, OctetsReady, OctetsRefused, QualifiedWord, QualifiedOctetsResult, QualifiedOctetsReady, QualifiedOctetsRefused, word_of_int, word_from_octets, word_to_octets, word_shift_left, word_shift_right, word_and, word_or, octet_int_values, octets_qualified, qualified_word_unwrap } +import extdeps.toolchain.architecture_profile { BigEndian } +import std.bytes { pure_dag_seam_unreachable, pure_dag_seam_unreachable_string } import std.disposition { Disposition, Scaffold, Terminal, SingleAuthority } import std.decl_ref { DeclarationRef, WholeDeclaration } +import std.error_primitives { Result, Ok, Err } +import std.unicode.types { + unicode_scalar_max_code_point, + unicode_surrogate_first_code_point, + unicode_surrogate_last_code_point, +} type Encoding = ASCII @@ -117,6 +125,47 @@ fn utf8_decode_bytes(payload: Bytes) -> String { from_code_point(pure_dag_seam_unreachable()) } +// UTF-8 ENCODING, RFC 3629 §3, over the code points of a String. The decode direction above is +// still a seam; this direction is pure arithmetic and is authored. A code point that is not a +// Unicode scalar value -- a surrogate, or one above U+10FFFF -- has no UTF-8 encoding at all +// (RFC 3629 §3 forbids encoding surrogates), so it refuses rather than producing the CESU-style +// three-octet form a naive range table would emit. A String admitted by the text layer cannot hold +// one; the refusal exists so this function's contract does not depend on that. +type Utf8EncodeRefusal + = Utf8SurrogateRefused { cp: Int } + | Utf8OutOfRangeRefused { cp: Int } + +fn utf8_encode_code_point(cp: Int) -> Result, Utf8EncodeRefusal> { + if cp < 0 || cp > unicode_scalar_max_code_point { + Err { value: Utf8OutOfRangeRefused { cp: cp } } + } else if cp >= unicode_surrogate_first_code_point && cp <= unicode_surrogate_last_code_point { + Err { value: Utf8SurrogateRefused { cp: cp } } + } else if cp < 128 { + Ok { value: [cp] } + } else if cp < 2048 { + Ok { value: [192 + cp / 64, 128 + cp % 64] } + } else if cp < 65536 { + Ok { value: [224 + cp / 4096, 128 + (cp / 64) % 64, 128 + cp % 64] } + } else { + Ok { value: [240 + cp / 262144, 128 + (cp / 4096) % 64, 128 + (cp / 64) % 64, 128 + cp % 64] } + } +} + +fn utf8_encode_code_points(code_points: List, acc: List) -> Result, Utf8EncodeRefusal> { + match code_points.first() { + Absent => Ok { value: acc } + Present { value: cp } => + match utf8_encode_code_point(cp: cp) { + Err { value: e } => Err { value: e } + Ok { value: os } => utf8_encode_code_points(code_points: code_points.skip(n: 1), acc: concat(acc, os)) + } + } +} + +fn utf8_encode_octets(s: String) -> Result, Utf8EncodeRefusal> { + utf8_encode_code_points(code_points: s |> chars, acc: []) +} + type Base64Variant = Standard | UrlSafe fn base64_alphabet(variant: Base64Variant) -> String { @@ -128,71 +177,224 @@ fn base64_alphabet(variant: Base64Variant) -> String { type Base64EncodeBuf = EncEmpty - | EncOne { b0: Int } - | EncTwo { b0: Int, b1: Int } + | EncOne { b0: QualifiedWord } + | EncTwo { b0: QualifiedWord, b1: QualifiedWord } type Base64EncodeState { out: String 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) +} + +// THE ONE PLACE AN OCTET IS MADE, AND THEREFORE THE ONE PLACE IT IS REFUSED. +// +// base64_encode previously returned String? so that an out-of-range octet could refuse at the +// ENCODER. That was a widening, and a widening is defeated at every caller: main's +// gunbc.auth.approval_device_wire joined the Optional straight into a URL path and rendered +// "id-Present \{ value: ... \}" into a route identity, with nothing in the type system objecting. +// One unhandled arm undid the whole channel. +// +// An out-of-range octet is a CONSTRUCTION failure, not an encoding failure, so it belongs here. +// base64_octets admits a List into the qualified carrier once; past this point an octet +// cannot be out of range BY TYPE, so base64_encode is total again and every caller stops carrying +// an arm that cannot occur for it. This is the same move std.machine_word makes with QualifiedWord, +// applied at the boundary where raw values enter. +fn base64_octets(values: List) -> QualifiedOctetsResult { + octets_qualified(octets: [], remaining: values |> map(v => Word { width: Width8, value: v + 0 })) +} + +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: QualifiedWord, y: QualifiedWord, z: QualifiedWord) -> WordResult { + base64_group_of_words( + a: qualified_word_unwrap(q: x), + b: qualified_word_unwrap(q: y), + c: qualified_word_unwrap(q: z) + ) } -fn base64_sextet_char(alphabet: String, n: Int, divisor: Int) -> String { - char_at(alphabet, (n / divisor) % 64) +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: Int, alphabet: String) -> Base64EncodeState { +fn base64_encode_step(st: Base64EncodeState, octet: QualifiedWord, 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: QualifiedWord, 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_zero_octet() { + WordRefused { cause: _ } => none + WordReady { word: zero } => + match base64_group_of_words(a: qualified_word_unwrap(q: x), 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_zero_octet() { + WordRefused { cause: _ } => none + WordReady { word: zero } => + match base64_group_of_words(a: qualified_word_unwrap(q: x), b: qualified_word_unwrap(q: y), 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_optional(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) + } +} + +// THE DIVERGENCE IS NAMED, BECAUSE AN ABORT THAT IDENTIFIES NOTHING IS NOT A LOCATED FAILURE. +// +// std.bytes' seam is a bare 1 / 0. Diverging through it directly would abort with a generic +// divide-by-zero naming neither the carrier that was forged nor the operation that was running -- +// loud, but anonymous. .dag has no throw-with-message, so the only thing that carries identity at +// an abort is the FUNCTION NAME on the stack. This wrapper exists to put both facts there: the +// operation (base64 encode) and the cause (a forged qualified octet). It has one caller and no +// other reason to exist. +fn base64_encode_forged_qualified_octet_diverges() -> String { + pure_dag_seam_unreachable_string() +} + +// TOTAL FOR EVERY OCTET THE SANCTIONED CONSTRUCTOR PRODUCES. +// +// Every member produced by base64_octets is an established Width8 octet, so no shift, mask or +// packing can refuse for any input this module can construct, and the encoder needs no refusal +// channel. The one way to reach the arm below is to forge the carrier; that possibility, its rung +// and its trigger are stated ONCE at their home -- std.machine_word's QualifiedWord annotation -- +// and are not restated here, because a fact with two statements is a fact that can disagree with +// itself, which is what an earlier cut of this annotation did. +// +// Returning "" instead would be a fabricated plausible output: "" is the legitimate encoding of the +// empty input, so it would stand where a failure happened and be indistinguishable from success. +fn base64_encode(octets: List, variant: Base64Variant) -> String { + match base64_encode_optional(octets: octets, variant: variant) { + Present { value: encoded } => encoded + Absent => base64_encode_forged_qualified_octet_diverges() + } } fn base64_char_value(c: String, variant: Base64Variant) -> Int? { @@ -247,21 +449,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 +525,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 +639,28 @@ 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 admits the member through word_of_int at Width8, so a value outside the byte +// range REFUSES instead of being renamed. It admits ONE member rather than going through +// base64_octets, which admits a whole list: this fold already visits members one at a time and +// already has a per-member refusal state to land on. 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 word_of_int(width: Width8, value: b + 0) { + 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..b16c24ab2a7 --- /dev/null +++ b/dag/std/machine_word.dag @@ -0,0 +1,798 @@ +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, BitWidth, bit_width, bit_width_count } +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 + +// THE BIT COUNT IS A MEASURE, AND std.measure ALREADY OWNS IT. BitWidth = Measure is the corpus's carrier for exactly this fact, and std.integer +// uint8_channel_bit_width_int consumes it for exactly this purpose -- so returning a bare Int here +// would have been a second representation of a unit the corpus already models, which is section 2's +// re-invention and section 3's fork in one. The width answers the CARRIER; word_width_bits is the +// projection to Int for the arithmetic below, derived through bit_width_count rather than spelled +// independently, which is the same two-step std.integer uses. +fn word_bit_width(w: WordWidth) -> BitWidth { + match w { + Width8 => bit_width(count: 8) + Width16 => bit_width(count: 16) + Width32 => bit_width(count: 32) + Width64 => bit_width(count: 64) + } +} + +fn word_width_bits(w: WordWidth) -> Int { + bit_width_count(b: word_bit_width(w: w)) +} + +// 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, AND THIS IS THE ONE PLACE IT IS SAID. 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. Every consumer that has an arm +// reachable only by that forgery CITES this paragraph rather than restating it -- std.encoding +// base64_encode is the current one. A fact with two statements is a fact that can disagree with +// itself, and it did: an earlier cut had this annotation calling the carrier forgeable while the +// encoder called its own arm unreachable, in the same change (review 68594). 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. +// The octet's own width, routed through the same carrier rather than re-typing bits_per_byte's Nat +// down to Int in passing. This is std.integer uint8_channel_bit_width_int's exact form. +fn octet_bit_width() -> Int { + bit_width_count(b: bit_width(count: 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. +// +// THE SHA-256 ROWS ARE GONE BECAUSE THEIR CONSUMER ARRIVED, NOT BECAUSE THEY WERE REBOUND. Rows for +// word_wrapping_add, word_rotate_right, word_xor and word_not stood here, unbound, while +// extdeps.crypto.sha2 existed only on gunbc#11647: a DeclarationRef is a CITATION resolved against +// the tree it runs in, so citing an absent module refused CITED-MODULE-ABSENT. #11647 deletes them in +// the transaction that lands sha256_add_all, sha256_sigma, sha256_xor3 and sha256_ch. Rebinding them +// there would have produced rows whose DeclarationAppears trigger fires in the commit that writes +// them -- a frontier discharged on arrival describes nothing, and section 3c's state for a +// declaration whose consumer is in the closure is consumed-by-execution, which needs no row. +// +// Every row that remains is unbound for the other reason: the consuming change is named but has +// authored no declaration to point at, and 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_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/primitives.dag b/dag/std/primitives.dag index ec917ef9fcf..5a903560b7a 100644 --- a/dag/std/primitives.dag +++ b/dag/std/primitives.dag @@ -30,29 +30,6 @@ data string_length_contract: PrimitiveContract = { carrier_cost: CarrierInsensitive } -// Work is linear in the message, as any MAC over it must be. The output is one bit -- deliberately, -// since extdeps.crypto.mac exposes no computed tag: the comparison happens inside the bound -// implementation, in constant time, and a caller that could see the tag could compare it in -// variable time instead. -data hmac_sha256_verify_hex_contract: PrimitiveContract = { - name: "hmac_sha256_verify_hex", - work: "n", - output_size: "1", - certainty: Proven, - carrier_cost: CarrierInsensitive -} - -// Issuance: work linear in the message, output the 64 lowercase hex digits of a 32-octet tag. A -// SECOND contract rather than a widened verify, because only the key holder mints; a verifier keeps -// its one-bit answer (hmac_sha256_verify_hex_contract above) and never sees a tag to compare. -data hmac_sha256_hex_contract: PrimitiveContract = { - name: "hmac_sha256_hex", - work: "n", - output_size: "64", - certainty: Proven, - carrier_cost: CarrierInsensitive -} - data substring_contract: PrimitiveContract = { name: "substring", work: "end", @@ -562,8 +539,6 @@ data contiguous_loop_elementwise_float_kernel_contract: PrimitiveContract = { fn builtin_registry_surface_names() -> List { [ - "hmac_sha256_verify_hex", - "hmac_sha256_hex", "count", "string_length", "code_point", @@ -717,8 +692,6 @@ fn primitive_contract_roster() -> List { [ char_at_contract, string_length_contract, - hmac_sha256_verify_hex_contract, - hmac_sha256_hex_contract, substring_contract, string_contains_contract, starts_with_contract, diff --git a/dag/test/claim/approval_device_redemption_witness_test.dag b/dag/test/claim/approval_device_redemption_witness_test.dag index 1ca68ea121b..9c273d60c94 100644 --- a/dag/test/claim/approval_device_redemption_witness_test.dag +++ b/dag/test/claim/approval_device_redemption_witness_test.dag @@ -5,7 +5,7 @@ import std.types { String, NonEmptyStr, Timestamp, Secret } import std.measure { byte_size } import std.scoped_authorization { AttemptIdentity } import std.durable_compare_and_set { cas_generation_count } -import extdeps.crypto.mac { MacKey, HmacSha256, mac_sign, MacSigned, MacKeyMaterialNotHex } +import extdeps.crypto.mac { MacKey, HmacSha256, mac_sign, MacSigned, MacKeyMaterialNotHex, MacComputationRefused } import extdeps.transports.rest { RestOk, RestStatusRefused, RestTransportRefused } import extdeps.apple.apns { apns_send_outcome_of } import extdeps.apple.app_attest { @@ -186,6 +186,7 @@ fn mac_hex(message: NonEmptyStr) -> NonEmptyStr { match mac_sign(key: fx_key(), message: message) { MacSigned { tag: t } => t.hex MacKeyMaterialNotHex { key_id: _ } => "not-hex" + MacComputationRefused { key_id: _, cause: _ } => "refused" } } diff --git a/dag/test/claim/approval_request_submission_witness_test.dag b/dag/test/claim/approval_request_submission_witness_test.dag index 80fc865edaa..2db0fd55dca 100644 --- a/dag/test/claim/approval_request_submission_witness_test.dag +++ b/dag/test/claim/approval_request_submission_witness_test.dag @@ -3,7 +3,7 @@ module test.claim.approval_request_submission_witness_test import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.types { Bool, NonEmptyStr, String, Secret } import std.scoped_authorization { AttemptIdentity } -import extdeps.crypto.mac { MacKey, HmacSha256, MacSigned, MacKeyMaterialNotHex, MacVerified, mac_verify } +import extdeps.crypto.mac { MacKey, HmacSha256, MacSigned, MacKeyMaterialNotHex, MacComputationRefused, MacVerified, mac_verify } import gunbc.auth.approval_capability { ProposeApprove, ProposeDeny, approval_capability_signing_input } import gunbc.auth.approval_decision_store { ApprovalKeyringRead, ApprovalKeyLoaded, ApprovalKeyringRefused, ApprovalKeyFileAbsent, StoredApprovalRequest, stored_request_json, claims_for, @@ -51,6 +51,7 @@ fn signed_envelope() -> String { match sign_submission(key: submission_key(), request: request()) { MacSigned { tag: t } => submission_envelope_json(request: request(), tag_hex: t.hex) MacKeyMaterialNotHex { key_id: _ } => "" + MacComputationRefused { key_id: _, cause: _ } => "" } } @@ -112,6 +113,7 @@ test fn the_capability_key_cannot_file_a_request() -> Bool { _ => false } MacKeyMaterialNotHex { key_id: _ } => false + MacComputationRefused { key_id: _, cause: _ } => false } } diff --git a/dag/test/claim/auth/approval_capability_issuance_witness_test.dag b/dag/test/claim/auth/approval_capability_issuance_witness_test.dag index 143eefa80bf..c3a111b8b42 100644 --- a/dag/test/claim/auth/approval_capability_issuance_witness_test.dag +++ b/dag/test/claim/auth/approval_capability_issuance_witness_test.dag @@ -27,7 +27,7 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // seam, which is right for discriminating verify_capability's policy and says nothing about whether // a tag the broker mints actually verifies. This file is that inhabitance claim: every capability // below is produced by issue_capability, and every verdict comes from mac_verify running -// hmac_sha256_verify_hex over the bytes the verifier itself serialized. Deleting issuance, the +// the modeled HMAC-SHA-256 over the bytes the verifier itself serialized. Deleting issuance, the // transcoding, or the shared signing input must turn the round-trip red. data broker_key_id: MacKeyId = "broker-2026-09" as MacKeyId diff --git a/dag/test/claim/base64_rfc4648_witness_test.dag b/dag/test/claim/base64_rfc4648_witness_test.dag index 24c1720482e..5f802647e85 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_octets(values: octets) { + QualifiedOctetsReady { octets: qualified } => base64_encode(octets: qualified, variant: variant) + QualifiedOctetsRefused { cause: _ } => "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 word_of_int at Width8, 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/mac_verification_witness_test.dag b/dag/test/claim/mac_verification_witness_test.dag index 1a8408ec9ff..6d24e13d518 100644 --- a/dag/test/claim/mac_verification_witness_test.dag +++ b/dag/test/claim/mac_verification_witness_test.dag @@ -3,15 +3,16 @@ module test.claim.mac_verification_witness_test import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import extdeps.crypto.mac { MacKey, MacKeyId, MacSuite, HmacSha256, MacVerification, MacVerified, - MacTagMismatch, mac_verify, mac_verification_ok, - MacSigning, MacSigned, MacKeyMaterialNotHex, mac_sign, + MacTagMismatch, MacTagMalformed, MacTagNotHex, MacKeyMaterialMalformed, + mac_verify, mac_verification_ok, + MacSigning, MacSigned, MacKeyMaterialNotHex, MacComputationRefused, mac_sign, } import std.types { NonEmptyStr, Secret } import std.logic { Bool } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly -// ── RFC 4231 test vectors, verified through the bound implementation ───────────────────────── +// ── RFC 4231 test vectors, verified through the modeled HMAC ───────────────────────────────── // THESE ARE NOT FIXTURES I COMPUTED. RFC 4231 publishes HMAC-SHA-256 test vectors precisely so an // implementation can be checked against something it did not produce. A fixture generated by the // code under test would pass whatever that code does, including nothing -- which is the @@ -19,6 +20,8 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // // Case 1: key = 20 octets of 0x0b, message = "Hi There" // Case 2: key = "Jefe", message = "what do ya want for nothing?" +// Case 6: key = 131 octets of 0xaa (LONGER than the 64-octet block, so RFC 2104 §2 hashes the key +// first), message = "Test Using Larger Than Block-Size Key - Hash Key First" data rfc4231_case1_key: MacKey = MacKey { id: "rfc4231-case1" as MacKeyId, @@ -38,6 +41,15 @@ data rfc4231_case2_key: MacKey = MacKey { data rfc4231_case2_message: NonEmptyStr = "what do ya want for nothing?" as NonEmptyStr data rfc4231_case2_tag: NonEmptyStr = "5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843" as NonEmptyStr +data rfc4231_case6_key: MacKey = MacKey { + id: "rfc4231-case6" as MacKeyId, + suite: HmacSha256, + material: "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa" as Secret, +} + +data rfc4231_case6_message: NonEmptyStr = "Test Using Larger Than Block-Size Key - Hash Key First" as NonEmptyStr +data rfc4231_case6_tag: NonEmptyStr = "60e431591ee0b67f0d8a26aacbf5b77f8e0bc6213728c5140546040f0ee37f54" as NonEmptyStr + // THE POSITIVE CONTROL, AND IT IS DOING REAL WORK HERE. Every refusal below is only informative if // the implementation can verify a tag it should. A verifier that answered false unconditionally // would pass every negative test in this file. @@ -104,7 +116,7 @@ test fn a_tag_does_not_verify_under_a_different_key() -> Bool { // ── A near-miss tag fails ──────────────────────────────────────────────────────────────────── // The published tag with its LAST character changed. A comparison that stopped early, truncated, // or compared a prefix would accept this. It is also the shape a timing attack produces on its -// final step, which is why the comparison is the library's constant-time one. +// final step, which is why mac_verify compares full-scan (extdeps.crypto.mac hmac_tag_difference). test fn a_tag_differing_in_one_character_fails() -> Bool { !mac_verification_ok( v: mac_verify( @@ -116,35 +128,55 @@ test fn a_tag_differing_in_one_character_fails() -> Bool { } // A TRUNCATED TAG IS NOT A PREFIX MATCH. Accepting a short tag that matches as far as it goes is -// the classic MAC-verification defect: it reduces the work of forging one to guessing a byte. +// the classic MAC-verification defect: it reduces the work of forging one to guessing a byte. It +// refuses as MacTagMalformed naming both lengths -- a length defect, not a mismatch. test fn a_truncated_tag_fails_rather_than_matching_a_prefix() -> Bool { - !mac_verification_ok( - v: mac_verify( - key: rfc4231_case1_key, - message: rfc4231_case1_message, - tag_hex: "b0344c61" as NonEmptyStr, - ) - ) + match mac_verify( + key: rfc4231_case1_key, + message: rfc4231_case1_message, + tag_hex: "b0344c61" as NonEmptyStr, + ) { + MacTagMalformed { octets_declared: d, octets_expected: x } => d == 4 && x == 32 + _ => false + } } -// ── Malformed input is not authentication ──────────────────────────────────────────────────── -// A key or tag that is not hex answers the same way a wrong tag does: not authenticated. The -// caller cannot distinguish them, which is deliberate -- reporting "your key was malformed" tells -// a prober their guess was at least well-formed. -test fn non_hex_key_and_tag_material_do_not_authenticate() -> Bool { - !mac_verification_ok( - v: mac_verify( - key: MacKey { id: "bad" as MacKeyId, suite: HmacSha256, material: "not-hex" as Secret }, - message: rfc4231_case1_message, - tag_hex: rfc4231_case1_tag, - ) - ) - && !mac_verification_ok( - v: mac_verify( - key: rfc4231_case1_key, - message: rfc4231_case1_message, - tag_hex: "zzzz" as NonEmptyStr, - ) +// ── Malformed input is refused, TYPED ──────────────────────────────────────────────────────── +// Undecodable input is never answered as a mismatch (gunbc#11628 qualification). A tag that is not +// lowercase hex is MacTagNotHex; key material that is not hex is MacKeyMaterialMalformed. Neither +// is authentication, and neither pretends to be a tag that happened not to match. +test fn a_non_hex_tag_refuses_as_not_hex() -> Bool { + match mac_verify(key: rfc4231_case1_key, message: rfc4231_case1_message, tag_hex: "zzzz" as NonEmptyStr) { + MacTagNotHex { key_id: k } => k == "rfc4231-case1" + _ => false + } +} + +test fn non_hex_key_material_refuses_as_malformed_key() -> Bool { + match mac_verify( + key: MacKey { id: "bad" as MacKeyId, suite: HmacSha256, material: "not-hex" as Secret }, + message: rfc4231_case1_message, + tag_hex: rfc4231_case1_tag, + ) { + MacKeyMaterialMalformed { key_id: k } => k == "bad" + _ => false + } +} + +// A well-formed tag that differs is the ONE case that is a mismatch -- pinned by arm, not only by +// "not ok", so a refactor that turns tampering into a refusal (or the reverse) is red. +test fn a_well_formed_wrong_tag_is_a_mismatch() -> Bool { + match mac_verify(key: rfc4231_case2_key, message: rfc4231_case1_message, tag_hex: rfc4231_case1_tag) { + MacTagMismatch { key_id: k } => k == "rfc4231-case2" + _ => false + } +} + +// THE LONG-KEY ARM. Case 6's key exceeds the block, so K0 = H(K) zero-extended. An implementation +// that zero-extended or truncated the raw key instead would produce a different tag. +test fn the_published_rfc4231_case6_long_key_vector_verifies() -> Bool { + mac_verification_ok( + v: mac_verify(key: rfc4231_case6_key, message: rfc4231_case6_message, tag_hex: rfc4231_case6_tag) ) } @@ -170,6 +202,7 @@ fn signed_hex(v: MacSigning) -> NonEmptyStr? { match v { MacSigned { tag: t } => Present { value: t.hex } MacKeyMaterialNotHex { key_id: _ } => none + MacComputationRefused { key_id: _, cause: _ } => none } } @@ -187,5 +220,6 @@ test fn mac_sign_refuses_key_material_that_is_not_hex() -> Bool { match mac_sign(key: unencoded, message: rfc4231_case2_message) { MacKeyMaterialNotHex { key_id: k } => k == unencoded.id MacSigned { tag: _ } => false + MacComputationRefused { key_id: _, cause: _ } => false } } 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..0584a27c8ba --- /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_octets(values: [256, 0, 0]) { + QualifiedOctetsRefused { cause: WordValueOutOfRange { width: _, value: v } } => v == 256 + QualifiedOctetsRefused { cause: _ } => false + QualifiedOctetsReady { octets: _ } => false + } +} + +test fn base64_encode_still_admits_the_byte_range_holds() -> Bool { + match base64_octets(values: [255, 0, 255]) { + QualifiedOctetsRefused { cause: _ } => false + QualifiedOctetsReady { octets: qualified } => base64_encode(octets: qualified, variant: Standard) == "/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 + }) +} + +// word_wrapping_add, word_rotate_right, word_xor and word_not left the expected set when gunbc#11647 +// landed their consumer (extdeps.crypto.sha2); that they are consumed is now evidenced by execution +// in test.claim.sha256_fips180_witness_test, not by a row. +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_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..8738039906b 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_octets(values: bs) { + QualifiedOctetsReady { octets: qualified } => base64_encode(octets: qualified, variant: UrlSafe) + QualifiedOctetsRefused { cause: _ } => "" + } Absent => "" } return { credential: cred } diff --git a/dag/test/claim/sha256_fips180_witness_test.dag b/dag/test/claim/sha256_fips180_witness_test.dag new file mode 100644 index 00000000000..a37f5adfef6 --- /dev/null +++ b/dag/test/claim/sha256_fips180_witness_test.dag @@ -0,0 +1,99 @@ +module test.claim.sha256_fips180_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.error_primitives { Result, Ok, Err } +import std.integer { UInt8 } +import std.machine_word { Word, Width32, WordReady, WordRefused, word_of_int } +import extdeps.numeric.base16 { base16_encode_lower } +import extdeps.crypto.sha2 { + Sha256Refusal, Sha256OctetOutOfRange, + sha256_octets, sha256_pad, sha256_small_sigma_0, +} +import std.logic { Bool } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// PUBLISHED VECTORS, NOT MEASUREMENTS. The three digests are the examples NIST publishes for +// FIPS 180-4 SHA-256 (csrc.nist.gov Cryptographic Standards and Guidelines, "Examples with +// Intermediate Values": SHA256.pdf) and the empty-input digest every implementation prints for +// zero octets. None was read back out of extdeps.crypto.sha2. Together they cover: zero octets +// (padding alone fills the block), a short one-block message, and a 56-octet message whose padding +// cannot fit in the first block, so a SECOND block is compressed with the chained hash value. +fn digest_hex(message: List) -> String { + match sha256_octets(message: message) { + Ok { value: d } => base16_encode_lower(octets: d) + Err { value: _ } => "refused" + } +} + +// "abc" as octets: 0x61 0x62 0x63. +test fn the_published_abc_digest_holds() -> Bool { + digest_hex(message: [97, 98, 99]) == "ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad" +} + +test fn the_empty_message_digest_holds() -> Bool { + digest_hex(message: []) == "e3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855" +} + +// "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq": fourteen overlapping four-letter +// windows starting at a, b, c, ... n. Spelled as its octets so no String encoding is under test here. +fn two_block_message() -> List { + [ + 97, 98, 99, 100, 98, 99, 100, 101, 99, 100, 101, 102, 100, 101, 102, 103, + 101, 102, 103, 104, 102, 103, 104, 105, 103, 104, 105, 106, 104, 105, 106, 107, + 105, 106, 107, 108, 106, 107, 108, 109, 107, 108, 109, 110, 108, 109, 110, 111, + 109, 110, 111, 112, 110, 111, 112, 113, + ] +} + +test fn the_published_two_block_digest_holds() -> Bool { + digest_hex(message: two_block_message()) == "248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1" +} + +// PADDING SHAPE (§5.1.1), pinned separately from the digest so a padding defect is located here +// rather than only as a wrong digest. 3 octets pad to one 64-octet block; 56 octets pad to two, +// because 56 + 1 + 8 exceeds 64. The last octet of "abc"'s padding is the bit length, 24. +test fn padding_block_counts_hold() -> Bool { + match sha256_pad(message: [97, 98, 99]) { + Err { value: _ } => false + Ok { value: one } => + list_length(items: one) == 64 + && octet_at_is(xs: one, index: 3, expected: 128) + && octet_at_is(xs: one, index: 63, expected: 24) + && match sha256_pad(message: two_block_message()) { + Err { value: _ } => false + Ok { value: two } => list_length(items: two) == 128 && octet_at_is(xs: two, index: 127, expected: 192) + } + } +} + +fn octet_at_is(xs: List, index: Int, expected: Int) -> Bool { + match get(xs: xs, index: index) { + Present { value: v } => v == expected + Absent => false + } +} + +// σ0 ON THE FIRST INITIAL-HASH WORD, the value NUMERIC-BIT-0's witness pins for the same shape +// (std.machine_word sha2_small_sigma_zero_shape_holds: rotr7 ⊕ rotr18 ⊕ shr3 of 0x6a09e667 = +// 3121411458). Pinned here against THIS module's sigma so swapping a rotate for a shift, or the +// amounts between the lower- and upper-case functions, is red at the function rather than only in +// a digest. +test fn small_sigma_zero_matches_the_substrate_pin() -> Bool { + match word_of_int(width: Width32, value: 1779033703) { + WordRefused { cause: _ } => false + WordReady { word: x } => + match sha256_small_sigma_0(x: x) { + WordRefused { cause: _ } => false + WordReady { word: y } => y.value == 3121411458 + } + } +} + +// AN OCTET OUT OF RANGE REFUSES, it is not reduced modulo 256: 256 is not an octet. +test fn an_out_of_range_octet_refuses() -> Bool { + match sha256_octets(message: [97, 256]) { + Err { value: Sha256OctetOutOfRange { value: v } } => v == 256 + _ => false + } +} diff --git a/dag/test/claim/utf8_encode_rfc3629_witness_test.dag b/dag/test/claim/utf8_encode_rfc3629_witness_test.dag new file mode 100644 index 00000000000..d5a655c055f --- /dev/null +++ b/dag/test/claim/utf8_encode_rfc3629_witness_test.dag @@ -0,0 +1,60 @@ +module test.claim.utf8_encode_rfc3629_witness_test + +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import std.error_primitives { Result, Ok, Err } +import std.encoding { + Utf8SurrogateRefused, Utf8OutOfRangeRefused, + utf8_encode_code_point, utf8_encode_octets, +} +import std.logic { Bool } + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +// RFC 3629 §3 encodes a scalar in one to four octets by its range. One scalar per length class, +// each at a value whose octets are published in the RFC's own §7 examples or are the class +// boundary, and expected octets written from the §3 table -- not read back from std.encoding. + +// U+0041 'A' → 41 (one octet; ASCII is its own encoding). +test fn one_octet_class_holds() -> Bool { + utf8_encode_code_point(cp: 65) == Ok { value: [65] } +} + +// U+00E9 'é' → C3 A9 (two octets). +test fn two_octet_class_holds() -> Bool { + utf8_encode_code_point(cp: 233) == Ok { value: [195, 169] } +} + +// U+20AC '€' → E2 82 AC (three octets). +test fn three_octet_class_holds() -> Bool { + utf8_encode_code_point(cp: 8364) == Ok { value: [226, 130, 172] } +} + +// U+1F600 → F0 9F 98 80 (four octets). +test fn four_octet_class_holds() -> Bool { + utf8_encode_code_point(cp: 128512) == Ok { value: [240, 159, 152, 128] } +} + +// Class boundaries: the last of each class stays in it. 0x7F, 0x7FF, 0xFFFF, 0x10FFFF. +test fn class_boundaries_hold() -> Bool { + utf8_encode_code_point(cp: 127) == Ok { value: [127] } + && utf8_encode_code_point(cp: 2047) == Ok { value: [223, 191] } + && utf8_encode_code_point(cp: 65535) == Ok { value: [239, 191, 191] } + && utf8_encode_code_point(cp: 1114111) == Ok { value: [244, 143, 191, 191] } +} + +// Surrogates have no UTF-8 encoding (RFC 3629 §3); above U+10FFFF is not a scalar at all. +test fn surrogates_and_out_of_range_refuse() -> Bool { + match utf8_encode_code_point(cp: 55296) { + Err { value: Utf8SurrogateRefused { cp: c } } => c == 55296 + _ => false + } + && match utf8_encode_code_point(cp: 1114112) { + Err { value: Utf8OutOfRangeRefused { cp: c } } => c == 1114112 + _ => false + } +} + +// THE STRING ROUTE, the one extdeps.crypto.mac consumes: a String's scalars, in order, each encoded. +test fn a_mixed_string_encodes_in_order() -> Bool { + utf8_encode_octets(s: "Aé€") == Ok { value: [65, 195, 169, 226, 130, 172] } +} diff --git a/docs/plans/blackjack-onboarding.md b/docs/plans/blackjack-onboarding.md index d33b3b8f8ee..7af949d3c1e 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_decode } 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, already admitted as octets by the decoder, and a fold +// combines them. Take the real decoded type here -- do not mint an Int list, and do not re-admit +// what the decoder has already established. 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 folds over those octets — 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. diff --git a/src/v1/04_method.dag b/src/v1/04_method.dag index d26220ad5b0..4c20de6fdc1 100644 --- a/src/v1/04_method.dag +++ b/src/v1/04_method.dag @@ -269,8 +269,6 @@ fn builtin_kernel_seed_diagnostics() -> List { // One word "declared" covering all four would be the rung inflation the ladder names. data builtin_function_registry: Map = { "count": derived_signature(names: ["xs"], method: "count", returns: int_type), - "hmac_sha256_verify_hex": BuiltinSignature { params: [BuiltinParam { name: "key_hex", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "message", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "tag_hex", ty: NamedTemplate { name: "String" } }], returns: bool_type }, - "hmac_sha256_hex": BuiltinSignature { params: [BuiltinParam { name: "key_hex", ty: NamedTemplate { name: "String" } }, BuiltinParam { name: "message", ty: NamedTemplate { name: "String" } }], returns: with_optional_cardinality(n: string_type) }, "string_length": BuiltinSignature { params: [BuiltinParam { name: "s", ty: NamedTemplate { name: "String" } }], returns: int_type }, "code_point": BuiltinSignature { params: [BuiltinParam { name: "c", ty: NamedTemplate { name: "String" } }], returns: int_type }, "to_int": derived_signature(names: ["s"], method: "to_int", returns: int_type), diff --git a/src/v1/stage0/Cargo.toml b/src/v1/stage0/Cargo.toml index 0c1be947195..2e5d49a2ab5 100644 --- a/src/v1/stage0/Cargo.toml +++ b/src/v1/stage0/Cargo.toml @@ -48,7 +48,6 @@ clap = { version = "4", features = ["derive"] } lazy_static = "1" serde = { version = "1", features = ["derive", "rc"] } serde_json = "1" -hmac = { workspace = true } hex = { workspace = true } sha2 = "0.10" toml = { workspace = true } diff --git a/src/v1/stage0/src/v1_compiler_infer_method.rs b/src/v1/stage0/src/v1_compiler_infer_method.rs index 59d9334e75f..12271b5b459 100644 --- a/src/v1/stage0/src/v1_compiler_infer_method.rs +++ b/src/v1/stage0/src/v1_compiler_infer_method.rs @@ -256,39 +256,6 @@ pub fn builtin_function_registry() -> Rc>> static CACHED: Rc>> = { let mut __m = HashMap::new(); __m.insert("count".to_string(), derived_signature(Rc::new(vec!["xs".to_string()]), "count".to_string(), int_type())); - __m.insert("hmac_sha256_verify_hex".to_string(), Rc::new(BuiltinSignature { - params: Rc::new(vec![Rc::new(BuiltinParam { - name: "key_hex".to_string(), - ty: Rc::new(AlgebraTypeTemplate::NamedTemplate { - name: "String".to_string(), - }), - }), Rc::new(BuiltinParam { - name: "message".to_string(), - ty: Rc::new(AlgebraTypeTemplate::NamedTemplate { - name: "String".to_string(), - }), - }), Rc::new(BuiltinParam { - name: "tag_hex".to_string(), - ty: Rc::new(AlgebraTypeTemplate::NamedTemplate { - name: "String".to_string(), - }), - })]), - returns: bool_type(), - })); - __m.insert("hmac_sha256_hex".to_string(), Rc::new(BuiltinSignature { - params: Rc::new(vec![Rc::new(BuiltinParam { - name: "key_hex".to_string(), - ty: Rc::new(AlgebraTypeTemplate::NamedTemplate { - name: "String".to_string(), - }), - }), Rc::new(BuiltinParam { - name: "message".to_string(), - ty: Rc::new(AlgebraTypeTemplate::NamedTemplate { - name: "String".to_string(), - }), - })]), - returns: crate::v1_std_core::with_optional_cardinality(string_type()), - })); __m.insert("string_length".to_string(), Rc::new(BuiltinSignature { params: Rc::new(vec![Rc::new(BuiltinParam { name: "s".to_string(), diff --git a/src/v1/stage0/src/v1_interpreter.rs b/src/v1/stage0/src/v1_interpreter.rs index d2ac5dba487..a1159dc0107 100644 --- a/src/v1/stage0/src/v1_interpreter.rs +++ b/src/v1/stage0/src/v1_interpreter.rs @@ -19831,69 +19831,6 @@ macro_rules! v1_builtin_arms { None => Ok(None), }, - // THE ONE PLACE A MAC IS ACTUALLY COMPUTED, and it is a host builtin rather than a - // shell transport for a specific reason: every shell form of HMAC - // (`openssl dgst -hmac `) puts the KEY IN THE ARGV, which is the exposure - // gunbc.credential_argv_exposure exists to forbid. A process listing is enough to - // learn a signing key, and with a symmetric MAC the signing key is also the - // verification key, so leaking it forges approvals rather than merely reading them. - // - // The comparison is RustCrypto's `verify_slice`, not an equality on bytes we - // computed. That is the whole reason extdeps.crypto.mac exposes no accessor for a - // computed tag: an ordinary `==` over MAC bytes leaks, through timing, how many - // leading bytes of a forged tag were correct, which turns forging a 32-byte tag from - // infeasible into a few thousand requests. - // - // Key and tag arrive as lowercase hex because the corpus already models digests that - // way (extdeps.crypto.hash Digest.hex) and hex has one spelling per value -- base64 - // has several, and a decoder that accepts more spellings than it should is how one - // envelope acquires two representations. - // - // Every malformed input answers FALSE rather than raising: a caller cannot tell a - // bad key encoding from a wrong tag, which is correct here, because both mean the - // same thing to the only consumer -- this message is not authenticated. - arm "free_call.hmac_sha256_verify_hex" { "hmac_sha256_verify_hex" } => { - use hmac::{Hmac, Mac}; - use sha2::Sha256; - let key_hex = expect_value_str($positional.first().copied(), "hmac_sha256_verify_hex key")?; - let message = expect_value_str($positional.get(1).copied(), "hmac_sha256_verify_hex message")?; - let tag_hex = expect_value_str($positional.get(2).copied(), "hmac_sha256_verify_hex tag")?; - let key = match hex::decode(key_hex.as_str()) { - Ok(k) => k, - Err(_) => return Ok(Some(Value::Bool(false))), - }; - let tag = match hex::decode(tag_hex.as_str()) { - Ok(t) => t, - Err(_) => return Ok(Some(Value::Bool(false))), - }; - let mut mac = match Hmac::::new_from_slice(&key) { - Ok(m) => m, - Err(_) => return Ok(Some(Value::Bool(false))), - }; - mac.update(message.as_str().as_bytes()); - Ok(Some(Value::Bool(mac.verify_slice(&tag).is_ok()))) - }, - - // ISSUANCE, THE KEY HOLDER'S OWN OPERATION, and a second primitive rather than a - // widening of verify: the verify arm above deliberately yields one bit, so a verifier - // is never handed a computed tag to compare in variable time. Minting is the only - // purpose a computed tag has, and with a symmetric MAC only the key holder (the - // broker) can perform it (extdeps.crypto.mac symmetric_verification_is_issuance_note). - // - // Same RustCrypto Hmac, same hex key spelling as verify. A key that is not - // hex answers ABSENT (the optional's null), never a tag: there is no key to have - // signed with, and a fabricated tag would be a plausible output standing where a - // refusal belongs. extdeps.crypto.mac mac_sign turns that absence into its typed arm. - arm "free_call.hmac_sha256_hex" { "hmac_sha256_hex" } => { - Ok(Some(match hmac_sha256_hex_tag( - expect_value_str($positional.first().copied(), "hmac_sha256_hex key")?.as_str(), - expect_value_str($positional.get(1).copied(), "hmac_sha256_hex message")?.as_str(), - ) { - Some(tag) => str_value(tag), - None => Value::Null, - })) - }, - arm "free_call.string_length" { "string_length" } => { let s = expect_value_str($positional.first().copied(), "string_length")?; Ok(Some(Value::Int(s.string_length()))) @@ -22563,48 +22500,6 @@ fn expect_string(val: &Value, context: &str) -> InterpResult { } } -/// The `hmac_sha256_hex` builtin's computation: the lowercase hex HMAC-SHA256 tag of `message` -/// under the hex-encoded key, or `None` when the key is not hex -- no key, no tag. -fn hmac_sha256_hex_tag(key_hex: &str, message: &str) -> Option { - use hmac::{Hmac, Mac}; - use sha2::Sha256; - let key = hex::decode(key_hex).ok()?; - let mut mac = Hmac::::new_from_slice(&key).ok()?; - mac.update(message.as_bytes()); - Some(hex::encode(mac.finalize().into_bytes())) -} - -#[cfg(test)] -mod hmac_sha256_hex_tests { - use super::hmac_sha256_hex_tag; - - // RFC 4231 publishes these so an implementation is checked against values it did not produce. - #[test] - fn rfc4231_case1_tag_is_produced() { - assert_eq!( - hmac_sha256_hex_tag("0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b0b", "Hi There").as_deref(), - Some("b0344c61d8db38535ca8afceaf0bf12b881dc200c9833da726e9376c2e32cff7"), - ); - } - - #[test] - fn rfc4231_case2_tag_is_produced() { - assert_eq!( - hmac_sha256_hex_tag("4a656665", "what do ya want for nothing?").as_deref(), - Some("5bdcc146bf60754e6a042426089575c75a003f089d2739839dec58b964ec3843"), - ); - } - - #[test] - fn a_key_that_is_not_hex_yields_no_tag() { - assert_eq!( - hmac_sha256_hex_tag("Jefe", "what do ya want for nothing?"), - None - ); - assert_eq!(hmac_sha256_hex_tag("0b0", "Hi There"), None); - } -} - /// Like `expect_str`, but returns the `Value::Str` carrier itself instead of an owned /// copy: the caller gets the `&str` view AND the carried ASCII fact, and pays no O(n) /// `.to_string()` for a read-only use (STRING-INDEX-0). diff --git a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs index e6ed1063c6a..6802f2e57f2 100644 --- a/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs +++ b/src/v1/stage0/src/v1_interpreter_dispatch_generated.rs @@ -21,8 +21,6 @@ pub enum EvalBuiltinArm { FreeCallConcat, FreeCallCount, FreeCallReverse, - FreeCallHmacSha256VerifyHex, - FreeCallHmacSha256Hex, FreeCallStringLength, FreeCallSubstring, FreeCallCharAt, @@ -166,8 +164,6 @@ pub fn lookup_eval_builtin_inner(spelling: &str) -> Option { "concat" => Some(EvalBuiltinArm::FreeCallConcat), "count" => Some(EvalBuiltinArm::FreeCallCount), "reverse" => Some(EvalBuiltinArm::FreeCallReverse), - "hmac_sha256_verify_hex" => Some(EvalBuiltinArm::FreeCallHmacSha256VerifyHex), - "hmac_sha256_hex" => Some(EvalBuiltinArm::FreeCallHmacSha256Hex), "string_length" => Some(EvalBuiltinArm::FreeCallStringLength), "substring" => Some(EvalBuiltinArm::FreeCallSubstring), "char_at" => Some(EvalBuiltinArm::FreeCallCharAt), @@ -315,8 +311,6 @@ macro_rules! eval_builtin_inner_arm { ("free_call.concat") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallConcat }; ("free_call.count") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallCount }; ("free_call.reverse") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallReverse }; - ("free_call.hmac_sha256_verify_hex") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallHmacSha256VerifyHex }; - ("free_call.hmac_sha256_hex") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallHmacSha256Hex }; ("free_call.string_length") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallStringLength }; ("free_call.substring") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallSubstring }; ("free_call.char_at") => { $crate::v1_interpreter_dispatch_generated::EvalBuiltinArm::FreeCallCharAt };