LAWS.install_path_limit: law of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/LAWS.bend as LAWS
Lines 300-301 of bend-osdev-bpf@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&start_line=300&end_line=301

import Base
import bend-osdev-bpf@0.1.0.0/insn.bend as I
import bend-osdev-bpf@0.1.0.0/seccomp.bend as S

law install_path_limit:
  {S.seccomp_install(S.SeccompLimits{4096n, 19n}, [deny(39, 1), deny(39, 2)], I.bpf_encode(deny(110, 3))) == Fail{I.BpfErrPathTooLong{20n}} : Result<&2, &2, I.BpfError, List<&2, List<&2, I.BpfOp>>>}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=deny
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfError
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfOp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_encode
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompLimits
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_install