def u32_sub_add

bend-osdev-legacy-ciphers@0.1.0.0 · PROOF.bend:1410

import Base

1410def u32_sub_add(a: U32, b: U32) -> {a == U32.add(U32.sub(a, b), b) : U32}:
1411  match a b:
1412    case U32{x} U32{y}:
1413      %adc_sub_add(32n, x, y, True{}) : {U32{x} == U32{_} : U32}
1414      {==}