law bsel

lawful-words@0.1.0.0 · proof_bytes.bend:1072

import Base
import lawful-words@0.1.0.0/defs.bend as D

1072law bsel:
1073  for +b: U32
1074  for +x: Nat
1075  for +j: Nat
1076  for +k: Nat
1077  for +hb: {Nat.is_lt(U32.to_nat(b), Nat.pow(2n, 8n)) == True{} : Bool}
1078  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1079  {D.bit(U32.shln(b, Nat.mul(8n, x)), Nat.add(Nat.mul(8n, j), k))
1080    == Bool.and(Nat.is_eq(j, x), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b, k))) : Bool}