def encoded_put
stelliferous@0.0.2.0 · proofs/u32_shift.bend:54
import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
54def encoded_put(+c: Bool,+w: Word(32n)) -> {U32{Word.shl.put(32n,c,w)} == U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))) : U32}:
55 match c:
56 case False{}:
57 %WordArithmetic.shift_put(32n,w) : {U32{_} == U32.from_nat(Nat.double(Word.to_nat(32n,w))) : U32}
58 encoded_shift(w)
59 case True{}:
60 %Equal.sym(Word(32n),Word.shl.put(32n,True{},w),Word.inc(32n,Word.shl(32n,w)),put_inc(32n,
61 w)) : {U32{_} == U32.inc(U32.from_nat(Nat.double(Word.to_nat(32n,w)))) : U32}
62 %encoded_shift(w) : {U32.inc(U32{Word.shl(32n,w)}) == U32.inc(_) : U32}
63 {==}