law pack_bits

lawful-words@0.1.0.0 · proof_bytes.bend:1099

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

1099# Bit k (k < 8) of byte j of pack4(b0, b1, b2, b3).
1100law pack_bits:
1101  for +b0: U32
1102  for +b1: U32
1103  for +b2: U32
1104  for +b3: U32
1105  for +j: Nat
1106  for +k: Nat
1107  for +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool}
1108  for +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool}
1109  for +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool}
1110  for +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool}
1111  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
1112  {D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k)) ==
1113    Bool.or(Bool.and(Nat.is_eq(j, 0n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b0, k))),
1114    Bool.or(Bool.and(Nat.is_eq(j, 1n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b1, k))),
1115    Bool.or(Bool.and(Nat.is_eq(j, 2n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b2, k))),
1116            Bool.and(Nat.is_eq(j, 3n), Bool.and(Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n), D.bit(b3, k)))))) : Bool}