octets.bend

bend-osdev-crypto@0.1.0.0 · 90 lines · 12 definitions

1# Byte-string helpers the modes and MACs share: XOR of two byte strings, a
2# byte repeated, and a message cut into pieces of a block size.
3import Base
4import bend-osdev-bytes@0.1.0.0/bytes.bend as B
5
6# xs xor ys, element by element, over xs's length (a missing element of ys
7# counts as 0)
8def cr.oct.xorl(xs: List<&2, U32>, ys: List<&2, U32>) -> List<&2, U32>:
9  match xs:
10    case Nil{}:
11      Nil{}
12    case Con{x, xt}:
13      match ys:
14        case Nil{}:
15          Con{U32.xor(x, 0), cr.oct.xorl(xt, Nil{})}
16        case Con{y, yt}:
17          Con{U32.xor(x, y), cr.oct.xorl(xt, yt)}
18
19# a xor b, byte by byte, over a's length (b's missing bytes count as 0)
20def CrOct.xor(a: B.Octets, b: B.Octets) -> B.Octets:
21  B.Octets.of_list(cr.oct.xorl(B.Octets.to_list(a), B.Octets.to_list(b)))
22
23def cr.oct.rep(n: Nat, +b: U32) -> List<&2, U32>:
24  match n:
25    case 0n:
26      Nil{}
27    case 1n+p:
28      Con{b, cr.oct.rep(p, b)}
29
30# the byte b, n times
31def CrOct.rep(n: Nat, +b: U32) -> B.Octets:
32  B.Octets.of_list(cr.oct.rep(n, b))
33
34def cr.oct.rev(xs: List<&2, U32>, acc: List<&2, U32>) -> List<&2, U32>:
35  match xs:
36    case Nil{}:
37      acc
38    case Con{h, t}:
39      cr.oct.rev(t, Con{h, acc})
40
41def cr.oct.revs(xs: List<&2, List<&2, U32>>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
42  match xs:
43    case Nil{}:
44      acc
45    case Con{h, t}:
46      cr.oct.revs(t, Con{h, acc})
47
48def cr.oct.flush(cur: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
49  match cur:
50    case Nil{}:
51      acc
52    case Con{h, t}:
53      Con{cr.oct.rev(Con{h, t}, Nil{}), acc}
54
55def cr.oct.pieces.step(full: Bool, +c: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
56  match full:
57    case True{}:
58      Con{cr.oct.rev(c, Nil{}), acc}
59    case False{}:
60      acc
61
62def cr.oct.pieces.cur(full: Bool, +c: List<&2, U32>) -> List<&2, U32>:
63  match full:
64    case True{}:
65      Nil{}
66    case False{}:
67      c
68
69def cr.oct.pieces.i(full: Bool, +i: Nat) -> Nat:
70  match full:
71    case True{}:
72      0n
73    case False{}:
74      i
75
76# the pieces of xs, last first: whole n-byte pieces, then what is left
77# (cur: the piece being filled, reversed, i bytes long)
78def cr.oct.pieces.go(xs: List<&2, U32>, +n: Nat, +i: Nat, +cur: List<&2, U32>, acc: List<&2, List<&2, U32>>) -> List<&2, List<&2, U32>>:
79  match xs:
80    case Nil{}:
81      cr.oct.flush(cur, acc)
82    case Con{x, t}:
83      +c : List<&2, U32> = Con{x, cur}
84      +full = Nat.is_eq(1n+i, n)
85      cr.oct.pieces.go(t, n, cr.oct.pieces.i(full, 1n+i), cr.oct.pieces.cur(full, c), cr.oct.pieces.step(full, c, acc))
86
87# xs cut into pieces of n bytes, in order: every piece but the last has n
88# bytes, the last 1 to n (no pieces for no bytes)
89def CrOct.pieces(n: Nat, xs: List<&2, U32>) -> List<&2, List<&2, U32>>:
90  cr.oct.revs(cr.oct.pieces.go(xs, n, 0n, Nil{}, Nil{}), Nil{})