def pack4_bytes.go

lawful-words@0.1.0.0 · proof_bytes.bend:1309

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

1309def pack4_bytes.go(+w: U32, +j: Nat, +k: Nat, +hk: {Nat.is_lt(k, 8n) == True{} : Bool}, z: Bool, +ez: {Nat.is_lt(j, 4n) == z : Bool}) ->
1310  {D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), Nat.add(Nat.mul(8n, j), k)) == D.bit(w, Nat.add(Nat.mul(8n, j), k)) : Bool}:
1311  match z:
1312    case True{}:
1313      +p = Nat.add(Nat.mul(8n, j), k)
1314      %Equal.sym(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p),
1315          D.bit(D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), k),
1316          pack_byte(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n), j, k,
1317            lt256(D.byte(w, 0n), byte_lt(w, 0n)), lt256(D.byte(w, 1n), byte_lt(w, 1n)), lt256(D.byte(w, 2n), byte_lt(w, 2n)), lt256(D.byte(w, 3n), byte_lt(w, 3n)), ez, hk)) :
1318        {_ == D.bit(w, p) : Bool}
1319      %Equal.sym(U32, D.nth4(j, D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), D.byte(w, j), nth4_byte(w, j, ez)) : {D.bit(_, k) == D.bit(w, p) : Bool}
1320      %Equal.sym(Bool, D.bit(D.byte(w, j), k), Bool.and(Nat.is_lt(k, 8n), D.bit(w, p)), bit_byte(w, j, k)) : {_ == D.bit(w, p) : Bool}
1321      %Equal.sym(Bool, Nat.is_lt(k, 8n), True{}, hk) : {Bool.and(_, D.bit(w, p)) == D.bit(w, p) : Bool}
1322      {==}
1323    case False{}:
1324      +p = Nat.add(Nat.mul(8n, j), k)
1325      +h32 = N.le_trans(32n, Nat.mul(8n, j), p, N.le_mul_l(8n, 4n, j, N.not_lt_le(j, 4n, ez)), N.le_add_r(Nat.mul(8n, j), k))
1326      Equal.trans(Bool, D.bit(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p), False{}, D.bit(w, p),
1327        bit_ge32(D.pack4(D.byte(w, 0n), D.byte(w, 1n), D.byte(w, 2n), D.byte(w, 3n)), p, h32),
1328        Equal.sym(Bool, D.bit(w, p), False{}, bit_ge32(w, p, h32)))