def u32_add_sub

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

import Base

1404def u32_add_sub(a: U32, b: U32) -> {a == U32.sub(U32.add(a, b), b) : U32}:
1405  match a b:
1406    case U32{x} U32{y}:
1407      %adc_add_sub(32n, x, y, False{}) : {U32{x} == U32{_} : U32}
1408      {==}