[circomlib] Prove `BinSub` soundness and completeness

[pirapira]

Formalize the BinSub (binary subtraction) circuit from circomlib.

The BinSub circuit performs binary subtraction with borrow bit handling.

Implementation details

• Located in circomlib/circuits/binsub.circom
• Implements n-bit binary subtraction: (in[0] + 2^n) - in[1] = out + aux*2^n
• Takes two n-bit binary inputs and produces n-bit output plus auxiliary borrow bit
• Similar complexity to BinSum which is already being formalized

References

• Parent epic: Formalize all of circomlib #155 (Formalize all of circomlib)
• Related: Formalize BinSum gadget #198 (Formalize BinSum gadget)
• Original circomlib source