law octets_over_limit

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

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

77# a stored program with a byte at offset max (so more than max bytes) is
78# refused, whatever its bytes
79law octets_over_limit:
80  for +max: Nat
81  for +order: I.BpfOrder
82  for +o: B.Octets
83  for b: U32
84  for e: {B.Octets.at(o, max) == Some{b} : Maybe<&2, U32>}
85  {I.bpf_of_octets_with(max, order, o) == Fail{I.BpfErrStoredTooLong{max}} : Result<&2, &2, I.BpfError, List<&2, I.BpfRaw>>}