def aes_fixed_bytes_length

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:542

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES

542def aes_fixed_bytes_length(+n: Nat, +bytes: List<&2, U32>) ->
543    {List.length(&2, U32, AES.fixed_bytes(n, bytes)) == n : Nat}:
544    match n bytes:
545        case 0n _: {==}
546        case 1n+p Nil{}:
547            Equal.cong(Nat, Nat, x => 1n+x,
548                List.length(&2, U32, AES.fixed_bytes(p, Nil{})), p,
549                aes_fixed_bytes_length(p, Nil{}))
550        case 1n+p byte <> tail:
551            Equal.cong(Nat, Nat, x => 1n+x,
552                List.length(&2, U32, AES.fixed_bytes(p, tail)), p,
553                aes_fixed_bytes_length(p, tail))