src/crypto/secp256k1/bytes.bend

bend-collections-laws-crypto@1.0.0.0 · 57 lines · 10 definitions

1import Base
2
3# Octet strings and 16-bit limbs. Bytes are U32 values; only the low 8 bits
4# of a byte are read (the library's byte convention keeps them below 256).
5
6def byte(+b: U32) -> Nat:
7  U32.to_nat(U32.and(b, 255))
8
9# little-endian limbs of little-endian bytes (two bytes per limb)
10def limbs_le(bs: List<&2, U32>) -> List<&2, Nat>:
11  match bs:
12    case Nil{}: Nil{}
13    case b0 <> Nil{}: [byte(b0)]
14    case b0 <> b1 <> t: Nat.add(Nat.mul(byte(b1), 256n), byte(b0)) <> limbs_le(t)
15
16# the 16 limbs of a 32-byte big-endian string (SEC 1 OS2IP)
17def of_be(bs: List<&2, U32>) -> List<&2, Nat>:
18  limbs_le(List.reverse(&2, U32, bs))
19
20# little-endian bytes of limbs below 2^16
21def bytes_le(xs: List<&2, Nat>) -> List<&2, U32>:
22  match xs:
23    case Nil{}: Nil{}
24    case +x <> t: U32.from_nat(Nat.mod(x, 256n)) <> U32.from_nat(Nat.div(x, 256n)) <> bytes_le(t)
25
26# the 32-byte big-endian string of 16 limbs (SEC 1 I2OSP)
27def to_be(xs: List<&2, Nat>) -> List<&2, U32>:
28  List.reverse(&2, U32, bytes_le(xs))
29
30def has_len(n: Nat, bs: List<&2, U32>) -> Bool:
31  match n bs:
32    case 0n Nil{}: True{}
33    case 0n b <> t: False{}
34    case 1n+k Nil{}: False{}
35    case 1n+k b <> t: has_len(k, t)
36
37def prefix(n: Nat, bs: List<&2, U32>) -> List<&2, U32>:
38  match n bs:
39    case 0n _: Nil{}
40    case 1n+k Nil{}: Nil{}
41    case 1n+k b <> t: b <> prefix(k, t)
42
43def suffix(n: Nat, bs: List<&2, U32>) -> List<&2, U32>:
44  match n bs:
45    case 0n _: bs
46    case 1n+k Nil{}: Nil{}
47    case 1n+k b <> t: suffix(k, t)
48
49def head(bs: List<&2, U32>) -> U32:
50  match bs:
51    case Nil{}: 0
52    case b <> t: b
53
54def tail(bs: List<&2, U32>) -> List<&2, U32>:
55  match bs:
56    case Nil{}: Nil{}
57    case b <> t: t