std.crypto: SHA-512, and the logical shift it needed

Status: built, second slice of the initiative docs/crypto.md opened.

crypto.md §7 named this as the next real consumer’s dependency — lex-os-capsule’s Ed25519 signing needs SHA-512, not SHA-256, per RFC 8032 — and said nothing here should be read as scoping Ed25519 itself in advance. It still isn’t. This document is SHA-512 alone, and §5 below is explicit about how much of Ed25519 remains unstarted after it.

1. Same algorithm, different word width

SHA-512 is FIPS 180-4’s other hash: eighty rounds instead of sixty-four, 128-byte blocks instead of 64, eight 64-bit running words instead of eight 32-bit ones, and a 128-bit big-endian bit-length field instead of a 64-bit one. compress512 in std/crypto.cho is structurally compress again — same message-schedule shape, same eight-variable round, same eight-word finalization — at the wider width, and sha512’s own padding is sha256’s padding with 9 replaced by 17 (1 byte for 0x80, 16 for the length, not 8) and 64 replaced by 128.

sha512_h0 and sha512_k are FIPS 180-4’s own words: the first eight primes’ square roots and the first eighty primes’ cube roots, fractional part, 64 bits each. Independently derived here — an integer square root and a binary-searched integer cube root over p * 2^128 and p * 2^192 respectively, not a memorised or copied table — and then checked the only way that means anything for a hash function: run through Python’s own hashlib.sha512 on four inputs and matched byte for byte, and separately against the system sha512sum on the same four inputs. Both agree with each other and with §4 below.

2. The word width that helped SHA-256 is exactly what breaks here

crypto.md §2’s whole design was possible only because a SHA-256 word lives in [0, 0xffffffff], comfortably inside this language’s 64-bit int — with 32 bits of headroom above it to mask into and mask out of. A SHA-512 word is the int width. There is no headroom, and two real consequences follow from having none.

wrapping_add replaces mask32(checked +) outright, and this is the easy consequence. mod 2^64 is not a mask applied after a checked add any more — it is what wrapping_add already computes, on the exact bits a 64-bit word has. Nothing here needed not32’s workaround either: ~e is the true 64-bit complement the round function wants, because unlike SHA-256’s masked word, a SHA-512 word has no bits above it for ~ to wrongly flip.

Every rotate and every shift SHA-512 needs is now a logical one — zero-filling — and this language’s >> is arithmetic, sign-extending, by design (docs/bitwise.md §2: “it will be arithmetic; int is signed”, with unsigned integers, and a logical >> on them, named as future work). SHA-256’s rotr32 never had to face this: every word it rotates is confined to [0, 0xffffffff] by mask32, which as a 64-bit int is always non-negative, so an arithmetic and a logical shift agree on it by construction — the gap was there the whole time, invisible because nothing SHA-256 does ever sets the sign bit of a value it then shifts. A SHA-512 word is the full 64 bits and routinely has its own top bit set (sha512_h0[1], 0xbb67ae8584caa73b, is one), and rotr64/s0/s1/S0/S1 all need the true bit pattern shifted, not a sign-extended one.

The fix does not need a new operator. x >> n already has the correct low 64 - n bits of a logical shift regardless of x’s sign — sign-extension only ever writes the top n bits, which a logical shift would have zeroed. So:

fn low_mask64(k: int) -> [] int {
    if k == 63 { return 0x7fffffffffffffff; }
    return (1 << k) - 1;
}

fn lshr64(x: int, n: int) -> [] int {
    return (x >> n) & low_mask64(64 - n);
}

fn rotr64(x: int, n: int) -> [] int {
    return lshr64(x, n) | (x << (64 - n));
}

masking off exactly the bits sign-extension might have gotten wrong turns the arithmetic shift already available into the logical one needed. rotr64’s two halves need no mask of their own the way rotr32’s masked | does: lshr64(x, n) zero-fills its own top n bits and x << (64 - n) zero-fills its own bottom 64 - n bits (docs/bitwise.md §4 — a left shift never traps on the bit pattern it produces), so the two ranges are disjoint and the | just is the rotate.

low_mask64’s own k == 63 branch is the one place this still bites: (1 << 63) - 1 is not 0x7fffffffffffffff, because 1 << 63 is int::MIN’s bit pattern and subtracting one from it is ordinary checked arithmetic, which underflows and traps (docs/defined-behaviour.md). rotr64(x, 1) is the one call site in this file that reaches low_mask64(63), so the trap is not hypothetical — it is written as the literal instead, which is what the value always was.

A related, and separate, gap: a 64-bit literal with the top bit set does not parse. sha512_h0’s and sha512_k’s tables include values like 0xbb67ae8584caa73b, which is int::MIN-or-past as a plain literal — and this language refuses it at the literal, the same way (1 << 63) - 1 is refused at the subtraction, not accepted and then misread. Every such constant here is written as (hi << 32) | lo instead, splitting it into two 32-bit halves that are always comfortably positive literals — a mechanical, checkable transform (each half reconstructed and compared against the original 64-bit value before being written down), not a judgement call made per-constant. Twenty-two of the eighty-eight words in sha512_h0 and sha512_k need it; the other sixty-six could have been written as plain literals and are spelled the same way anyway, so the file has one rule rather than two.

3. The length field is 128 bits; this language’s int is not

FIPS 180-4 §5.1.2 appends a 16-byte big-endian bit-length. sha512 writes only the low 8 of those 16 bytes — total * 8 is a 64-bit int, and the high 8 bytes of the field stay at alloc_slice’s own zero fill. This is exact, not truncated, for every message this language can hold at all: a slice’s length is itself an int, so total is already bounded by the same 64-bit ceiling bit_len = total * 8 would need eleven more bits of headroom to approach, and * is checked — a message long enough to need those upper 8 bytes traps computing total * 8 before sha512 could write a wrong length field, rather than silently wrapping past it. The honest statement is not “this cannot happen,” it is “this language could not hand sha512 a message big enough for it to matter, and if it somehow could, sha512 would refuse rather than mismeasure.”

Corrected by docs/hkdf.md §2. The length field is right, but “every message this language can hold” was false: sha512 copied the padded message into a 64 KiB arena and trapped at 65,536 bytes, long before the length field could matter. It streams now (sha512_init/update/final), and FIPS 180-4’s million-a example passes.

4. Checked, not assumed

Four vectors, matched against Python’s own hashlib.sha512 and, separately, the system sha512sum — not transcribed from either:

The 112-byte vector is the one that matters most, the same reason crypto.md’s 56-byte SHA-256 vector does: "" and "abc" both pad into exactly one 128-byte block, so neither exercises the multi-block path. 112 + 17 = 129 > 128 is the smallest input that does, mirroring SHA-256’s 56 + 9 = 65 > 64 at the wider width.

tests/accept/sha512.cho checks all four, byte-for-byte, through --std, on both backends — the_two_backends_agree_on_sha512 in crates/cancho/tests/conformance/backends.rs.

std_declarations_cost_nothing_unless_called (docs/crypto.md §6) needed nothing new here: sha512_h0/sha512_k are reachability-gated by the same fold::collect_static_refs pass §6 built for sha256_h0/sha256_k, which is exactly the case it was built to generalize rather than a second one to find.

5. What is next, and what this slice deliberately does not touch

SHA-512 is a hash function: no key, no secret, and getting it wrong produces a wrong digest that the vectors above would have caught. Ed25519 is a signature scheme with a private key to keep secret and a curve to get right, and crypto.md §1 already drew this line once — “hashing and signing are different primitives with different failure modes” — before there was a second hash function to make the point with a second example.

What Ed25519 needs beyond this slice, named rather than started:

• Field arithmetic over GF(2^255 - 19). std.bignum (std/bignum.cho) is the closest thing this language has to the bignum Ed25519’s field arithmetic needs, and it is not that thing yet: mul_small multiplies by a machine-word multiplier, not by a second bignum, and there is no modular reduction at all, let alone one shaped for this prime’s own reduction trick (2^255 ≡ 19 mod p). Full multiply and a reduction step are new code, not an extension of what is there.
• Point arithmetic on the twisted Edwards curve, and the encode/ decode of a compressed point (a sign bit folded into the top bit of the y-coordinate’s byte representation) that Ed25519’s own wire format is built on.
• Scalar multiplication and clamping, and the deterministic nonce derivation RFC 8032 specifies (itself a SHA-512 call — the one concrete link back to this slice).
• A constant-time posture worth stating honestly, not assuming. ed25519-dalek, what lex-os-capsule calls today, is written to make key-dependent branching and key-dependent memory access patterns hard to introduce by accident. Nothing forces the same property here yet — this language’s checked-arithmetic traps and ordinary if/match control flow are not designed against timing side channels, and a first correct-by-vectors implementation should not be read as a constant-time one until that is checked specifically, the same way low_mask64’s trap and the literal-parse gap above were each checked specifically rather than assumed away.

None of this is scoped further here on purpose, for the same reason crypto.md §1 gave for not scoping Ed25519 in general: each is its own correctness surface, and bundling the scoping with the one primitive this slice actually finishes is exactly the premature-scope mistake both documents are refusing.