def double_rounds
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8randimport Base
86def double_rounds(n: Nat, x: List<&2, U32>) -> List<&2, U32>:
87 match n:
88 case 0n:
89 x
90 case 1n+p:
91 double_rounds(p, double_round(x))
Uses (4)
Used by (4)
- bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block:block_correct
- bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block:drs_correct
- bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block:rounds_correct
- bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand:chacha8