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".
7	import Base
8	import bend-osdev-word64@0.1.0.0/word64.bend as W
9	import bend-osdev-bytes@0.1.0.0/bytes.bend as B
10	import ./crc.bend as C
11	import ./table.bend as T
12	
13	law 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	
20	law 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
28	law check_crc32c:
29	  {C.crc32c(B.Octets.of_string("123456789")) == 3808858755 : U32}
30	
31	law check_crc32:
32	  {C.crc32(B.Octets.of_string("123456789")) == 3421780262 : U32}
33	
34	law check_crc16:
35	  {C.crc16(B.Octets.of_string("123456789")) == 47933 : U32}
36	
37	law check_crc_t10dif:
38	  {C.crc_t10dif(B.Octets.of_string("123456789")) == 53467 : U32}
39	
40	# 0x6C40DF5F0B497347, 0x995DC9BBDF1939FA, 0xAE8B14860A799888
41	law check_crc64_ecma:
42	  {C.crc64_ecma(B.Octets.of_string("123456789")) == W.W64.from_parts(1816190815, 189363015) : W.W64}
43	
44	law check_crc64_xz:
45	  {C.crc64_xz(B.Octets.of_string("123456789")) == W.W64.from_parts(2573060539, 3742972410) : W.W64}
46	
47	law 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
51	law empty_crc32c:
52	  {C.crc32c(B.Octets.empty()) == 0 : U32}
53	
54	law 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	
61	law fast_crc32c:
62	  {T.Crc32Spec.compute_fast(C.crc32c.spec(), B.Octets.of_string("123456789")) == 3808858755 : U32}
63	
64	law fast_crc16:
65	  {T.Crc32Spec.compute_fast(C.crc16.spec(), B.Octets.of_string("123456789")) == 47933 : U32}
66	
67	law fast_crc_t10dif:
68	  {T.Crc32Spec.compute_fast(C.crc_t10dif.spec(), B.Octets.of_string("123456789")) == 53467 : U32}
69	
70	law 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	
73	law 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	
76	law 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	
84	law check_crc4_itu:
85	  {C.crc4_itu(B.Octets.of_string("123456789")) == 7 : U32}
86	
87	law check_crc7_mmc:
88	  {C.crc7_mmc(B.Octets.of_string("123456789")) == 117 : U32}
89	
90	law check_crc8_smbus:
91	  {C.crc8_smbus(B.Octets.of_string("123456789")) == 244 : U32}
92	
93	law check_crc8_itu:
94	  {C.crc8_itu(B.Octets.of_string("123456789")) == 161 : U32}
95	
96	law check_crc8_maxim:
97	  {C.crc8_maxim(B.Octets.of_string("123456789")) == 161 : U32}
98	
99	law check_crc8_dvb_s2:
100	  {C.crc8_dvb_s2(B.Octets.of_string("123456789")) == 188 : U32}
101	
102	law check_crc8_autosar:
103	  {C.crc8_autosar(B.Octets.of_string("123456789")) == 223 : U32}
104	
105	law check_crc16_kermit:
106	  {C.crc16_kermit(B.Octets.of_string("123456789")) == 8585 : U32}
107	
108	law check_crc16_ccitt_false:
109	  {C.crc16_ccitt_false(B.Octets.of_string("123456789")) == 10673 : U32}
110	
111	law check_crc16_xmodem:
112	  {C.crc16_xmodem(B.Octets.of_string("123456789")) == 12739 : U32}
113	
114	law fast_crc7_mmc:
115	  {T.Crc32Spec.compute_fast(C.crc7_mmc.spec(), B.Octets.of_string("123456789")) == 117 : U32}
116	
117	law fast_crc4_itu:
118	  {T.Crc32Spec.compute_fast(C.crc4_itu.spec(), B.Octets.of_string("123456789")) == 7 : U32}
119	
120	law fast_crc16_xmodem:
121	  {T.Crc32Spec.compute_fast(C.crc16_xmodem.spec(), B.Octets.of_string("123456789")) == 12739 : U32}