Block.drs: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend as Block
Lines 10-16 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend&start_line=10&end_line=16

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

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

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=Vector
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend&name=dr