def le_bytes

bend-collections-laws-crypto@1.0.0.0 · spec/crypto/poly1305.bend:58

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C

58# num_to_n_le_bytes: the low n bytes of x.
59def le_bytes(n: Nat, +x: Nat) -> List<&2, U32>:
60  match n:
61    case 0n: Nil{}
62    case 1n+k: U32.from_nat(C.low(8n, x)) <> le_bytes(k, C.high(8n, x))