def drs

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/chacha8/block.bend:10

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as B

10# n double rounds, the model of the implementation's dr(dr(dr(dr(x))))
11def drs(n: Nat, v: B.Vector) -> B.Vector:
12  match n:
13    case 0n:
14      v
15    case 1n+p:
16      drs(p, B.dr(v))