~/jendhub

def oc.le16

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

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL

1473def oc.le16(+o: B.Octets, h: {Nat.is_le(16n, B.Octets.len(o)) == True{} : Bool}) -> {Nat.is_le(16n, B.len(B.Octets.to_list(o))) == True{} : Bool}:
1474  %BL.octets_len_list(o) : {Nat.is_le(16n, _) == True{} : Bool}
1475  h

Uses (7)

Used by (1)