law aes256gcm_encrypts_valid_input

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

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

323# This prevents satisfying the conditional roundtrip by always failing.
324law aes256gcm_encrypts_valid_input:
325    for key: AES.SecretKey
326    for nonce: AES.Nonce
327    for aad: List<&2, U32>
328    for plaintext: List<&2, U32>
329    for aad_ok: {AES.aad_valid(aad) == True{} : Bool}
330    for plaintext_ok: {AES.plaintext_valid(plaintext) == True{} : Bool}
331    {Result.is_done(&2, &2, AES.Error, AES.Envelope,
332        AES.encrypt(key, nonce, aad, plaintext)) == True{} : Bool}

Uses (12)

Used by (0)

No other definition uses this definition.