def pack4_bytes.k

lawful-words@0.1.0.0 · proof_bytes.bend:1330

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

1330def pack4_bytes.k(+w: U32, +k: Nat) -> {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k) == D.bit(w, k) : Bool}:
1331  +j = Nat.div(k, 8n)
1332  +r = Nat.mod(k, 8n)
1333  %Equal.trans(Nat, Nat.add(Nat.mul(8n, j), r), Nat.add(Nat.mul(j, 8n), r), k,
1334      Equal.cong(Nat, Nat, t => Nat.add(t, r), Nat.mul(8n, j), Nat.mul(j, 8n), N.mul_comm(8n, j)), N.div_mod(k, 8n)) :
1335    {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), _) == D.bit(w, _) : Bool}
1336  pack4_bytes.go(w, j, r, N.mod_lt(k, 8n, {==}), Nat.is_lt(j, 4n), {==})