def stream_parameters

qasim-bend-kit@0.1.0.2 · proof/AES_NistObservationProof.bend:18

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCMCore.bend as Core

18def stream_parameters(+size: Nat, +words: List<&2, U32>, +start: List<&2, U32>,
19    +known_size: Nat, +known_start: List<&2, U32>, +stream: List<&2, U32>,
20    count: {size == known_size : Nat}, counter: {start == known_start : List<&2, U32>},
21    computed: {Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}) == stream : List<&2, U32>}) ->
22    {Core.gcm_ctr_stream_exact(size, words, start) == stream : List<&2, U32>}:
23    Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact(size, words, start),
24        Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}), stream,
25        Equal.cong(Nat, List<&2, U32>, n => Core.gcm_ctr_stream_exact.go(n, words, start, Nil{}), size, known_size, count),
26        Equal.trans(List<&2, U32>, Core.gcm_ctr_stream_exact.go(known_size, words, start, Nil{}),
27            Core.gcm_ctr_stream_exact.go(known_size, words, known_start, Nil{}), stream,
28            Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.gcm_ctr_stream_exact.go(known_size, words, value, Nil{}),
29                start, known_start, counter), computed))