def WB_unsigned

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:103

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

103def WB_unsigned(+n: Nat, +w: Word(n)) -> {Nat.is_lt(S.unsigned(n, w), S.scale_binary(n, 1n)) == True{} : Bool}:
104  match n:
105    case 0n:
106      {==}
107    case 1n+p:
108      match w:
109        case WCon{b, t}:
110          N.double_lt_bit(b, S.unsigned(p, t), S.scale_binary(p, 1n), WB_unsigned(p, t))