def wp.sub_split.fin

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

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

138def wp.sub_split.fin(-ahw: Word(32n), -alw: Word(32n), -bhw: Word(32n), -blw: Word(32n), cb: Bool) -> {W.W64{U32.sub(U32{Word.sub(32n, ahw, bhw)}, W.W64.bit(cb)), U32{Word.sub(32n, alw, blw)}} == W.W64{U32{Word.sub(32n, Word.sub(32n, ahw, bhw), P.wv.bitw(32n, cb))}, U32{Word.sub(32n, alw, blw)}} : W.W64}:
139  match cb:
140    case True{}:
141      {==}
142    case False{}:
143      {==}