X25519.kbit: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X25519
Lines 18-42 of bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&start_line=18&end_line=42

import Base

# bit t of a little-endian byte string
def kbit(bs: List<&2, U32>, t: Nat) -> U32:
  match bs:
    case Nil{}:
      0
    case Con{b, bt}:
      match t:
        case 0n:
          U32.and(b, 1)
        case 1n:
          U32.and(U32.shrn(b, 1n), 1)
        case 2n:
          U32.and(U32.shrn(b, 2n), 1)
        case 3n:
          U32.and(U32.shrn(b, 3n), 1)
        case 4n:
          U32.and(U32.shrn(b, 4n), 1)
        case 5n:
          U32.and(U32.shrn(b, 5n), 1)
        case 6n:
          U32.and(U32.shrn(b, 6n), 1)
        case 7n:
          U32.and(U32.shrn(b, 7n), 1)
        case 8n+q:
          kbit(bt, q)

Uses (5):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.shrn