def nonce_ok

bend-osdev-aead@0.1.0.0 · PROOF.bend:339

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B

339def nonce_ok(+n: B.Octets, hn: {B.Octets.len(n) == 16n : Nat}) -> {Nat.is_eq(B.Octets.len(n), 16n) == True{} : Bool}:
340  %Equal.sym(Nat, B.Octets.len(n), 16n, hn) : {Nat.is_eq(_, 16n) == True{} : Bool}
341  {==}