Fix description of tnum.mask, and use C-style comment

model-checking-bpf-verifier-presentation.ipynb

When I look at tnum_const function, the tnum.mask comment should read "which bits are unknown".

It'd be interesting to implement Tnum.popcount() (of the mask) and try proving sum.popcount() <= t1.popcount() + t2.popcount() + margin to see how tnum_add is efficient in conserving certainity.

(I hope that z3 prover doesn't use same tnums implementation internally ;-).)

When I look at tnum_const function, the tnum.mask comment should read "which bits are unknown".

@Werkov thanks for spotting the mistake! Now fixed.

It'd be interesting to implement Tnum.popcount() (of the mask) and try proving sum.popcount() <= t1.popcount() + t2.popcount() + margin to see how tnum_add is efficient in conserving certainity.

Very interesting indeed, though I wonder if I should eliminate cases where it overflows, otherwise a Tnum(val=-1, mask=0) + Tnum(val=0, mask=1) == Tnum(val=0, mask=-1) worst-case might kill all the fun.

Another ideal would be to brute-force through all the combinations at a lower size (i.e. bandwidth), maybe 16-bit instead of 64-bit, then plot some thing like a closure plot (using the posits paper as an example here)

In Sound, Precise, and Fast Abstract Interpretation with Tristate Numbers, they used brute-forcing to compare the precision between their proposed multiplication algorithm and the original tnum_mul() in the Linux kernel.

(I hope that z3 prover doesn't use same tnums implementation internally ;-).)

I hope not :P

Another ideal would be to brute-force through all the combinations at a lower size (i.e. bandwidth), maybe 16-bit instead of 64-bit, then plot some thing like a closure plot (using the posits paper as an example here)

Scratch that... I cannot represent tnum on a single number line