def encrypt_block_length

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:47

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

47def encrypt_block_length(+words: List<&2, U32>, +counter: List<&2, U32>) ->
48    {List.length(&2, U32, Core.aes256_encrypt_expanded(words, counter)) ==
49     16n : Nat}:
50    match words:
51        case Nil{}: {==}
52        case head <> tail: {==}