0xe4067e0d fails

0xe4067e0d858024083f36a7abe7281e89

no description

Anonymous package: import it by hash.

Published

2026-09-25

Size

1,549,241 bytes, 69 files

License

MIT (src/crypto/keccak/LICENSE)

Declarations

229 laws (10 proved), 2115 defs, 102 types

Import

import 0xe4067e0d858024083f36a7abe7281e89/main.bend as Main
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/conformance.bend as Conformance
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/correctness.bend as Correctness
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/laws.bend as Laws
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/list_proofs.bend as List_proofs
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/buffer_proof.bend as Buffer_proof
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/conformance.bend as Conformance
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/core_model.bend as Core_model
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/laws.bend as Laws
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/legacy_model.bend as Legacy_model
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/packed_array_proof.bend as Packed_array_proof
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/packed_proof.bend as Packed_proof
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/packed/proof.bend as Proof
import 0xe4067e0d858024083f36a7abe7281e89/proofs/crypto/sha/padding.bend as Padding
import 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha.bend as Sha
import 0xe4067e0d858024083f36a7abe7281e89/spec/crypto/sha/packed.bend as Packed
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/balanced_search_tree.bend as Balanced_search_tree
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/binary_heap.bend as Binary_heap
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/bitlist.bend as Bitlist
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/bitset.bend as Bitset
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/deque.bend as Deque
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/dlist_iterator.bend as Dlist_iterator
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/doubly_linked_list.bend as Doubly_linked_list
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/dynamic_array.bend as Dynamic_array
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/hash_table.bend as Hash_table
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/internal/dlist_storage.bend as Dlist_storage
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/lru.bend as Lru
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/priority_queue.bend as Priority_queue
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/queue.bend as Queue
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/simple_queue.bend as Simple_queue
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/stack.bend as Stack
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/binary_heap.bend as Binary_heap
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/bitlist.bend as Bitlist
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/bitset.bend as Bitset
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/deque.bend as Deque
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/doubly_linked_list.bend as Doubly_linked_list
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/dynamic_array.bend as Dynamic_array
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/internal_dlist.bend as Internal_dlist
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/queue.bend as Queue
import 0xe4067e0d858024083f36a7abe7281e89/src/containers/types/stack.bend as Stack
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2b/blake2b.bend as Blake2b
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2b/compress.bend as Compress
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2b/hex.bend as Hex
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2b/lane.bend as Lane
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2b/types.bend as Types
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2s/blake2s.bend as Blake2s
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2s/compress.bend as Compress
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2s/hex.bend as Hex
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake2s/types.bend as Types
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake3/blake3.bend as Blake3
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake3/compress.bend as Compress
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake3/hex.bend as Hex
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/blake/blake3/types.bend as Types
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/hex.bend as Hex
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/keccak.bend as Keccak
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/lane.bend as Lane
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/permutation.bend as Permutation
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/keccak/types.bend as Types
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/core.bend as Core
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/buffer.bend as Buffer
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/core.bend as Core
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/packed.bend as Packed
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/packed/sha256.bend as Sha256
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/sha256.bend as Sha256
import 0xe4067e0d858024083f36a7abe7281e89/src/crypto/sha/state.bend as State
import 0xe4067e0d858024083f36a7abe7281e89/src/math/hash.bend as Hash
import 0xe4067e0d858024083f36a7abe7281e89/src/math/pow2.bend as Pow2
import 0xe4067e0d858024083f36a7abe7281e89/src/math/u64.bend as U64

Modules

• main.bend 0 declarations
• proofs/crypto/sha/conformance.bend 76 declarations, 75 laws
• proofs/crypto/sha/correctness.bend 1 declarations, 1 laws
• proofs/crypto/sha/laws.bend 5 declarations, 5 laws
• proofs/crypto/sha/list_proofs.bend 7 declarations, 7 laws
• proofs/crypto/sha/packed/buffer_proof.bend 8 declarations, 6 laws
• proofs/crypto/sha/packed/conformance.bend 76 declarations, 75 laws
• proofs/crypto/sha/packed/core_model.bend 100 declarations — Proof-only historical implementation model; not a production dependency.
• proofs/crypto/sha/packed/laws.bend 7 declarations, 7 laws
• proofs/crypto/sha/packed/legacy_model.bend 8 declarations — PROOF-ONLY historical list model. Not imported by the production API.
• proofs/crypto/sha/packed/packed_array_proof.bend 6 declarations, 2 laws
• proofs/crypto/sha/packed/packed_proof.bend 49 declarations, 49 laws
• proofs/crypto/sha/packed/proof.bend 1 declarations, 1 laws
• proofs/crypto/sha/padding.bend 1 declarations, 1 laws
• spec/crypto/sha.bend 35 declarations
• spec/crypto/sha/packed.bend 20 declarations
• src/containers/balanced_search_tree.bend 383 declarations — Generated by tools/generators/tree_map.py; edit algorithm definitions there.
• src/containers/binary_heap.bend 75 declarations
• src/containers/bitlist.bend 52 declarations
• src/containers/bitset.bend 91 declarations
• src/containers/deque.bend 32 declarations
• src/containers/dlist_iterator.bend 56 declarations
• src/containers/doubly_linked_list.bend 63 declarations
• src/containers/dynamic_array.bend 107 declarations
• src/containers/hash_table.bend 120 declarations
• src/containers/internal/dlist_storage.bend 93 declarations
• src/containers/lru.bend 181 declarations
• src/containers/priority_queue.bend 7 declarations
• src/containers/queue.bend 20 declarations
• src/containers/simple_queue.bend 6 declarations
• src/containers/stack.bend 17 declarations
• src/containers/types/binary_heap.bend 14 declarations
• src/containers/types/bitlist.bend 20 declarations
• src/containers/types/bitset.bend 19 declarations
• src/containers/types/deque.bend 16 declarations
• src/containers/types/doubly_linked_list.bend 27 declarations
• src/containers/types/dynamic_array.bend 21 declarations
• src/containers/types/internal_dlist.bend 27 declarations
• src/containers/types/queue.bend 13 declarations
• src/containers/types/stack.bend 13 declarations
• src/crypto/blake/blake2b/blake2b.bend 75 declarations — Generated by tools/generators/blake2b_gen.py; do not edit by hand.
• src/crypto/blake/blake2b/compress.bend 140 declarations — Generated by tools/generators/blake2b_gen.py; do not edit by hand.
• src/crypto/blake/blake2b/hex.bend 7 declarations — Lowercase hex of a 64-byte BLAKE2b digest (sixteen little-endian words).
• src/crypto/blake/blake2b/lane.bend 6 declarations — Generated by tools/generators/blake2b_gen.py; do not edit by hand.
• src/crypto/blake/blake2b/types.bend 10 declarations — Generated by tools/generators/blake2b_gen.py; do not edit by hand.
• src/crypto/blake/blake2s/blake2s.bend 46 declarations — Generated by tools/generators/blake2s_gen.py; do not edit.
• src/crypto/blake/blake2s/compress.bend 5 declarations — Generated by tools/generators/blake2s_gen.py; do not edit.
• src/crypto/blake/blake2s/hex.bend 7 declarations
• src/crypto/blake/blake2s/types.bend 4 declarations
• src/crypto/blake/blake3/blake3.bend 43 declarations
• src/crypto/blake/blake3/compress.bend 11 declarations
• src/crypto/blake/blake3/hex.bend 6 declarations
• src/crypto/blake/blake3/types.bend 8 declarations
• src/crypto/keccak/hex.bend 7 declarations
• src/crypto/keccak/keccak.bend 81 declarations
• src/crypto/keccak/lane.bend 30 declarations
• src/crypto/keccak/permutation.bend 6 declarations
• src/crypto/keccak/types.bend 4 declarations
• src/crypto/sha/core.bend 164 declarations
• src/crypto/sha/packed/buffer.bend 3 declarations
• src/crypto/sha/packed/core.bend 64 declarations
• src/crypto/sha/packed/packed.bend 44 declarations
• src/crypto/sha/packed/sha256.bend 7 declarations
• src/crypto/sha/sha256.bend 6 declarations
• src/crypto/sha/state.bend 2 declarations
• src/math/hash.bend 4 declarations
• src/math/pow2.bend 2 declarations
• src/math/u64.bend 19 declarations

Other files

• src/crypto/keccak/LICENSE 1,067 bytes

Dependencies

No imports from other hub packages.

Dependents

No package in this build imports it.

Status on bend 2.0.36

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
619 |   for +r: Nat
620>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
621 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
619 |   for +r: Nat
620>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
621 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
619 |   for +r: Nat
620>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
621 |

SOME PROOFS FAIL
Error: 5 TODOs found.
The code is incomplete, and not a valid proof yet.

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |

Error:
- expected : a defined name
- observed : Nat.mod.fin
Context:
- x : Nat
- m : Nat
- d : Nat
- e : Nat
- r : Nat
Location: mod_quotient
620 |   for +r: Nat
621>|   {Nat.mod.fin(Nat.divmod.go(x, m, d, r)) == Nat.mod.fin(Nat.divmod.go(x, m, e, r)) : Nat}
    |    ^^^^^^^^^^^
622 |