check.bend
bend-osdev-gf@0.1.2.0 · 99 lines · 0 definitions
1import Base
2import bend-osdev-bytes@0.1.1.1/bytes.bend as B
3import bend-osdev-gf@0.1.2.0/gf.bend as G
4import bend-osdev-gf@0.1.2.0/tables.bend as T
5import bend-osdev-gf@0.1.2.0/gf128.bend as H
6import bend-osdev-gf@0.1.2.0/gfm.bend as M
7
8def show(x: U32) -> String:
9 U32.show(x)
10
11# The table path against the reference over every pair of bytes (and every
12# inverse): the number of disagreements. r is the table and its answer for
13# (a, b).
14def tab.count(ok: Bool, bad: Nat) -> Nat:
15 match ok:
16 case True{}:
17 bad
18 case False{}:
19 1n+bad
20
21def tab.row(n: Nat, +f: G.Gf8Field, r: T.Gf8Tab & U32, +a: U32, +b: U32, bad: Nat) -> T.Gf8Tab & Nat:
22 match n:
23 case 0n:
24 (t, v) = r
25 (t, bad)
26 case 1n+k:
27 (t, +v) = r
28 +b1 = U32.add(b, 1)
29 tab.row(k, f, T.Gf8Tab.mul(t, a, b1), a, b1, tab.count(U32.is_eq(v, G.Gf8.mul(f, a, b)), bad))
30
31def tab.all(n: Nat, +f: G.Gf8Field, r: T.Gf8Tab & Nat, +a: U32) -> T.Gf8Tab & Nat:
32 match n:
33 case 0n:
34 r
35 case 1n+k:
36 (t, bad) = r
37 tab.all(k, f, tab.row(256n, f, T.Gf8Tab.mul(t, a, 0), a, 0, bad), U32.add(a, 1))
38
39def tab.inv(n: Nat, +f: G.Gf8Field, r: T.Gf8Tab & U32, +a: U32, bad: Nat) -> Nat:
40 match n:
41 case 0n:
42 bad
43 case 1n+k:
44 (t, +v) = r
45 +a1 = U32.add(a, 1)
46 tab.inv(k, f, T.Gf8Tab.inv(t, a1), a1, tab.count(U32.is_eq(v, G.Gf8.inv(f, a)), bad))
47
48def tab.snd(r: T.Gf8Tab & Nat) -> Nat:
49 (t, n) = r
50 n
51
52def tab.check(+f: G.Gf8Field) -> Nat:
53 Nat.add(tab.snd(tab.all(256n, f, (T.Gf8Tab.new(f), 0n), 0)), tab.inv(256n, f, T.Gf8Tab.inv(T.Gf8Tab.new(f), 0), 0, 0n))
54
55def gcm_h() -> H.Gf128:
56 H.Gf128.of_words(1726565332, 4018809915, 2286746201, 3392416558)
57
58def gcm_c() -> H.Gf128:
59 H.Gf128.of_words(59300558, 1622582162, 4079534777, 1907555960)
60
61def main() -> IO(Unit):
62 do IO<Unit>:
63 IO.print(show(G.Gf8.mul(G.Gf8.aes(), 87, 131)))
64 IO.print(show(G.Gf8.mul(G.Gf8.aes(), 87, 19)))
65 IO.print(show(G.Gf8.xtime(G.Gf8.aes(), 87)))
66 IO.print(show(G.Gf8.inv(G.Gf8.aes(), 83)))
67 IO.print(Nat.show(G.Gf8.log(G.Gf8.aes(), 83)))
68 IO.print(show(G.Gf8.exp(G.Gf8.aes(), G.Gf8.log(G.Gf8.aes(), 83))))
69 IO.print(show(G.Gf8.exp(G.Gf8.rs(), 8n)))
70 IO.print(show(G.Gf8.div(G.Gf8.rs(), 1, 2)))
71 IO.print(Nat.show(tab.check(G.Gf8.aes())))
72 IO.print(Nat.show(tab.check(G.Gf8.rs())))
73 IO.print(H.Gf128.hex(H.Gf128.mul_gcm(gcm_c(), gcm_h())))
74 IO.print(H.Gf128.hex(H.Gf128.ghash(gcm_h(), [gcm_c(), H.Gf128.of_words(0, 0, 0, 128)])))
75 IO.print(H.Gf128.hex(H.Gf128.double_be(H.Gf128.of_words(2113366796, 448305587, 1044574279, 3105576047))))
76 IO.print(H.Gf128.hex(H.Gf128.double_le(H.Gf128.of_words(0, 0, 0, 255))))
77 IO.print(show(M.Gfm.mul(M.Gfm.bch13(), 1234, 5678)))
78 IO.print(show(M.Gfm.inv(M.Gfm.bch13(), 1234)))
79 IO.print(show(M.Gfm.log(M.Gfm.bch13(), 1234)))
80 IO.print(show(M.Gfm.exp(M.Gfm.bch14(), 16383)))
81
82#|193
83#|254
84#|174
85#|202
86#|48
87#|83
88#|29
89#|142
90#|0
91#|0
92#|5e2ec746917062882c85b0685353deb7
93#|f38cbb1ad69223dcc3457ae5b6b0f885
94#|fbeed618357133667c85e08f7236a8de
95#|870000000000000000000000000000fe
96#|4994
97#|2297
98#|2924
99#|1