LAWS.seccomp_validated_acts: law of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/LAWS.bend as LAWS
Lines 114-120 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=114&end_line=120

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
import bend-osdev-bpf@0.1.0.0/seccomp.bend as S

law seccomp_validated_acts:
  for +opts: V.BpfValidateOptions
  for +order: I.BpfOrder
  for +prog: List<&2, I.BpfOp>
  for +d: S.SeccompData
  for +ok: {S.seccomp_validate_with(opts, prog) == Done{Unit{}} : Result<&2, &2, I.BpfError, Unit>}
  {Result.is_done(&2, &2, I.BpfError, S.SeccompAction, S.seccomp_run(order, prog, d)) == True{} : Bool}

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Base/base.bend&name=Result.is_done
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/LAWS.bend&name=validated_returns
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=fin_done
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/PROOF.bend&name=sc_l
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/bpf.bend&name=bpf_run
  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=BpfOrder
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompData
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompData.input
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_validate_with
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=BpfValidateOptions
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_validate_with