gfm.bend
bend-osdev-gf@0.1.0.0 · 121 lines · 0 definitions
1# bend-osdev-gf, GF(2^m) for small m (2 to 16): the fields BCH codes work
2# in (Lin and Costello, "Error Control Coding", chapters 2 and 6).
3#
4# An element is a number below 2^m held in U32 (bit i the coefficient of
5# x^i; arguments are read modulo 2^m). A GfmField names m and the reduction
6# polynomial with all its bits (x^m included). The named fields use
7# primitive polynomials, so x (2) generates the multiplicative group and
8# Gfm.exp / Gfm.log are to base x.
9import Base
10
11type GfmField is Data:
12 GfmField{m: Nat, poly: U32}
13
14# x^4 + x + 1
15def Gfm.gf16() -> GfmField:
16 GfmField{4n, 19}
17
18# x^5 + x^2 + 1
19def Gfm.gf32() -> GfmField:
20 GfmField{5n, 37}
21
22# x^13 + x^4 + x^3 + x + 1 (0x201B), for BCH over 8191-bit codewords
23def Gfm.bch13() -> GfmField:
24 GfmField{13n, 8219}
25
26# x^14 + x^10 + x^6 + x + 1 (0x4443)
27def Gfm.bch14() -> GfmField:
28 GfmField{14n, 17475}
29
30def Gfm.m(f: GfmField) -> Nat:
31 match f:
32 case GfmField{m, poly}:
33 m
34
35# 2^m - 1, and the number of nonzero elements
36def Gfm.mask(f: GfmField) -> U32:
37 match f:
38 case GfmField{m, poly}:
39 U32.sub(U32.shln(1, m), 1)
40
41def Gfm.elt(f: GfmField, a: U32) -> U32:
42 U32.and(Gfm.mask(f), a)
43
44def Gfm.add(+f: GfmField, a: U32, b: U32) -> U32:
45 Gfm.elt(f, U32.xor(a, b))
46
47# all ones if the low bit of b is set, else 0
48def gfm.mask(b: U32) -> U32:
49 U32.sub(0, U32.and(b, 1))
50
51# a * x for a below 2^m: shift, and reduce if x^m appeared
52def gfm.x(+m: Nat, +poly: U32, a: U32) -> U32:
53 +s = U32.shl(a)
54 U32.xor(s, U32.and(poly, gfm.mask(U32.shrn(s, m))))
55
56def Gfm.xtime(+f: GfmField, a: U32) -> U32:
57 match f:
58 case GfmField{+m, +poly}:
59 gfm.x(m, poly, Gfm.elt(GfmField{m, poly}, a))
60
61# the product, over the m bits of b from the bottom: p += a * bit; a *= x
62def gfm.mul.go(n: Nat, +m: Nat, +poly: U32, +a: U32, +b: U32, p: U32) -> U32:
63 match n:
64 case 0n:
65 p
66 case 1n+k:
67 gfm.mul.go(k, m, poly, gfm.x(m, poly, a), U32.shr(b), U32.xor(p, U32.and(a, gfm.mask(b))))
68
69# the product of a and b, both below 2^m (matching both first, so that the
70# product of unknown values stays a small term for the proof checkers)
71def gfm.mul.raw(f: GfmField, a: U32, b: U32) -> U32:
72 match f a b:
73 case GfmField{+m, +poly} U32{wa} U32{wb}:
74 gfm.mul.go(m, m, poly, U32{wa}, U32{wb}, 0)
75
76def Gfm.mul(+f: GfmField, a: U32, b: U32) -> U32:
77 gfm.mul.raw(f, Gfm.elt(f, a), Gfm.elt(f, b))
78
79# a^e by squaring, over the 32 bits of e from the top
80def gfm.pow.go(n: Nat, +f: GfmField, +a: U32, +e: U32, +r: U32) -> U32:
81 match n:
82 case 0n:
83 r
84 case 1n+k:
85 +sq = Gfm.mul(f, r, r)
86 gfm.pow.go(k, f, a, U32.shl(e), Gfm.mul(f, sq, U32.or(U32.and(a, gfm.mask(U32.shrn(e, 31n))), U32.and(1, U32.not(gfm.mask(U32.shrn(e, 31n)))))))
87
88def gfm.pow.start(+f: GfmField, x: U32, e: U32) -> U32:
89 match x:
90 case U32{w}:
91 gfm.pow.go(32n, f, U32{w}, e, 1)
92
93# a^e (a^0 = 1)
94def Gfm.pow(+f: GfmField, +a: U32, e: U32) -> U32:
95 gfm.pow.start(f, Gfm.elt(f, a), e)
96
97# a^-1 = a^(2^m - 2); the inverse of 0 is 0
98def Gfm.inv(+f: GfmField, +a: U32) -> U32:
99 Gfm.pow(f, a, U32.sub(Gfm.mask(f), 1))
100
101def Gfm.div(+f: GfmField, a: U32, +b: U32) -> U32:
102 Gfm.mul(f, a, Gfm.inv(f, b))
103
104# x^i
105def Gfm.exp(+f: GfmField, i: U32) -> U32:
106 Gfm.pow(f, 2, i)
107
108# the least i with x^i = a, searching i below 2^m - 1 (0 for a = 0)
109def Gfm.log.go(n: Nat, hit: Bool, +f: GfmField, +a: U32, +cur: U32, +i: U32) -> U32:
110 match n hit:
111 case _ True{}:
112 i
113 case 0n False{}:
114 0
115 case 1n+k False{}:
116 +nxt = Gfm.xtime(f, cur)
117 Gfm.log.go(k, U32.is_eq(nxt, a), f, a, nxt, U32.add(i, 1))
118
119def Gfm.log(+f: GfmField, a: U32) -> U32:
120 +e = Gfm.elt(f, a)
121 Gfm.log.go(U32.to_nat(Gfm.mask(f)), U32.is_eq(1, e), f, e, 1, 0)