def byte_merge_lo.k

lawful-words@0.1.0.0 · proof_bytes.bend:771

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

771def byte_merge_lo.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +h: {Nat.is_lt(Nat.add(j, r), 4n) == True{} : Bool}, +k: Nat) ->
772  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}:
773  +l = Nat.is_lt(k, 8n)
774  +i = Nat.add(Nat.mul(8n, j), k)
775  +r8 = Nat.mul(8n, r)
776  +u8 = Nat.mul(8n, Nat.sub(4n, r))
777  +y = Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))
778  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k), Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))), bit_merge(lo, hi, r, j, k)) :
779    {_ == D.bit(D.byte(lo, Nat.add(j, r)), k) : Bool}
780  %Equal.sym(Bool, D.bit(D.byte(lo, Nat.add(j, r)), k), Bool.and(l, D.bit(lo, Nat.add(Nat.mul(8n, Nat.add(j, r)), k))), bit_byte(lo, Nat.add(j, r), k)) :
781    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == _ : Bool}
782  %idx_add(j, r, k) : {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), y))) == Bool.and(l, D.bit(lo, _)) : Bool}
783  bor_low(l, D.bit(lo, Nat.add(i, r8)), Nat.is_le(u8, i), y,
784    hk => lt_not_le(i, u8, N.lt_le_trans(i, Nat.mul(8n, 1n+j), u8, lt_mul8(j, k, hk),
785      N.le_mul_l(8n, 1n+j, Nat.sub(4n, r), %Equal.sym(Bool, Nat.is_le(1n+j, Nat.sub(4n, r)), Nat.is_lt(j, Nat.sub(4n, r)), N.le_succ_lt(j, Nat.sub(4n, r))) : {_ == True{} : Bool};
786        lt_sub(j, r, 4n, h)))))