def bounded_put
stelliferous@0.0.2.0 · proofs/u32_shift.bend:65
import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
65def bounded_put(+c: Bool,+w: Word(32n),+cap: U32,cap_ok: {U32.is_le(cap,2147483648) == True{} : Bool},h: {Nat.is_le(Comparison.digit(c,
66 Word.to_nat(32n,w)),U32.to_nat(cap)) == True{} : Bool}) -> {U32.to_nat(U32{Word.shl.put(32n,c,w)}) == Comparison.digit(c,
67 Word.to_nat(32n,w)) : Nat}:
68 %Equal.sym(U32,U32{Word.shl.put(32n,c,w)},U32.from_nat(Comparison.digit(c,Word.to_nat(32n,w))),encoded_put(c,
69 w)) : {U32.to_nat(_) == Comparison.digit(c,Word.to_nat(32n,w)) : Nat}
70 Bounds.roundtrip(Comparison.digit(c,Word.to_nat(32n,w)),cap,cap_ok,h)