def xor_from_stream

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

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

35def xor_from_stream(+words: List<&2, U32>, +nonce: List<&2, U32>, +input: List<&2, U32>, +stream: List<&2, U32>,
36    computed: {Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))) == stream : List<&2, U32>}) ->
37    {Core.gcm_decrypt_expanded(words, nonce, input) == Core.gcm_zip_xor(input, stream) : List<&2, U32>}:
38    Equal.cong(List<&2, U32>, List<&2, U32>, value => Core.gcm_zip_xor(input, value),
39        Core.gcm_ctr_stream_exact(List.length(&2, U32, input), words, Core.gcm_inc32(Core.gcm_j0(nonce))), stream, computed)