1	import 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	
6	def 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)
10	def 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)
17	def 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
21	def 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)
27	def to_be(xs: List<&2, Nat>) -> List<&2, U32>:
28	  List.reverse(&2, U32, bytes_le(xs))
29	
30	def 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	
37	def 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	
43	def 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	
49	def head(bs: List<&2, U32>) -> U32:
50	  match bs:
51	    case Nil{}: 0
52	    case b <> t: b
53	
54	def tail(bs: List<&2, U32>) -> List<&2, U32>:
55	  match bs:
56	    case Nil{}: Nil{}
57	    case b <> t: t