Bytes.bytes_le_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
Lines 269-289 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&start_line=269&end_line=289

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as B
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV

def bytes_le_v(+one: Nat, +h1: {one == 1n : Nat}, k: Nat, xs: List<&2, Nat>, +h: {FS.limbs16(one, k, xs) == True{} : Bool}) -> {B.bytes_le(xs) == CV.i2osp_le(Nat.double(k), LV.ev(xs)) : List<&2, U32>}:
  match k xs:
    case 0n Nil{}:
      {==}
    case 0n x <> t:
      Empty.absurd({B.bytes_le(x <> t) == CV.i2osp_le(Nat.double(0n), LV.ev(x <> t)) : List<&2, U32>}, Lg.false_true(h))
    case 1n+j Nil{}:
      Empty.absurd({B.bytes_le([]) == CV.i2osp_le(Nat.double(1n+j), LV.ev([])) : List<&2, U32>}, Lg.false_true(h))
    case 1n+ +j +x <> +t:
      +hx = Lg.and_left(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
      +ht = Lg.and_right(Nat.is_lt(x, C.shift(16n, one)), FS.limbs16(one, j, t), h)
      +f16 = fits_one(16n, one, h1, x, hx)
      +v = Nat.add(x, C.shift(16n, LV.ev(t)))
      +e1 = low_v(x, LV.ev(t))
      +e2 = mid_v(x, LV.ev(t), f16)
      +e3 = top_v(x, LV.ev(t), f16)
      %Equal.sym(Nat, C.low(8n, Nat.add(x, C.shift(16n, LV.ev(t)))), Nat.mod(x, 256n), e1) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(_) <> U32.from_nat(C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) <> CV.i2osp_le(Nat.double(j), C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) : List<&2, U32>}
      %Equal.sym(Nat, C.low(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t))))), Nat.div(x, 256n), e2) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(_) <> CV.i2osp_le(Nat.double(j), C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t)))))) : List<&2, U32>}
      %Equal.sym(Nat, C.high(8n, C.high(8n, Nat.add(x, C.shift(16n, LV.ev(t))))), LV.ev(t), e3) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> B.bytes_le(t) == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> CV.i2osp_le(Nat.double(j), _) : List<&2, U32>}
      %Equal.sym(List<&2, U32>, B.bytes_le(t), CV.i2osp_le(Nat.double(j), LV.ev(t)), bytes_le_v(one, h1, j, t, ht)) : {U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> _ == U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> CV.i2osp_le(Nat.double(j), LV.ev(t)) : List<&2, U32>}
      {==}

Uses (26):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=fits_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=low_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=mid_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend&name=top_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_left
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=and_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=false_true
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend&name=i2osp_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=limbs16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend&name=bytes_le