LAWS.bend

bend-osdev-crc@0.1.0.0 · 121 lines · 30 definitions

1# Properties, for every input: a CRC computed in pieces is the CRC of the
2# whole, for every parameter set, at both word sizes. The register passes from
3# one piece to the next through update; start and finish apply once.
4#
5# Vectors: every named CRC gives the reveng catalogue's check value on the
6# nine bytes "123456789".
7import Base
8import bend-osdev-word64@0.1.0.0/word64.bend as W
9import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10import bend-osdev-crc@0.1.0.0/crc.bend as C
11import bend-osdev-crc@0.1.0.0/table.bend as T
12
13law streaming32:
14  for spec: C.Crc32Spec
15  for c: U32
16  for +a: B.Octets
17  for +b: B.Octets
18  {C.Crc32Spec.update(spec, c, B.Octets.append(a, b)) == C.Crc32Spec.update(spec, C.Crc32Spec.update(spec, c, a), b) : U32}
19
20law streaming64:
21  for spec: C.Crc64Spec
22  for c: W.W64
23  for +a: B.Octets
24  for +b: B.Octets
25  {C.Crc64Spec.update(spec, c, B.Octets.append(a, b)) == C.Crc64Spec.update(spec, C.Crc64Spec.update(spec, c, a), b) : W.W64}
26
27# check values (reveng): 0xE3069283, 0xCBF43926, 0xBB3D, 0xD0DB
28law check_crc32c:
29  {C.crc32c(B.Octets.of_string("123456789")) == 3808858755 : U32}
30
31law check_crc32:
32  {C.crc32(B.Octets.of_string("123456789")) == 3421780262 : U32}
33
34law check_crc16:
35  {C.crc16(B.Octets.of_string("123456789")) == 47933 : U32}
36
37law check_crc_t10dif:
38  {C.crc_t10dif(B.Octets.of_string("123456789")) == 53467 : U32}
39
40# 0x6C40DF5F0B497347, 0x995DC9BBDF1939FA, 0xAE8B14860A799888
41law check_crc64_ecma:
42  {C.crc64_ecma(B.Octets.of_string("123456789")) == W.W64.from_parts(1816190815, 189363015) : W.W64}
43
44law check_crc64_xz:
45  {C.crc64_xz(B.Octets.of_string("123456789")) == W.W64.from_parts(2573060539, 3742972410) : W.W64}
46
47law check_crc64_nvme:
48  {C.crc64_nvme(B.Octets.of_string("123456789")) == W.W64.from_parts(2928350342, 175741064) : W.W64}
49
50# the empty input: init XOR xorout
51law empty_crc32c:
52  {C.crc32c(B.Octets.empty()) == 0 : U32}
53
54law empty_crc_t10dif:
55  {C.crc_t10dif(B.Octets.empty()) == 0 : U32}
56
57# The table-driven fast path (table.bend) gives the same check values, and
58# agrees with the reference on a longer input. Vectors only: a law for every
59# input would need lemmas about Array's internals.
60
61law fast_crc32c:
62  {T.Crc32Spec.compute_fast(C.crc32c.spec(), B.Octets.of_string("123456789")) == 3808858755 : U32}
63
64law fast_crc16:
65  {T.Crc32Spec.compute_fast(C.crc16.spec(), B.Octets.of_string("123456789")) == 47933 : U32}
66
67law fast_crc_t10dif:
68  {T.Crc32Spec.compute_fast(C.crc_t10dif.spec(), B.Octets.of_string("123456789")) == 53467 : U32}
69
70law fast_crc64_ecma:
71  {T.Crc64Spec.compute_fast(C.crc64_ecma.spec(), B.Octets.of_string("123456789")) == W.W64.from_parts(1816190815, 189363015) : W.W64}
72
73law fast_crc64_xz:
74  {T.Crc64Spec.compute_fast(C.crc64_xz.spec(), B.Octets.of_string("123456789")) == W.W64.from_parts(2573060539, 3742972410) : W.W64}
75
76law fast_agrees_crc32c:
77  {T.Crc32Spec.compute_fast(C.crc32c.spec(), B.Octets.of_string("bend-osdev: componentised, changeable, proved")) == C.crc32c(B.Octets.of_string("bend-osdev: componentised, changeable, proved")) : U32}
78
79# More named CRCs from the reveng catalogue, with their check values: CRC-4/
80# G-704 0x7, CRC-7/MMC 0x75, CRC-8/SMBUS 0xF4, CRC-8/I-432-1 0xA1,
81# CRC-8/MAXIM-DOW 0xA1, CRC-8/DVB-S2 0xBC, CRC-8/AUTOSAR 0xDF, CRC-16/KERMIT
82# 0x2189, CRC-16/IBM-3740 0x29B1, CRC-16/XMODEM 0x31C3
83
84law check_crc4_itu:
85  {C.crc4_itu(B.Octets.of_string("123456789")) == 7 : U32}
86
87law check_crc7_mmc:
88  {C.crc7_mmc(B.Octets.of_string("123456789")) == 117 : U32}
89
90law check_crc8_smbus:
91  {C.crc8_smbus(B.Octets.of_string("123456789")) == 244 : U32}
92
93law check_crc8_itu:
94  {C.crc8_itu(B.Octets.of_string("123456789")) == 161 : U32}
95
96law check_crc8_maxim:
97  {C.crc8_maxim(B.Octets.of_string("123456789")) == 161 : U32}
98
99law check_crc8_dvb_s2:
100  {C.crc8_dvb_s2(B.Octets.of_string("123456789")) == 188 : U32}
101
102law check_crc8_autosar:
103  {C.crc8_autosar(B.Octets.of_string("123456789")) == 223 : U32}
104
105law check_crc16_kermit:
106  {C.crc16_kermit(B.Octets.of_string("123456789")) == 8585 : U32}
107
108law check_crc16_ccitt_false:
109  {C.crc16_ccitt_false(B.Octets.of_string("123456789")) == 10673 : U32}
110
111law check_crc16_xmodem:
112  {C.crc16_xmodem(B.Octets.of_string("123456789")) == 12739 : U32}
113
114law fast_crc7_mmc:
115  {T.Crc32Spec.compute_fast(C.crc7_mmc.spec(), B.Octets.of_string("123456789")) == 117 : U32}
116
117law fast_crc4_itu:
118  {T.Crc32Spec.compute_fast(C.crc4_itu.spec(), B.Octets.of_string("123456789")) == 7 : U32}
119
120law fast_crc16_xmodem:
121  {T.Crc32Spec.compute_fast(C.crc16_xmodem.spec(), B.Octets.of_string("123456789")) == 12739 : U32}