~/jendhub

def ccmp.tag_le

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1750

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as CC

1750def ccmp.tag_le(+m: Nat, +nl: Nat, +n: Nat, +u: Unit, h: {CC.ccm.checks(m, nl, n) == Done{u} : Result<&2, &2, M.CmError, Unit>}) -> {Nat.is_le(m, 16n) == True{} : Bool}:
1751  ccmp.tag_le.go(CC.ccm.tag_ok(m), m, nl, n, u)({==})(h)

Uses (9)

Used by (1)