The Bedrock2 implementation is inspired by bn_sub_with_borrow in BoringSSL but has been rewritten to simplify verification using the tactic ZnWords. Specifically:
It accumulates borrow bits using sum, not bitwise or;
It checks for each borrow bit using word.ltu. This enables verification by proving an applying a simple lemma specifying subtraction with borrow over two operands.
The proof's organization roughly follows that of add_with_carry.
The Bedrock2 implementation is inspired by
bn_sub_with_borrowin BoringSSL but has been rewritten to simplify verification using the tacticZnWords. Specifically:word.ltu. This enables verification by proving an applying a simple lemma specifying subtraction with borrow over two operands.The proof's organization roughly follows that of
add_with_carry.