def ccm.len_ok.three

bend-osdev-cipher-modes@0.1.0.0 · ccm.bend:87

import Base

87# the message must be shorter than 2^(8L) bytes: a bound only for L = 2 or 3
88# (with L >= 4 every list is shorter)
89def ccm.len_ok.three(three: Bool, +n: Nat) -> Bool:
90  match three:
91    case True{}:
92      U32.is_lt(U32.from_nat(n), 16777216)
93    case False{}:
94      True{}