33.6Vector Crypto XIII: The Formal Sail Model

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

The chapter closes with the supporting Sail code — the executable definitions of the element-group accessors and crypto helpers every instruction operation referenced.

What the vector-crypto Sail defines
Function group
Element-group accessget_velem / set_velem at EGW=128 or 256 — the mapping from a logical element group onto the vector register’s bytes, and the vl/EGS, vstart/EGS loop bounds.
AES helpersShared with the scalar model: SBox forward/inverse, ShiftRows, MixColumns, GF(2⁸) arithmetic — now applied per lane group.
GF(2^128) for GHASHThe carry-less multiply and polynomial reduction that vghsh/vgmul (and the vclmul route) compute.
SHA / SM3 / SM4 transformsThe σ/Σ compositions, SM3 P0/P1, SM4 SBox + linear layers — the same primitives as the scalar chapter, vectorized.
Dotted-underlined cells have explanations — click one.

The element-group accessors are the vector-specific addition: they pin exactly how a 128-bit AES block or 256-bit SHA-512 state occupies the vector register bytes, so foreach i in vstart/EGS .. vl/EGS reads and writes the right bits. Everything else reuses the scalar crypto model’s helpers (u32 §32.9) — the Sail is ground truth, and the full RISC-V Sail model executes it.

Hardware Designer Notes

That completes vector cryptography: the extension map, the AES/SHA/ GCM/SM instruction references, the constant-time contract, and the formal model. The whole chapter is the scalar-crypto datapath replicated across the V extension’s lanes — big silicon for big throughput, whose difficulty is constant-time timing plus getting the element-group byte mapping exactly right, which the Sail model exists to guarantee.

Minimal Linux-boot hart MUST

  • Verify RTL against Sail-generated vectors spanning VLEN, LMUL, and element-group boundary conditions — not just algorithm test vectors
  • Match the element-group byte mapping exactly; a reflection or lane-order bug is silent until it corrupts specific configurations

MAY simplify / trap-and-emulate

  • Auto-generate SBox/GF logic and element-group addressing from the Sail definitions

Check yourself — vector crypto Sail model

1.The §33.6 Sail code defines helpers like get_velem and the element-group accessors. Why are these central to vector crypto's formal spec?

2.How should a hardware team use the vector-crypto Sail model?

2 questions