def inv

bend-collections-laws-math@1.0.0.0 · proofs/math/random/chacha8/stream.bend:57

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
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/src/math/random/chacha8.bend as C8
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/spec/math/random/source.bend as SRC
import bend-collections-laws-math@1.0.0.0/proofs/math/random/chacha8/block.bend as PB

57# the invariant: from state C{k, p, buf} the generator outputs buf, the rest
58# of the iteration keyed by k, then C2SP's stream from the next key
59def inv(+n: Nat, +k: B.Key, +buf: List<&2, W.U64>, +p: C8.Phase) -> {SRC.outputs(~C8.ChaCha8, ~C8.next, n, C8.C{k, p, buf}) == S.stream_go(n, app(buf, rest(S.key_list(k), p)), nk(S.key_list(k), p)) : List<&2, W.U64>}:
60  match n:
61    case 0n:
62      {==}
63    case 1n+m:
64      match buf:
65        case Con{x, t}:
66          Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{x, l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, p, t}), S.stream_go(m, app(t, rest(S.key_list(k), p)), nk(S.key_list(k), p)), inv(m, k, t, p))
67        case Nil{}:
68          match p:
69            case C8.G0{}:
70              %Equal.sym(List<&2, W.U64>, B.group(k, 0), gw(k, 0), PB.group_correct(k, 0)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G1{}, _})))} == S.stream_go(1n+m, [], S.key_list(k)) : List<&2, W.U64>}
71              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 0)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G1{}, S.tail(gw(k, 0))}), S.stream_go(m, app(S.tail(gw(k, 0)), rest(S.key_list(k), C8.G1{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 0)), C8.G1{}))
72            case C8.G1{}:
73              %Equal.sym(List<&2, W.U64>, B.group(k, 4), gw(k, 4), PB.group_correct(k, 4)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G2{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G1{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
74              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 4)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G2{}, S.tail(gw(k, 4))}), S.stream_go(m, app(S.tail(gw(k, 4)), rest(S.key_list(k), C8.G2{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 4)), C8.G2{}))
75            case C8.G2{}:
76              %Equal.sym(List<&2, W.U64>, B.group(k, 8), gw(k, 8), PB.group_correct(k, 8)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.C{k, C8.G3{}, _})))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G2{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
77              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 8)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{k, C8.G3{}, S.tail(gw(k, 8))}), S.stream_go(m, app(S.tail(gw(k, 8)), rest(S.key_list(k), C8.G3{})), S.next_key(S.key_list(k))), inv(m, k, S.tail(gw(k, 8)), C8.G3{}))
78            case C8.G3{}:
79              %Equal.sym(List<&2, W.U64>, B.group(k, 12), gw(k, 12), PB.group_correct(k, 12)) : {Con{SRC.fst64(C8.ChaCha8, C8.pop(C8.last(_))), SRC.outputs(~C8.ChaCha8, ~C8.next, m, SRC.snd64(C8.ChaCha8, C8.pop(C8.last(_))))} == S.stream_go(1n+m, rest(S.key_list(k), C8.G3{}), S.next_key(S.key_list(k))) : List<&2, W.U64>}
80              Equal.cong(List<&2, W.U64>, List<&2, W.U64>, l => Con{S.head(gw(k, 12)), l}, SRC.outputs(~C8.ChaCha8, ~C8.next, m, C8.C{C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), C8.G0{}, S.tail(List.take(&2, W.U64, gw(k, 12), 28n))}), S.stream_go(m, app(S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), []), S.key_list(C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)))), inv(m, C8.rekey(List.drop(&2, W.U64, gw(k, 12), 28n)), S.tail(List.take(&2, W.U64, gw(k, 12), 28n)), C8.G0{}))