def wp.add_split.fin

bend-osdev-word64@0.1.1.0 · PROOF.bend:124

import Base
import bend-osdev-word64@0.1.1.0/word64.bend as W
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

124def wp.add_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.add(U32{Word.add(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.add(32n, alw, blw)}} == W.W64{U32{Word.add(32n, Word.add(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.add(32n, alw, blw)}} : W.W64}:
125  match cb:
126    case True{}:
127      {==}
128    case False{}:
129      {==}