Check.main: def of bend-osdev-bpf@0.1.0.0
Import: import bend-osdev-bpf@0.1.0.0/check.bend as Check
Lines 159-179 of bend-osdev-bpf@0.1.0.0/check.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&start_line=159&end_line=179

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

def main() -> IO(Unit):
  +big = I.bpf_to_octets(I.BpfBig{}, big.prog(512n, 511, 511, Nil{}))
  +huge = I.bpf_to_octets(I.BpfLittle{}, big.prog(4096n, 4095, 4095, Nil{}))
  do IO<Unit>:
    IO.print("rarp " ++ show_run(run_raw(pkt_rarp(), rarp())) ++ " " ++ show_run(run_raw(pkt_arp(), rarp())))
    IO.print("hosts " ++ pkt_run(pkt_ip([128, 3, 112, 15], [128, 3, 112, 35]), hosts()) ++ " " ++ pkt_run(pkt_ip([128, 3, 112, 35], [128, 3, 112, 15]), hosts()) ++ " " ++ pkt_run(pkt_ip([128, 3, 112, 15], [10, 0, 0, 1]), hosts()) ++ " " ++ pkt_run(pkt_arp(), hosts()))
    IO.print("finger " ++ pkt_run(pkt_finger(), finger()) ++ " " ++ pkt_run(pkt_web(), finger()) ++ " " ++ pkt_run(pkt_frag(), finger()) ++ " " ++ pkt_run(pkt_finger_opts(), finger()))
    IO.print("short " ++ pkt_run(B.Octets.of_list([1, 2, 3]), finger()))
    IO.print("len " ++ pkt_run(pkt_rarp(), [I.BpfLdLen{}, I.BpfRet{I.BpfRetA{}}]))
    IO.print("div0 " ++ pkt_run(pkt_rarp(), [I.BpfLdImm{7}, I.BpfAlu{I.BpfDiv{}, I.BpfX{}}, I.BpfRet{I.BpfRetK{1}}]))
    IO.print("mem " ++ pkt_run(pkt_rarp(), [I.BpfLdImm{5}, I.BpfSt{15}, I.BpfLdxImm{3}, I.BpfLdMem{15}, I.BpfAlu{I.BpfMul{}, I.BpfX{}}, I.BpfStx{0}, I.BpfLdxMem{15}, I.BpfAlu{I.BpfSub{}, I.BpfX{}}, I.BpfNeg{}, I.BpfRet{I.BpfRetA{}}]))
    IO.print("bytes " ++ B.Octets.hex(I.bpf_to_octets(I.BpfLittle{}, rarp())))
    IO.print("validate " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), finger())) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [])) ++ ", " ++ show_ok(V.bpf_validate(1n, finger())) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfJa{1}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdImm{1}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfSt{16}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfAlu{I.BpfMod{}, I.BpfK{0}}, I.BpfRet{I.BpfRetA{}}])))
    IO.print("mem init " ++ show_ok(V.bpf_validate(V.bpf_maxinsns(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}])) ++ ", " ++ show_ok(V.bpf_validate_with(V.BpfValidateOptions.permissive(), [I.BpfLdMem{3}, I.BpfRet{I.BpfRetA{}}])))
    IO.print("decode " ++ show_run(run_raw(pkt_rarp(), [I.bpf_stmt(14, 0)])))
    IO.print("seccomp " ++ sc(example(), sc_call(59, S.seccomp_arch_x86_64())) ++ " " ++ sc(example(), sc_call(1, S.seccomp_arch_x86_64())) ++ " " ++ sc(example(), sc_call(59, S.seccomp_arch_i386())) ++ " " ++ sc(example(), sc_call(1073741883, S.seccomp_arch_x86_64())))
    IO.print("seccomp validate " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), example())) ++ ", " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), finger())) ++ ", " ++ show_ok(S.seccomp_validate(V.bpf_maxinsns(), [I.BpfLdAbs{I.BpfW{}, 6}, I.BpfRet{I.BpfRetA{}}])))
    IO.print("stack " ++ show_act(S.seccomp_eval([deny(39, 1), deny(39, 2), deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([deny(39, 1), ret_only(S.SeccompTrap{5}), deny(110, 3)], S.seccomp_order(), sc_call(39, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([deny(39, 1), deny(110, 3)], S.seccomp_order(), sc_call(110, S.seccomp_arch_x86_64()))) ++ " " ++ show_act(S.seccomp_eval([], S.seccomp_order(), sc_call(110, S.seccomp_arch_x86_64()))))
    IO.print("action " ++ S.SeccompAction.show(S.SeccompAction.of_u32(196613)) ++ " " ++ S.SeccompAction.show(S.SeccompAction.of_u32(65536)) ++ " " ++ S.SeccompAction.show(S.SeccompAction.of_u32(0)) ++ " " ++ U32.show(S.SeccompAction.to_u32(S.SeccompErrno{65549})))
    IO.print("big " ++ Nat.show(B.Octets.len(big)) ++ " bytes, answer " ++ big.read(I.bpf_of_octets(I.BpfBig{}, big), B.Octets.of_list(big.packet(65536n, 7, Nil{}))))
    IO.print("huge " ++ Nat.show(B.Octets.len(huge)) ++ " bytes: " ++ huge.read(I.bpf_of_octets(I.BpfLittle{}, huge)) ++ "; with a limit of 1 MB: " ++ huge.read(I.bpf_of_octets_with(1048576n, I.BpfLittle{}, huge)))

Uses (58):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.bind
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=IO.print
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.show
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.show
  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/check.bend&name=big.packet
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=big.prog
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=big.read
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=deny
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=example
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=finger
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=hosts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=huge.read
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_arp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_finger
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_finger_opts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_frag
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_ip
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_rarp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=pkt_web
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=rarp
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=ret_only
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=run_raw
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=sc_call
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=show_act
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=show_ok
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/check.bend&name=show_run
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfAluOp
  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/insn.bend&name=BpfRval
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfSize
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=BpfSrc
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_of_octets
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_of_octets_with
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_stmt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/insn.bend&name=bpf_to_octets
  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=SeccompAction.of_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction.show
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=SeccompAction.to_u32
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_arch_i386
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_arch_x86_64
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_eval
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_order
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/seccomp.bend&name=seccomp_validate
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=BpfValidateOptions.permissive
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_maxinsns
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_validate
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bpf@0.1.0.0/validate.bend&name=bpf_validate_with
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.hex
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.len
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-bytes@0.1.1.1/bytes.bend&name=Octets.of_list