LAWS.bend open laws/TODOs

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

6 imports

import Base
import ./sha256.bend as Runtime
import ./buffer.bend as Buffer
import ./legacy_model.bend as SHA
import ./fips.bend as FIPS
import ./packed_spec.bend as PackedSpec

Laws

law constants_correct provedin CORRECTNESS.bendsource · line 10 · raw

{0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.constants == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.constants : List<&2, U32>}

These claims mention the actual public API and the complete independent spec. There are no arbitrary preprocessing functions, tables, or correctness premises.

law sha256_correct provedin CORRECTNESS.bendsource · line 13 · raw

@+bytes:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.sha256(bytes) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.sha256(bytes) : List<&2, U32>}

law digest_bytes_correct provedin CORRECTNESS.bendsource · line 17 · raw

@+ws:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.digest_bytes(ws) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.digest_octets(ws) : List<&2, U32>}

law sha256_bytes_correct provedin CORRECTNESS.bendsource · line 21 · raw

@+bytes:List<&2, U32> -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.sha256_bytes(bytes) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.sha256_bytes(bytes) : List<&2, U32>}

law sha256_bytes_length provedin CORRECTNESS.bendsource · line 25 · raw

@+bytes:List<&2, U32> -> {List.length(&2, U32, 0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.sha256_bytes(bytes)) == 32n : Nat}

law sha256_packed_correct provedin CORRECTNESS.bendsource · line 30 · raw

@words:Array<U32> -> @+byte_length:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.sha256_packed(words, byte_length) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.sha256(words, byte_length) : Maybe<&2, List<&2, U32>>}

A separate packed-format contract; the original list-to-FIPS theorem is unchanged.

law sha256_array_correct provedin CORRECTNESS.bendsource · line 36 · raw

@words:Array<U32> -> @+byte_length:Nat -> {0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.sha256(words, byte_length) == 0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer.result(0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.hash(words, byte_length)) : Maybe<&1, Array<U32>>}

Actual production array API; historical list laws above concern only its model.