def byte_merge_hi.k

lawful-words@0.1.0.0 · proof_bytes.bend:799

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

799def byte_merge_hi.k(+lo: U32, +hi: U32, +r: Nat, +j: Nat, +hr: {Nat.is_le(r, 4n) == True{} : Bool}, +hj: {Nat.is_lt(j, 4n) == True{} : Bool},
800  +h: {Nat.is_le(4n, Nat.add(j, r)) == True{} : Bool}, +k: Nat) ->
801  {D.bit(D.byte(D.merge(lo, hi, r), j), k) == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}:
802  +l = Nat.is_lt(k, 8n)
803  +i = Nat.add(Nat.mul(8n, j), k)
804  +r8 = Nat.mul(8n, r)
805  +u = Nat.sub(4n, r)
806  +u8 = Nat.mul(8n, u)
807  +hu = le_sub_l(4n, r, j, h)
808  +x = D.bit(hi, Nat.add(Nat.mul(8n, Nat.sub(Nat.add(j, r), 4n)), k))
809  %Equal.sym(Bool, D.bit(D.byte(D.merge(lo, hi, r), j), k),
810      Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))), bit_merge(lo, hi, r, j, k)) :
811    {_ == D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k) : Bool}
812  %Equal.sym(Bool, D.bit(D.byte(hi, Nat.sub(Nat.add(j, r), 4n)), k), Bool.and(l, x), bit_byte(hi, Nat.sub(Nat.add(j, r), 4n), k)) :
813    {Bool.and(l, Bool.or(D.bit(lo, Nat.add(i, r8)), Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == _ : Bool}
814  %Equal.sym(Bool, D.bit(lo, Nat.add(i, r8)), False{}, bit_ge32(lo, Nat.add(i, r8),
815      %Equal.sym(Nat, Nat.add(i, r8), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), idx_add(j, r, k)) : {Nat.is_le(32n, _) == True{} : Bool}
816      N.le_trans(32n, Nat.mul(8n, Nat.add(j, r)), Nat.add(Nat.mul(8n, Nat.add(j, r)), k), N.le_mul_l(8n, 4n, Nat.add(j, r), h), N.le_add_r(Nat.mul(8n, Nat.add(j, r)), k)))) :
817    {Bool.and(l, Bool.or(_, Bool.and(Nat.is_le(u8, i), Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
818  %Equal.sym(Bool, Nat.is_le(u8, i), True{}, N.le_trans(u8, Nat.mul(8n, j), i, N.le_mul_l(8n, u, j, hu), N.le_add_r(Nat.mul(8n, j), k))) :
819    {Bool.and(l, Bool.or(False{}, Bool.and(_, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.sub(i, u8)))))) == Bool.and(l, x) : Bool}
820  %Equal.sym(Nat, Nat.sub(i, u8), Nat.add(Nat.mul(8n, Nat.sub(j, u)), k), idx_sub(u, j, k, hu)) :
821    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, _))))) == Bool.and(l, x) : Bool}
822  %Equal.sym(Nat, Nat.sub(j, u), Nat.sub(Nat.add(j, r), 4n), sub_sub_eq(j, r, 4n, hr)) :
823    {Bool.and(l, Bool.or(False{}, Bool.and(True{}, Bool.and(Nat.is_lt(i, 32n), D.bit(hi, Nat.add(Nat.mul(8n, _), k)))))) == Bool.and(l, x) : Bool}
824  bimp(l, Nat.is_lt(i, 32n), x, hk => idx32(j, k, hj, hk))