def gcm_mask_bytes_length

qasim-bend-kit@0.1.0.2 · libs/AES256GCMCore.bend:282

import Base

282def gcm_mask_bytes_length(+bytes: List<&2, U32>) ->
283    {List.length(&2, U32, gcm_mask_bytes(bytes)) ==
284     List.length(&2, U32, bytes) : Nat}:
285    match bytes:
286        case Nil{}: {==}
287        case byte <> tail:
288            Equal.cong(Nat, Nat, n => 1n+n,
289                List.length(&2, U32, gcm_mask_bytes(tail)),
290                List.length(&2, U32, tail),
291                gcm_mask_bytes_length(tail))