def F_count

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

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

214def F_count(+xs: List<&2, I.BpfOp>) -> {List.length(&2, I.BpfOp, xs) == V.bpf_count(xs) : Nat}:
215  Equal.sym(Nat, V.bpf_count(xs), List.length(&2, I.BpfOp, xs),
216    Equal.trans(Nat, V.bpf_count.go(xs, 0n), Nat.add(List.length(&2, I.BpfOp, xs), 0n), List.length(&2, I.BpfOp, xs),
217      g_count(xs, 0n), add_zero(List.length(&2, I.BpfOp, xs))))