~/bend-docscommunity

proofs/crypto/sha/packed/laws.bend fails

raw source on the hub · import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/laws.bend as Laws

6 imports
import Base
import ../../../../src/crypto/sha/packed/sha256.bend as Runtime
import ../../../../src/crypto/sha/packed/buffer.bend as Buffer
import ./legacy_model.bend as SHA
import ../../../../spec/crypto/sha.bend as FIPS
import ../../../../spec/crypto/sha/packed.bend as PackedSpec

Laws

law constants_correct openits proof in main.bend does not pass the checker (fails)source · line 10 · raw

{0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.constants == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.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 openits proof in main.bend does not pass the checker (fails)source · line 13 · raw

@+bytes:List<&2, U32> -> {0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.sha256(bytes) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.sha256(bytes) : List<&2, U32>}

law digest_bytes_correct openits proof in main.bend does not pass the checker (fails)source · line 17 · raw

@+ws:List<&2, U32> -> {0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.digest_bytes(ws) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.digest_octets(ws) : List<&2, U32>}

law sha256_bytes_correct openits proof in main.bend does not pass the checker (fails)source · line 21 · raw

@+bytes:List<&2, U32> -> {0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.sha256_bytes(bytes) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.sha256_bytes(bytes) : List<&2, U32>}

law sha256_bytes_length openits proof in main.bend does not pass the checker (fails)source · line 25 · raw

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

law sha256_packed_correct openits proof in main.bend does not pass the checker (fails)source · line 30 · raw

@words:Array<U32> -> @+byte_length:Nat -> {0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.sha256_packed(words, byte_length) == 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.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 openits proof in main.bend does not pass the checker (fails)source · line 36 · raw

@words:Array<U32> -> @+byte_length:Nat -> {0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/sha256.sha256(words, byte_length) == 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.result(0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.hash(words, byte_length)) : Maybe<&1, Array<U32>>}

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