The logic widget's identity folds five residuals. Three pin the quad differences to {0,1,2,3}; of the remaining two, only w − a·b binds the per-quad product wire, while the XOR/AND check consumes it as a cubic in the same wire.
No test forges that wire. logic_xor_binds_output_to_inputs forges the quad accumulators, which is an independent axis, so the binding term itself has never been exercised.
Forging the wire normally breaks both residuals at once, which would not isolate the binding term. On the quad pairs where the cubic admits a root other than the honest product, it does isolate: the other residual stays satisfied and the binding term is the only objection. This adds a regression built on such a pair and requires the proof to fail.
Completes the helper-wire coverage #882 and #894 added for the curve-addition and fixed-base widgets.
The logic widget's identity folds five residuals. Three pin the quad differences to
{0,1,2,3}; of the remaining two, onlyw − a·bbinds the per-quad product wire, while the XOR/AND check consumes it as a cubic in the same wire.No test forges that wire.
logic_xor_binds_output_to_inputsforges the quad accumulators, which is an independent axis, so the binding term itself has never been exercised.Forging the wire normally breaks both residuals at once, which would not isolate the binding term. On the quad pairs where the cubic admits a root other than the honest product, it does isolate: the other residual stays satisfied and the binding term is the only objection. This adds a regression built on such a pair and requires the proof to fail.
Completes the helper-wire coverage #882 and #894 added for the curve-addition and fixed-base widgets.