law aes256gcm_accepts_32_byte_key

qasim-bend-kit@0.1.0.2 · LAWS.bend:281

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

281law aes256gcm_accepts_32_byte_key:
282    for +bytes: List<&2, U32>
283    for size: {List.length(&2, U32, bytes) == 32n : Nat}
284    for valid: {AES.bytes_valid(bytes) == True{} : Bool}
285    {AES.key(bytes) == Done{AES.SecretKey{bytes, size, valid}} :
286        Result<&2, &2, AES.Error, AES.SecretKey>}

Uses (15)

Used by (0)

No other definition uses this definition.