32.9Scalar Crypto XIII: The Formal Sail Specification

Part III Linux boot: optional Vol. I (Unprivileged) pp. 462–469 · ~2 min read

The chapter closes with the supporting Sail code (§32.8-32.9) — the executable, machine-checkable definitions of the helper functions every crypto instruction description referenced by name.

What the supplementary Sail defines
Function group
AES primitivesaes_sbox_fwd / aes_sbox_inv (the 256-entry substitution tables), aes_mixcolumn helpers, aes_shift_rows, and the GF(2⁸) arithmetic (xtime, field multiply) underneath.
SM4 primitivessm4_sbox and the linear-layer constants — SM4’s own field and affine, distinct from AES.
SHA / SM3 transformsThe rotate/shift compositions are simple enough to appear inline in each instruction, but the shared rotate helpers (ror32/rol32) are defined here.
Rounding / utilityEXTS/EXTZ sign/zero-extension and the byte-select shifts the RV32 instructions use.
Dotted-underlined cells have explanations — click one.

The design principle: each instruction’s description shows the operation in a few lines of Sail (byte select, call the SBox, XOR into rs1), while the verbose constant tables live once in §32.9. The prose conveys intent; the Sail is ground truth — what a verification engineer tests against, and what the full RISC-V Sail model executes.

Hardware Designer Notes

That completes the scalar cryptography chapter: seven instruction reference pages, the entropy source, the constant-time contract, the rationale, and the formal model. The whole extension is small silicon (one AES SBox dominates the area) whose difficulty is entirely in the two non-functional properties — constant-time timing and certified entropy — plus getting the SBox bits exactly right, which the Sail model exists to guarantee.

Minimal Linux-boot hart MUST

  • Verify RTL against the Sail model’s generated vectors, not a hand-transcribed table — SBox transcription errors are silent and catastrophic
  • Match the field arithmetic exactly (AES and SM4 use different GF(2⁸) representations)

MAY simplify / trap-and-emulate

  • Auto-generate the SBox ROM and MixColumns logic from the Sail definitions to eliminate transcription risk

Check yourself — formal Sail specification

1.What is the Sail code in §32.9, and why is it authoritative?

2.A verification engineer needs the exact AES forward SBox values. Where does the spec put them?

2 questions