def block_rounds

bend-collections@1.0.0.0 · src/crypto/chacha/chacha20.bend:94

import Base

94# The block function entered through a match on the key's first cell: both
95# arms are block_body; with a symbolic key the proof checker leaves the call
96# unevaluated instead of unrolling the rounds when it compares types.
97def block_rounds(+r: Nat, key_bytes: List<&2, U32>, counter: U32, nonce_bytes: List<&2, U32>) -> List<&2, U32>:
98  match key_bytes:
99    case Nil{}: block_body(r, Nil{}, counter, nonce_bytes)
100    case b <> rest: block_body(r, b <> rest, counter, nonce_bytes)