0x3bdc0c9f checks

0x3bdc0c9f5265bb49f7fc76b61f529f24

no description

Anonymous package: import it by hash.

Earlier versions (1)

0xda83506f 2026-09-20

Published: 2026-09-30
Size: 580,741 bytes, 19 files
License: MIT-0 (no LICENSE file; the hub's default)
Declarations: 152 laws (152 proved), 285 defs, 3 types

Import

import 0x3bdc0c9f5265bb49f7fc76b61f529f24/CORRECTNESS.bend as CORRECTNESS
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/LAWS.bend as LAWS
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/PROOF.bend as PROOF
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer.bend as Buffer
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/buffer_proof.bend as Buffer_proof
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/conformance.bend as Conformance
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/core.bend as Core
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/core_model.bend as Core_model
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/fips.bend as Fips
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/legacy_model.bend as Legacy_model
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/list_proofs.bend as List_proofs
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/package.bend as Package
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed.bend as Packed
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_array_proof.bend as Packed_array_proof
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_proof.bend as Packed_proof
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/packed_spec.bend as Packed_spec
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/padding_proof.bend as Padding_proof
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as Sha256
import 0x3bdc0c9f5265bb49f7fc76b61f529f24/state.bend as State

Modules

CORRECTNESS.bend 1 declarations, 1 laws
LAWS.bend 7 declarations, 7 laws
PROOF.bend 4 declarations, 4 laws
buffer.bend 3 declarations
buffer_proof.bend 8 declarations, 6 laws
conformance.bend 76 declarations, 75 laws
core.bend 64 declarations
core_model.bend 100 declarations — Proof-only historical implementation model; not a production dependency.
fips.bend 35 declarations
legacy_model.bend 8 declarations — PROOF-ONLY historical list model. Not imported by the production API.
list_proofs.bend 7 declarations, 7 laws
package.bend 2 declarations — bend-sha256: pure Bend SHA-256 with packed arrays and checked source proofs.
packed.bend 44 declarations
packed_array_proof.bend 6 declarations, 2 laws
packed_proof.bend 49 declarations, 49 laws
packed_spec.bend 20 declarations
padding_proof.bend 1 declarations, 1 laws
sha256.bend 7 declarations
state.bend 2 declarations

Dependencies

No imports from other hub packages.

Dependents

0x74799d3f via src/share/sha.bend: import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as S
0x886223f5 via src/share/sha.bend: import 0x3bdc0c9f5265bb49f7fc76b61f529f24/sha256.bend as S

Status on bend 2.0.36

File	Status	Checker says	Time
CORRECTNESS.bend	checks	ALL PROOFS CHECK	26.4 s
LAWS.bend	open laws/TODOs	7 TODOs found. Checked alone, a law without a def is a TODO; all of them are proved in files that check, so the package counts this file as checks. output SOME PROOFS FAIL Error: 7 TODOs found. The code is incomplete, and not a valid proof yet.	26.9 s
PROOF.bend	checks	ALL PROOFS CHECK	45.1 s
buffer.bend	checks	ALL PROOFS CHECK	1.0 s
buffer_proof.bend	checks	ALL PROOFS CHECK	26.3 s
conformance.bend	checks	ALL PROOFS CHECK	27.1 s
core.bend	checks	ALL PROOFS CHECK	0.7 s
core_model.bend	checks	ALL PROOFS CHECK	1.0 s
fips.bend	checks	ALL PROOFS CHECK	0.6 s
legacy_model.bend	checks	ALL PROOFS CHECK	27.9 s
list_proofs.bend	checks	ALL PROOFS CHECK	0.7 s
package.bend	checks	ALL PROOFS CHECK	56.1 s
packed.bend	checks	ALL PROOFS CHECK	0.6 s
packed_array_proof.bend	checks	ALL PROOFS CHECK	0.5 s
packed_proof.bend	checks	ALL PROOFS CHECK	37.5 s
packed_spec.bend	checks	ALL PROOFS CHECK	0.4 s
padding_proof.bend	checks	ALL PROOFS CHECK	0.8 s
sha256.bend	checks	ALL PROOFS CHECK	0.6 s
state.bend	checks	ALL PROOFS CHECK	0.4 s