Xbits.kbit_val: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as Xbits
Lines 48-75 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&start_line=48&end_line=75

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/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

# X.kbit(bs, t) is bit t of the value of the bytes
def kbit_val(+bs: List<&2, U32>, +t: Nat, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {v(X.kbit(bs, t)) == S.kbit(FS.value(bs), t) : Nat}:
  match bs t:
    case Nil{} _:
      Equal.cong(Nat, Nat, z => C.bit(z), 0n, C.high(t, 0n), Equal.sym(Nat, C.high(t, 0n), 0n, high_zero(t)))
    case Con{+b, +bt} 0n:
      low_bit(0n, b, C.shift(7n, FS.value(bt)))
    case Con{+b, +bt} 1n:
      low_bit(1n, b, C.shift(6n, FS.value(bt)))
    case Con{+b, +bt} 2n:
      low_bit(2n, b, C.shift(5n, FS.value(bt)))
    case Con{+b, +bt} 3n:
      low_bit(3n, b, C.shift(4n, FS.value(bt)))
    case Con{+b, +bt} 4n:
      low_bit(4n, b, C.shift(3n, FS.value(bt)))
    case Con{+b, +bt} 5n:
      low_bit(5n, b, C.shift(2n, FS.value(bt)))
    case Con{+b, +bt} 6n:
      low_bit(6n, b, C.shift(1n, FS.value(bt)))
    case Con{+b, +bt} 7n:
      low_bit(7n, b, FS.value(bt))
    case Con{+b, +bt} 8n+ +q:
      +V = FS.value(bt)
      +hbl = N.le_lt_succ(v(b), 255n, LM.lea_head(b, bt, 255n, hb))
      +e1 = WI.high_comp(q, 8n, Nat.add(v(b), C.shift(8n, V)))
      +e2 = Equal.cong(Nat, Nat, z => C.high(q, z), C.high(8n, Nat.add(v(b), C.shift(8n, V))), V, WI.high_uniq(8n, v(b), V, hbl))
      +e3 = Equal.cong(Nat, Nat, z => C.bit(z), C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V))), C.high(q, V), Equal.trans(Nat, C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V))), C.high(q, C.high(8n, Nat.add(v(b), C.shift(8n, V)))), C.high(q, V), e1, e2))
      Equal.trans(Nat, v(X.kbit(bt, q)), C.bit(C.high(q, V)), C.bit(C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V)))), kbit_val(bt, q, LM.lea_tail(b, bt, 255n, hb)), Equal.sym(Nat, C.bit(C.high(Nat.add(8n, q), Nat.add(v(b), C.shift(8n, V)))), C.bit(C.high(q, V)), e3))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_head
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=lea_tail
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=high_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=low_bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_lt_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=high_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=high_uniq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=kbit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=bit
  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=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=kbit