def fill_inv

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

import Base
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/crypto/random.bend as SCR

131# THEOREM: after k bytes the accumulator, read back, is the old one followed
132# by the first k bytes of the pending bytes and the stream
133def fill_inv(+k: Nat, +f: CR.Fill) -> {rev(facc(CR.fill(k, f))) == SCR.append(rev(facc(f)), SCR.take(k, SCR.append(fpend(f), SCR.flat(outs(k, fsrc(f)))))) : List<&2, U32>}:
134  match k:
135    case 0n:
136      Equal.sym(List<&2, U32>, SCR.append(rev(facc(f)), []), rev(facc(f)), app_nil(rev(facc(f))))
137    case 1n+j:
138      Equal.trans(List<&2, U32>, rev(facc(CR.fill(j, CR.take1(f)))), SCR.append(rev(facc(CR.take1(f))), SCR.take(j, SCR.append(fpend(CR.take1(f)), SCR.flat(outs(j, fsrc(CR.take1(f))))))), SCR.append(rev(facc(f)), SCR.take(1n+j, SCR.append(fpend(f), SCR.flat(outs(1n+j, fsrc(f)))))),
139        fill_inv(j, CR.take1(f)),
140        step(j, f))