law shv

lawful-words@0.1.0.0 · proof_bytes.bend:1476

import Base

1476# The value of b << 8s, 16 or 24, with a = 2^8 and m = 2^32 abstract.
1477law shv:
1478  for +b: U32
1479  for +s: Nat
1480  for +p: Nat
1481  for +a: Nat
1482  for +m: Nat
1483  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1484  for +hp: {Nat.pow(2n, s) == p : Nat}
1485  for +hb: {Nat.is_lt(U32.to_nat(b), a) == True{} : Bool}
1486  for +hpm: {Nat.is_le(Nat.mul(a, p), m) == True{} : Bool}
1487  for +hp0: {Nat.is_lt(0n, p) == True{} : Bool}
1488  {U32.to_nat(U32.shln(b, s)) == Nat.mul(U32.to_nat(b), p) : Nat}