pub fn add3(a: [Field; 32], b: [Field; 32], c: [Field; 32]) -> [Field; 32]Expand description
(a + b + c) mod 2^32 — a three-input modular add done as a SINGLE 34-bit
range-check instead of two chained add32s.
The three words sum to < 3·2^32 < 2^34, so decomposing the field sum into
34 bits (32 result + 2 carry) and returning the low 32 pins (a+b+c) mod 2^32 in one gadget. Cost: 34 booleanity gates + 1 recomposition, vs the
chain’s 2×(33+1) = 68. Soundness: formal/Formal/Blake.lean
add3Mod32_bit_sound (with add3Mod32_eq_nested bridging it to the
addMod32 (addMod32 a b) c the BLAKE G spec uses).