def step_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/random/bytes.bend:108

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as C8
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as CR
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as SRC
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as SCR

108def step_nil(+j: Nat, +acc: List<&2, U32>, q: W.U64 & C8.ChaCha8) -> {SCR.append(rev(facc(CR.split(acc, q))), SCR.take(j, SCR.append(fpend(CR.split(acc, q)), SCR.flat(outs(j, fsrc(CR.split(acc, q))))))) == SCR.append(rev(acc), SCR.take(1n+j, SCR.flat(Con{SRC.fst64(C8.ChaCha8, q), outs(j, SRC.snd64(C8.ChaCha8, q))}))) : List<&2, U32>}:
109  match q:
110    case Tuple{x, +c1}:
111      match x:
112        case W.U64{+l, +h}:
113          +r7 = {[U32.and(U32.shrn(l, 8n), 255), U32.and(U32.shrn(l, 16n), 255), U32.and(U32.shrn(l, 24n), 255), U32.and(h, 255), U32.and(U32.shrn(h, 8n), 255), U32.and(U32.shrn(h, 16n), 255), U32.and(U32.shrn(h, 24n), 255)] : List<&2, U32>}
114          rev_cons(U32.and(l, 255), acc, SCR.take(j, SCR.append(r7, SCR.flat(outs(j, c1)))))