def parts

stelliferous@0.0.2.0 · proofs/u32_shift.bend:28

import Base
import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32Successor
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

28def parts(+c: Bool,+parts: WordEncoding.Split<31n,1n>) -> Goal(WordEncoding.join(31n,1n,parts),c):
29  WordEncoding.Parts{+low,+high} = parts
30  bound =>
31    %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {Word.shl.out(32n,c,WordEncoding.concat(31n,1n,low,
32          _)) == (False{},Word.shl.put(32n,c,WordEncoding.concat(31n,1n,low,_))) : Bool & Word(32n)}
33    %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),U32Successor.concat_pad(31n,
34        low)) : {Word.shl.out(32n,c,_) == (False{},Word.shl.put(32n,c,_)) : Bool & Word(32n)}
35    out_pad(31n,c,low)