def byte_pack4.l

lawful-words@0.1.0.0 · proof_bytes.bend:1240

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

1240def byte_pack4.l(+b0: U32, +b1: U32, +b2: U32, +b3: U32, +j: Nat, +k: Nat,
1241  +h0: {Nat.is_lt(U32.to_nat(b0), Nat.pow(2n, 8n)) == True{} : Bool},
1242  +h1: {Nat.is_lt(U32.to_nat(b1), Nat.pow(2n, 8n)) == True{} : Bool},
1243  +h2: {Nat.is_lt(U32.to_nat(b2), Nat.pow(2n, 8n)) == True{} : Bool},
1244  +h3: {Nat.is_lt(U32.to_nat(b3), Nat.pow(2n, 8n)) == True{} : Bool},
1245  +hj: {Nat.is_lt(j, 4n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(k, 8n) == z : Bool}) ->
1246  {Bool.and(z, D.bit(D.pack4(b0, b1, b2, b3), Nat.add(Nat.mul(8n, j), k))) == D.bit(D.nth4(j, b0, b1, b2, b3), k) : Bool}:
1247  match z:
1248    case True{}:
1249      pack_byte(b0, b1, b2, b3, j, k, h0, h1, h2, h3, hj, ez)
1250    case False{}:
1251      Equal.sym(Bool, D.bit(D.nth4(j, b0, b1, b2, b3), k), False{},
1252        bit_lt_pow(D.nth4(j, b0, b1, b2, b3), 8n, k, nth4_lt(j, b0, b1, b2, b3, h0, h1, h2, h3), N.not_lt_le(k, 8n, ez)))