PROOF.bend
bend-osdev-crc@0.1.0.0 · 161 lines · 6 definitions
1import Base
2import bend-osdev-word64@0.1.0.0/word64.bend as W
3import bend-osdev-bytes@0.1.0.0/bytes.bend as B
4import bend-osdev-crc@0.1.0.0/crc.bend as C
5import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL
6import bend-osdev-bytes@0.1.0.0/PROOF.bend as BP
7import bend-osdev-crc@0.1.0.0/LAWS.bend as Laws
8
9
10
11
12def r32_split(xs: List<&2, U32>, +poly: U32, c: U32, ys: List<&2, U32>) -> {C.r32.raw(B.append(xs, ys), poly, c) == C.r32.raw(ys, poly, C.r32.raw(xs, poly, c)) : U32}:
13 match xs:
14 case Nil{}:
15 {==}
16 case Con{h, t}:
17 r32_split(t, poly, C.r32.bits(8n, poly, U32.xor(c, U32.and(h, 255))), ys)
18
19def n32_split(xs: List<&2, U32>, +poly: U32, +shift: Nat, +topbit: U32, +mask: U32, c: U32, ys: List<&2, U32>) -> {C.n32.raw(B.append(xs, ys), poly, shift, topbit, mask, c) == C.n32.raw(ys, poly, shift, topbit, mask, C.n32.raw(xs, poly, shift, topbit, mask, c)) : U32}:
20 match xs:
21 case Nil{}:
22 {==}
23 case Con{h, t}:
24 n32_split(t, poly, shift, topbit, mask, C.n32.bits(8n, poly, topbit, mask, U32.xor(c, U32.shln(U32.and(h, 255), shift))), ys)
25
26def s32_split(xs: List<&2, U32>, +poly: U32, +topsh: Nat, +mask: U32, c: U32, ys: List<&2, U32>) -> {C.s32.raw(B.append(xs, ys), poly, topsh, mask, c) == C.s32.raw(ys, poly, topsh, mask, C.s32.raw(xs, poly, topsh, mask, c)) : U32}:
27 match xs:
28 case Nil{}:
29 {==}
30 case Con{h, t}:
31 s32_split(t, poly, topsh, mask, C.s32.bits(8n, poly, topsh, mask, U32.and(h, 255), c), ys)
32
33def r64_split(xs: List<&2, U32>, +poly: W.W64, c: W.W64, ys: List<&2, U32>) -> {C.r64.raw(B.append(xs, ys), poly, c) == C.r64.raw(ys, poly, C.r64.raw(xs, poly, c)) : W.W64}:
34 match xs:
35 case Nil{}:
36 {==}
37 case Con{h, t}:
38 r64_split(t, poly, C.r64.bits(8n, poly, W.W64.xor(c, W.W64.from_u32(U32.and(h, 255)))), ys)
39
40def n64_split(xs: List<&2, U32>, +poly: W.W64, c: W.W64, ys: List<&2, U32>) -> {C.n64.raw(B.append(xs, ys), poly, c) == C.n64.raw(ys, poly, C.n64.raw(xs, poly, c)) : W.W64}:
41 match xs:
42 case Nil{}:
43 {==}
44 case Con{h, t}:
45 n64_split(t, poly, C.n64.bits(8n, poly, W.W64.xor(c, W.W64.from_parts(U32.shln(U32.and(h, 255), 24n), 0))), ys)
46
47
48def msb_split(+small: Bool, +width: Nat, +poly: U32, c: U32, xs: List<&2, U32>, ys: List<&2, U32>) -> {C.Crc32Spec.update.msb(small, width, poly, c, B.append(xs, ys)) == C.Crc32Spec.update.msb(small, width, poly, C.Crc32Spec.update.msb(small, width, poly, c, xs), ys) : U32}:
49 match small:
50 case True{}:
51 s32_split(xs, poly, Nat.sub(width, 1n), U32.sub(U32.shln(1, width), 1), c, ys)
52 case False{}:
53 n32_split(xs, poly, Nat.sub(width, 8n), U32.shln(1, Nat.sub(width, 1n)), U32.sub(U32.shln(1, width), 1), c, ys)
54
55
56
57def Laws.streaming32(spec, c, a, b):
58 match spec:
59 case C.Crc32Spec{+width, +poly, init, reflected, xorout}:
60 match reflected:
61 case True{}:
62 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {C.r32.raw(_, C.reflect32(poly, width), c) == C.r32.raw(B.Octets.to_list(b), C.reflect32(poly, width), C.r32.raw(B.Octets.to_list(a), C.reflect32(poly, width), c)) : U32}
63 r32_split(B.Octets.to_list(a), C.reflect32(poly, width), c, B.Octets.to_list(b))
64 case False{}:
65 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {C.Crc32Spec.update.msb(Nat.is_lt(width, 8n), width, poly, c, _) == C.Crc32Spec.update.msb(Nat.is_lt(width, 8n), width, poly, C.Crc32Spec.update.msb(Nat.is_lt(width, 8n), width, poly, c, B.Octets.to_list(a)), B.Octets.to_list(b)) : U32}
66 msb_split(Nat.is_lt(width, 8n), width, poly, c, B.Octets.to_list(a), B.Octets.to_list(b))
67
68def Laws.streaming64(spec, c, a, b):
69 match spec:
70 case C.Crc64Spec{+poly, init, reflected, xorout}:
71 match reflected:
72 case True{}:
73 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {C.r64.raw(_, C.reflect64(poly), c) == C.r64.raw(B.Octets.to_list(b), C.reflect64(poly), C.r64.raw(B.Octets.to_list(a), C.reflect64(poly), c)) : W.W64}
74 r64_split(B.Octets.to_list(a), C.reflect64(poly), c, B.Octets.to_list(b))
75 case False{}:
76 %Equal.sym(List<&2, U32>, B.Octets.to_list(B.Octets.append(a, b)), B.append(B.Octets.to_list(a), B.Octets.to_list(b)), BL.octets_append_list(a, b)) : {C.n64.raw(_, poly, c) == C.n64.raw(B.Octets.to_list(b), poly, C.n64.raw(B.Octets.to_list(a), poly, c)) : W.W64}
77 n64_split(B.Octets.to_list(a), poly, c, B.Octets.to_list(b))
78
79def Laws.check_crc32c():
80 {==}
81
82def Laws.check_crc32():
83 {==}
84
85def Laws.check_crc16():
86 {==}
87
88def Laws.check_crc_t10dif():
89 {==}
90
91def Laws.check_crc64_ecma():
92 {==}
93
94def Laws.check_crc64_xz():
95 {==}
96
97def Laws.check_crc64_nvme():
98 {==}
99
100def Laws.empty_crc32c():
101 {==}
102
103def Laws.empty_crc_t10dif():
104 {==}
105
106def Laws.fast_crc32c():
107 {==}
108
109def Laws.fast_crc16():
110 {==}
111
112def Laws.fast_crc_t10dif():
113 {==}
114
115def Laws.fast_crc64_ecma():
116 {==}
117
118def Laws.fast_crc64_xz():
119 {==}
120
121def Laws.fast_agrees_crc32c():
122 {==}
123
124def Laws.check_crc4_itu():
125 {==}
126
127def Laws.check_crc7_mmc():
128 {==}
129
130def Laws.check_crc8_smbus():
131 {==}
132
133def Laws.check_crc8_itu():
134 {==}
135
136def Laws.check_crc8_maxim():
137 {==}
138
139def Laws.check_crc8_dvb_s2():
140 {==}
141
142def Laws.check_crc8_autosar():
143 {==}
144
145def Laws.check_crc16_kermit():
146 {==}
147
148def Laws.check_crc16_ccitt_false():
149 {==}
150
151def Laws.check_crc16_xmodem():
152 {==}
153
154def Laws.fast_crc7_mmc():
155 {==}
156
157def Laws.fast_crc4_itu():
158 {==}
159
160def Laws.fast_crc16_xmodem():
161 {==}