law octets_max_default

bend-osdev-bpf@0.1.0.0 · LAWS.bend:241

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/validate.bend as V

241# the default limit on stored programs: 8 bytes for each of BPF_MAXINSNS
242# instructions (compared as U32, which holds both)
243law octets_max_default:
244  {U32.from_nat(I.bpf_octets_max()) == U32.mul(8, U32.from_nat(V.bpf_maxinsns())) : U32}