def sbox

bend-collections-laws-crypto@1.0.0.0 · src/crypto/aes/sbox.bend:140

import Base

140# The S-box. (The one-constructor match only opens the U32, no branch: it
141# keeps a proof about an unknown word from expanding the 117 gates.)
142def sbox(x: U32) -> U32:
143  match x:
144    case U32{w}: sbox_word(U32{w})