def word_of

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/aes/gcm.bend:34

import Base

34# The first n bits of a bit string, zero-filled.
35def word_of(n: Nat, bs: List<&2, Bool>) -> Word(n):
36  match n bs:
37    case 0n _:
38      WNil{}
39    case 1n+p Nil{}:
40      WCon{False{}, word_of(p, Nil{})}
41    case 1n+p b <> rest:
42      WCon{b, word_of(p, rest)}