def ccm.tag_ok

import bend-osdev-cipher-modes@0.1.0.0/ccm.bend as Ccm

import Base

84def ccm.tag_ok(+m: Nat) -> Bool:
85  Bool.and(Nat.is_le(4n, m), Bool.and(Nat.is_le(m, 16n), Nat.is_eq(Nat.mod(m, 2n), 0n)))

Uses (6)