LAWS.bend open laws/TODOs

raw source on the hub · import 0xff0c68fa4ce715b1f30ee5944192f0b7/LAWS.bend as LAWS

Definitional laws for Crc32's Base-only List<&2, U32> API.

2 imports

import Base
import ./lib.bend as Crc

Laws

law encode_empty provedin PROOF.bendsource · line 6 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([]) == 0 : U32}

The standard empty CRC is zero after init and final XOR.

law encode_zero_octet provedin PROOF.bendsource · line 10 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([0]) == 3523407757 : U32}

A zero octet is the standard CRC-32 vector D202EF8D.

law encode_check_vector provedin PROOF.bendsource · line 14 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([49, 50, 51, 52, 53, 54, 55, 56, 57]) == 3421780262 : U32}

The canonical CRC-32 check vector for ASCII "123456789" is CBF43926.

law encode_hello provedin PROOF.bendsource · line 22 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([104, 101, 108, 108, 111]) == 907060870 : U32}

A second short ASCII vector: CRC-32("hello") = 3610A686.

law encode_masks_octet provedin PROOF.bendsource · line 30 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([256]) == 0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.encode([0]) : U32}

Values are interpreted as octets, so high bits are ignored.

law finalize_update_empty provedin PROOF.bendsource · line 34 · raw

{0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.finalize(0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.update(0xff0c68fa4ce715b1f30ee5944192f0b7/lib.Crc32.init, [])) == 0 : U32}

Finalization is the same operation exposed independently.