def F_encode

bend-osdev-bpf@0.1.0.0 · PROOF.bend:525

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

525def F_encode(+ops: List<&2, I.BpfOp>) -> {I.bpf_encode.ref(ops) == I.bpf_encode(ops) : List<&2, I.BpfRaw>}:
526  Equal.sym(List<&2, I.BpfRaw>, I.bpf_encode(ops), I.bpf_encode.ref(ops),
527    Equal.trans(List<&2, I.BpfRaw>, I.bpf_encode(ops), List.reverse.go(&2, I.BpfRaw, List.reverse.go(&2, I.BpfRaw, I.bpf_encode.ref(ops), Nil{}), Nil{}), I.bpf_encode.ref(ops),
528      Equal.cong(List<&2, I.BpfRaw>, List<&2, I.BpfRaw>, l => List.reverse.go(&2, I.BpfRaw, l, Nil{}), I.bpf_encode.go(ops, Nil{}), List.reverse.go(&2, I.BpfRaw, I.bpf_encode.ref(ops), Nil{}), g_encode(ops, Nil{})),
529      rev_twice(I.BpfRaw, I.bpf_encode.ref(ops))))