def drs_correct

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

import Base
import bend-collections-laws-math@1.0.0.0/src/math/random/chacha8/block.bend as B
import bend-collections-laws-math@1.0.0.0/spec/math/random/chacha8rand.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/rounds.bend as R

18def drs_correct(+n: Nat, +v: B.Vector) -> {R.vec(drs(n, v)) == S.double_rounds(n, R.vec(v)) : List<&2, U32>}:
19  match n:
20    case 0n:
21      {==}
22    case 1n+p:
23      Equal.trans(List<&2, U32>, R.vec(drs(p, B.dr(v))), S.double_rounds(p, R.vec(B.dr(v))), S.double_rounds(p, S.double_round(R.vec(v))),
24        drs_correct(p, B.dr(v)),
25        Equal.cong(List<&2, U32>, List<&2, U32>, x => S.double_rounds(p, x), R.vec(B.dr(v)), S.double_round(R.vec(v)), R.dr_correct(v)))