~/bend-docscommunity

bend-collections-laws-crypto@1.0.0.0 fails

0xa7e654f9780078ca65bf9e187da99d3e

no description

bend-collections-laws-crypto@1.0.0.0 by Giulio2002

Published
2026-09-30
Size
6,166,809 bytes, 407 files
License
MIT (LICENSE)
MIT (src/crypto/keccak/LICENSE)
Declarations
1268 laws (1105 proved), 7502 defs, 111 types

Import

import bend-collections-laws-crypto@1.0.0.0/laws_crypto.bend as Laws_crypto
import 0xa7e654f9780078ca65bf9e187da99d3e/laws_crypto.bend as Laws_crypto
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/chacha20poly1305.bend as Chacha20poly1305
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/chacha20poly1305.bend as Chacha20poly1305
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/sound.bend as Sound
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/sound.bend as Sound
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/subtle_eq.bend as Subtle_eq
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aead/subtle_eq.bend as Subtle_eq
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/aead.bend as Aead
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/aead.bend as Aead
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/api.bend as Api
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/api.bend as Api
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/cipher.bend as Cipher
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/cipher.bend as Cipher
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gcm.bend as Gcm
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/gcm.bend as Gcm
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/gf.bend as Gf
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/gf.bend as Gf
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash.bend as Ghash
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash.bend as Ghash
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_bits.bend as Ghash_bits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_bits.bend as Ghash_bits
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/ghash_defs.bend as Ghash_defs
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/ghash_defs.bend as Ghash_defs
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/inverse.bend as Inverse
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/inverse.bend as Inverse
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aes/sbox.bend as Sbox
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/aes/sbox.bend as Sbox
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/blamka.bend as Blamka
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/blamka.bend as Blamka
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/fill.bend as Fill
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/fill.bend as Fill
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/gb.bend as Gb
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/gb.bend as Gb
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/hash.bend as Hash
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/hash.bend as Hash
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/index.bend as Index
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/index.bend as Index
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/memory.bend as Memory
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/memory.bend as Memory
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/password.bend as Password
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/password.bend as Password
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/phc.bend as Phc
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/phc.bend as Phc
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/run.bend as Run
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/run.bend as Run
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/top.bend as Top
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/top.bend as Top
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/argon2/words.bend as Words
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/argon2/words.bend as Words
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/api.bend as Api
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/api.bend as Api
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/array.bend as MArray
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/array.bend as MArray
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/blocks.bend as Blocks
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/blocks.bend as Blocks
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2b/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2b/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/array.bend as MArray
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/array.bend as MArray
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/bytes.bend as Bytes
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/bytes.bend as Bytes
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake2s/reads.bend as Reads
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake2s/reads.bend as Reads
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/array.bend as MArray
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/array.bend as MArray
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/chunk.bend as Chunk
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/chunk.bend as Chunk
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/lists.bend as Lists
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/lists.bend as Lists
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/loop.bend as Loop
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/loop.bend as Loop
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/read.bend as Read
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/read.bend as Read
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/blake3/tree.bend as Tree
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/blake3/tree.bend as Tree
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/blake/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/blake/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/involution.bend as Involution
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/involution.bend as Involution
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/stream.bend as Stream
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/stream.bend as Stream
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/chacha/xchacha.bend as Xchacha
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/chacha/xchacha.bend as Xchacha
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as Canon
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/canon.bend as Canon
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as Cong
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/cong.bend as Cong
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as Consts
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/consts.bend as Consts
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as Eqf
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/eqf.bend as Eqf
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as Fieldops
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/fieldops.bend as Fieldops
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as Fold
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/fold.bend as Fold
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend as Freeze
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/freeze.bend as Freeze
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as Ladder
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/ladder.bend as Ladder
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.bend as Limbs
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as Mulw
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/mulw.bend as Mulw
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as Num
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/num.bend as Num
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/poly.bend as Poly
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend as Pow
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/pow.bend as Pow
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as Prime
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/prime.bend as Prime
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/reduce.bend as Reduce
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/reduce.bend as Reduce
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as Rel
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/rel.bend as Rel
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as Xbits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/xbits.bend as Xbits
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as Adc
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/adc.bend as Adc
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/bytes.bend as Bytes
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/bytes.bend as Bytes
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pcodec.bend as Pcodec
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as Pdec
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/pdec.bend as Pdec
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend as Prel
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/prel.bend as Prel
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as Scalar
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar.bend as Scalar
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as Scalar2
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar2.bend as Scalar2
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as Scalar3
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/scalar3.bend as Scalar3
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/top.bend as Top
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/ed25519/top.bend as Top
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/incremental.bend as Incremental
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/hash/incremental.bend as Incremental
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/hash/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/lists.bend as Lists
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/hash/lists.bend as Lists
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/hash/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/hash/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/kdf/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/okm.bend as Okm
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/kdf/okm.bend as Okm
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/kdf/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/kdf/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/api.bend as Api
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/api.bend as Api
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/array.bend as MArray
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/array.bend as MArray
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/permutation.bend as Permutation
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/permutation.bend as Permutation
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/keccak/sponge.bend as Sponge
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/keccak/sponge.bend as Sponge
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/hmac.bend as Hmac
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/mac/hmac.bend as Hmac
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/mac/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/mac/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/mac/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as Arith
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/arith.bend as Arith
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/final.bend as Final
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/final.bend as Final
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as Mac
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/mac.bend as Mac
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/modp.bend as Modp
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/modp.bend as Modp
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/poly.bend as Poly
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/poly.bend as Poly
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/step.bend as Step
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.bend as Step
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as Value
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.bend as Value
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/bytes.bend as Bytes
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/random/bytes.bend as Bytes
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/random/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/random/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsrel.bend as Bitsrel
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsrel.bend as Bitsrel
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bitsv.bend as Bitsv
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bitsv.bend as Bitsv
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/blist.bend as Blist
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/blist.bend as Blist
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as Bounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bounds.bend as Bounds
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bytes.bend as Bytes
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/bytes.bend as Bytes
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as Consts
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/consts.bend as Consts
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldops.bend as Fieldops
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/fieldops.bend as Fieldops
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fieldpow.bend as Fieldpow
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/fieldpow.bend as Fieldpow
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fprot.bend as Fprot
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/fprot.bend as Fprot
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/fwrap.bend as Fwrap
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/fwrap.bend as Fwrap
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as Ineq
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/ineq.bend as Ineq
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws_recover.bend as Laws_recover
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/laws_recover.bend as Laws_recover
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws_schnorr.bend as Laws_schnorr
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/laws_schnorr.bend as Laws_schnorr
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws_sign.bend as Laws_sign
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/laws_sign.bend as Laws_sign
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/laws_verify.bend as Laws_verify
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/laws_verify.bend as Laws_verify
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as Limbs
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/limbs.bend as Limbs
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/listops.bend as Listops
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/lits.bend as Lits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/lits.bend as Lits
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/modexp.bend as Modexp
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/modexp.bend as Modexp
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/negate.bend as Negate
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as Paff
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/paff.bend as Paff
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pdec.bend as Pdec
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pdec.bend as Pdec
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pecr.bend as Pecr
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pecr.bend as Pecr
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/penc.bend as Penc
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/penc.bend as Penc
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/peth.bend as Peth
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/peth.bend as Peth
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pmul.bend as Pmul
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pmul.bend as Pmul
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/point.bend as Point
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/point.bend as Point
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ppub.bend as Ppub
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/ppub.bend as Ppub
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/prec.bend as Prec
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/proof_recover.bend as Proof_recover
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/proof_recover.bend as Proof_recover
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/proof_schnorr.bend as Proof_schnorr
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/proof_schnorr.bend as Proof_schnorr
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/proof_sign.bend as Proof_sign
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/proof_sign.bend as Proof_sign
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/proof_verify.bend as Proof_verify
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/proof_verify.bend as Proof_verify
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pscal.bend as Pscal
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pscal.bend as Pscal
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pschn.bend as Pschn
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pschn.bend as Pschn
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/psign.bend as Psign
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/psign.bend as Psign
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ptwo.bend as Ptwo
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/ptwo.bend as Ptwo
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/pver.bend as Pver
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/pver.bend as Pver
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as Rconst
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/rconst.bend as Rconst
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as Reduce
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/reduce.bend as Reduce
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reducek.bend as Reducek
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/reducek.bend as Reducek
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarops.bend as Scalarops
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/scalarops.bend as Scalarops
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/scalarpow.bend as Scalarpow
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/scalarpow.bend as Scalarpow
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as Sel
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/sel.bend as Sel
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as Semiring
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/semiring.bend as Semiring
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/u32and.bend as U32and
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/secp256k1/u32and.bend as U32and
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/conformance.bend as Conformance
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/conformance.bend as Conformance
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/correctness.bend as Correctness
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/correctness.bend as Correctness
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/list_proofs.bend as List_proofs
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/list_proofs.bend as List_proofs
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/buffer_proof.bend as Buffer_proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/buffer_proof.bend as Buffer_proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/conformance.bend as Conformance
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/conformance.bend as Conformance
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/core_model.bend as Core_model
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/core_model.bend as Core_model
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/legacy_model.bend as Legacy_model
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/legacy_model.bend as Legacy_model
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_array_proof.bend as Packed_array_proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/packed_array_proof.bend as Packed_array_proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/packed_proof.bend as Packed_proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/packed_proof.bend as Packed_proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/packed/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/packed/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/padding.bend as Padding
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/padding.bend as Padding
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/conformance.bend as Conformance
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha3/conformance.bend as Conformance
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha3/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha3/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha3/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/conformance.bend as Conformance
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/conformance.bend as Conformance
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/sha512/words.bend as Words
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/sha512/words.bend as Words
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/laws.bend as Laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/subtle/laws.bend as Laws
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/subtle/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/subtle/word.bend as MWord
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/subtle/word.bend as MWord
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as Arith
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/arith.bend as Arith
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/array.bend as MArray
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/array.bend as MArray
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as Addition
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/addition.bend as Addition
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/addition_bounds.bend as Addition_bounds
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/counter.bend as Counter
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/counter.bend as Counter
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_bounds.bend as Division_bounds
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_candidate.bend as Division_candidate
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_candidate_bound.bend as Division_candidate_bound
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_invariant.bend as Division_invariant
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_no_overflow.bend as Division_no_overflow
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_quotient.bend as Division_quotient
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_remainder.bend as Division_remainder
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_shift.bend as Division_shift
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/division_value.bend as Division_value
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/invariants.bend as Invariants
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_bridge.bend as Map_bridge
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_difference_order.bend as Map_difference_order
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_index.bend as Map_index
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_insert.bend as Map_insert
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_lookup.bend as Map_lookup
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/map_routing.bend as Map_routing
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/modular_addition.bend as Modular_addition
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/modular_negation.bend as Modular_negation
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/nat_algebra.bend as Nat_algebra
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/native_map.bend as Native_map
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/natural_division.bend as Natural_division
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/natural_products.bend as Natural_products
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/negation_magnitude.bend as Negation_magnitude
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/numeric.bend as Numeric
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/string_compare.bend as String_compare
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/subtraction_bounds.bend as Subtraction_bounds
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_addition.bend as Word_addition
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_bounds.bend as Word_bounds
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_comparison.bend as Word_comparison
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_multiplication.bend as Word_multiplication
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_shift.bend as Word_shift
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_subtraction.bend as Word_subtraction
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/proofs/word_value.bend as Word_value
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as Numeric
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/numeric.bend as Numeric
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/spec/unsigned_division.bend as Unsigned_division
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/cache.bend as Cache
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/cache.bend as Cache
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/time.bend as Time
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/time.bend as Time
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as Wide
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/src/wide.bend as Wide
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/types/model.bend as Model
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/lemmas/types/model.bend as Model
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/list.bend as MList
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/list.bend as MList
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Logic
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/logic.bend as Logic
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as MNat
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/nat.bend as MNat
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as MU32
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32.bend as MU32
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as U32alg
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32alg.bend as U32alg
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as U32div
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32div.bend as U32div
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32half.bend as U32half
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/u32half.bend as U32half
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as MWord
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.bend as MWord
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/words32.bend as Words32
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/words32.bend as Words32
import bend-collections-laws-crypto@1.0.0.0/proofs/math/hash/hash.bend as Hash
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/hash/hash.bend as Hash
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as Arith
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/arith.bend as Arith
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as Bits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/bits.bend as Bits
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend as Fact
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/fact.bend as Fact
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/gcd.bend as Gcd
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/gcd.bend as Gcd
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/inverse.bend as Inverse
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/inverse.bend as Inverse
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/lcm.bend as Lcm
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend as Lists
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/lists.bend as Lists
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/logs.bend as Logs
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/logs.bend as Logs
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/misc.bend as Misc
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/misc.bend as Misc
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/modpow.bend as Modpow
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/modpow.bend as Modpow
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/proof.bend as Proof
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/proof.bend as Proof
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/roots.bend as Roots
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/roots.bend as Roots
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/sqrtn.bend as Sqrtn
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/natural/sqrtn.bend as Sqrtn
import bend-collections-laws-crypto@1.0.0.0/proofs/math/pow2/pow2.bend as Pow2
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/pow2/pow2.bend as Pow2
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/below.bend as Below
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/below.bend as Below
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bits.bend as Bits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/bits.bend as Bits
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/bounded.bend as Bounded
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/bounded.bend as Bounded
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/block.bend as Block
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/chacha8/block.bend as Block
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/rounds.bend as Rounds
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/chacha8/rounds.bend as Rounds
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/seed.bend as Seed
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/chacha8/seed.bend as Seed
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/chacha8/stream.bend as Stream
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/chacha8/stream.bend as Stream
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as Lemire
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/lemire.bend as Lemire
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/shuffle.bend as Shuffle
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/shuffle.bend as Shuffle
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/random/uint64n.bend as Uint64n
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/f64bits.bend as F64bits
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/f64bl.bend as F64bl
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/f64bl.bend as F64bl
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natcmp.bend as Natcmp
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/natcmp.bend as Natcmp
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/natfuel.bend as Natfuel
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/natfuel.bend as Natfuel
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/shrn.bend as Shrn
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/shrn.bend as Shrn
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32.bend as MU32
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/u32.bend as MU32
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/u32laws.bend as U32laws
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/u32laws.bend as U32laws
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64add.bend as W64add
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64add.bend as W64add
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64clz.bend as W64clz
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64clz.bend as W64clz
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64div.bend as W64div
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64div.bend as W64div
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dm.bend as W64dm
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64dm.bend as W64dm
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64dmrem.bend as W64dmrem
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64dmrem.bend as W64dmrem
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64est.bend as W64est
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64est.bend as W64est
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64m128.bend as W64m128
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64m128.bend as W64m128
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64mul
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64mul.bend as W64mul
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as W64sh
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64sh.bend as W64sh
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64sqrt
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/w64sqrt.bend as W64sqrt
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as Width
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/typed/width.bend as Width
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64.bend as U64
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64.bend as U64
import bend-collections-laws-crypto@1.0.0.0/proofs/math/u64/u64div.bend as U64div
import 0xa7e654f9780078ca65bf9e187da99d3e/proofs/math/u64/u64div.bend as U64div
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/aes.bend as Aes
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/aes.bend as Aes
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/gcm.bend as Gcm
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/gcm.bend as Gcm
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as Poly
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/aes/poly.bend as Poly
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/argon2.bend as Argon2
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/argon2.bend as Argon2
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/argon2/blamka.bend as Blamka
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/argon2/blamka.bend as Blamka
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2b.bend as Blake2b
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2b.bend as Blake2b
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake2s.bend as Blake2s
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake2s.bend as Blake2s
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/blake/blake3.bend as Blake3
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/blake/blake3.bend as Blake3
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha.bend as Chacha
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha.bend as Chacha
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/chacha20poly1305.bend as Chacha20poly1305
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/chacha20poly1305.bend as Chacha20poly1305
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as Field
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.bend as Field
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as X25519
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/x25519.bend as X25519
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as Ed25519
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/ed25519.bend as Ed25519
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hkdf.bend as Hkdf
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hkdf.bend as Hkdf
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/hmac.bend as Hmac
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/hmac.bend as Hmac
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/main.bend as Main
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/main.bend as Main
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/keccak/permutation.bend as Permutation
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/keccak/permutation.bend as Permutation
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/kex.bend as Kex
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/kex.bend as Kex
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as Poly1305
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.bend as Poly1305
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/random.bend as Random
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/random.bend as Random
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as Curve
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/curve.bend as Curve
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as Ecdsa
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/ecdsa.bend as Ecdsa
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as Field
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/field.bend as Field
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/schnorr.bend as Schnorr
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/secp256k1/schnorr.bend as Schnorr
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha.bend as Sha
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha.bend as Sha
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha/packed.bend as Packed
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha/packed.bend as Packed
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha3.bend as Sha3
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha3.bend as Sha3
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sha512.bend as Sha512
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sha512.bend as Sha512
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/sign.bend as Sign
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/sign.bend as Sign
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/subtle.bend as Subtle
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/subtle.bend as Subtle
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as Common
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.bend as Common
import bend-collections-laws-crypto@1.0.0.0/spec/lib/numeric.bend as Numeric
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/numeric.bend as Numeric
import bend-collections-laws-crypto@1.0.0.0/spec/math/f64.bend as F64
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/f64.bend as F64
import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as Generic
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/generic.bend as Generic
import bend-collections-laws-crypto@1.0.0.0/spec/math/instances.bend as Instances
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/instances.bend as Instances
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as Natural
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/natural.bend as Natural
import bend-collections-laws-crypto@1.0.0.0/spec/math/random.bend as Random
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random.bend as Random
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/chacha8rand.bend as Chacha8rand
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/chacha8rand.bend as Chacha8rand
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/pcg.bend as Pcg
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/pcg.bend as Pcg
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend as Rand
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/rand.bend as Rand
import bend-collections-laws-crypto@1.0.0.0/spec/math/random/source.bend as Source
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/random/source.bend as Source
import bend-collections-laws-crypto@1.0.0.0/spec/math/u64.bend as U64
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/u64.bend as U64
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as W64
import 0xa7e654f9780078ca65bf9e187da99d3e/spec/math/w64.bend as W64
import bend-collections-laws-crypto@1.0.0.0/src/containers/hash_table.bend as Hash_table
import 0xa7e654f9780078ca65bf9e187da99d3e/src/containers/hash_table.bend as Hash_table
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead.bend as Aead
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead.bend as Aead
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aead/chacha20poly1305.bend as Chacha20poly1305
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aead/chacha20poly1305.bend as Chacha20poly1305
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/aes.bend as Aes
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/aes.bend as Aes
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/gcm.bend as Gcm
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/gcm.bend as Gcm
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/sbox.bend as Sbox
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/sbox.bend as Sbox
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aes/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aes/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/aesgcm.bend as Aesgcm
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/aesgcm.bend as Aesgcm
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/argon2.bend as Argon2
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/argon2.bend as Argon2
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/blamka.bend as Blamka
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/blamka.bend as Blamka
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/memory.bend as Memory
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/memory.bend as Memory
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/phc.bend as Phc
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/phc.bend as Phc
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/sub.bend as Sub
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/sub.bend as Sub
import bend-collections-laws-crypto@1.0.0.0/src/crypto/argon2/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/argon2/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/blake2b.bend as Blake2b
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/blake2b.bend as Blake2b
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/lane.bend as Lane
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/lane.bend as Lane
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/sized.bend as Sized
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/sized.bend as Sized
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2b/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2b/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/blake2s.bend as Blake2s
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/blake2s.bend as Blake2s
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake2s/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake2s/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/blake3.bend as Blake3
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/blake3.bend as Blake3
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/compress.bend as Compress
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/compress.bend as Compress
import bend-collections-laws-crypto@1.0.0.0/src/crypto/blake/blake3/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/blake/blake3/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/chacha20.bend as Chacha20
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/chacha20.bend as Chacha20
import bend-collections-laws-crypto@1.0.0.0/src/crypto/chacha/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/chacha/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as Field
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.bend as Field
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X25519
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/x25519.bend as X25519
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/ed25519.bend as Ed25519
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/ed25519.bend as Ed25519
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend as Point
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/point.bend as Point
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as Scalar
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/ed25519/scalar.bend as Scalar
import bend-collections-laws-crypto@1.0.0.0/src/crypto/hash.bend as Hash
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/hash.bend as Hash
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kdf.bend as Kdf
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kdf.bend as Kdf
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/keccak.bend as Keccak
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/keccak.bend as Keccak
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/lane.bend as Lane
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/lane.bend as Lane
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/permutation.bend as Permutation
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/permutation.bend as Permutation
import bend-collections-laws-crypto@1.0.0.0/src/crypto/keccak/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/keccak/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/kex.bend as Kex
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/kex.bend as Kex
import bend-collections-laws-crypto@1.0.0.0/src/crypto/mac.bend as Mac
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/mac.bend as Mac
import bend-collections-laws-crypto@1.0.0.0/src/crypto/password.bend as Password
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/password.bend as Password
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Limbs
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.bend as Limbs
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as Poly1305
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.bend as Poly1305
import bend-collections-laws-crypto@1.0.0.0/src/crypto/random.bend as Random
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/random.bend as Random
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1.bend as Secp256k1
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1.bend as Secp256k1
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/bytes.bend as Bytes
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/bytes.bend as Bytes
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as Ecdsa
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/ecdsa.bend as Ecdsa
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/field.bend as Field
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/field.bend as Field
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as Limbs
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/limbs.bend as Limbs
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/point.bend as Point
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/point.bend as Point
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/scalar.bend as Scalar
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/scalar.bend as Scalar
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/schnorr.bend as Schnorr
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/secp256k1/schnorr.bend as Schnorr
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/buffer.bend as Buffer
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/packed/buffer.bend as Buffer
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/packed/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/packed.bend as Packed
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/packed/packed.bend as Packed
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/packed/sha256.bend as Sha256
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/packed/sha256.bend as Sha256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/sha256.bend as Sha256
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/sha256.bend as Sha256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha/state.bend as State
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha/state.bend as State
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha3/sha3_256.bend as Sha3_256
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha3/sha3_256.bend as Sha3_256
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/core.bend as Core
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/core.bend as Core
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/sha512.bend as Sha512
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/sha512.bend as Sha512
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sha512/types.bend as Types
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sha512/types.bend as Types
import bend-collections-laws-crypto@1.0.0.0/src/crypto/sign.bend as Sign
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/sign.bend as Sign
import bend-collections-laws-crypto@1.0.0.0/src/crypto/subtle.bend as Subtle
import 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/subtle.bend as Subtle
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F64
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/f64.bend as F64
import bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend as Generic
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/generic.bend as Generic
import bend-collections-laws-crypto@1.0.0.0/src/math/hash.bend as Hash
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/hash.bend as Hash
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as Instances
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/instances.bend as Instances
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as Natural
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/natural.bend as Natural
import bend-collections-laws-crypto@1.0.0.0/src/math/num.bend as Num
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/num.bend as Num
import bend-collections-laws-crypto@1.0.0.0/src/math/pow2.bend as Pow2
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/pow2.bend as Pow2
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8.bend as Chacha8
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8.bend as Chacha8
import bend-collections-laws-crypto@1.0.0.0/src/math/random/chacha8/block.bend as Block
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/chacha8/block.bend as Block
import bend-collections-laws-crypto@1.0.0.0/src/math/random/pcg.bend as Pcg
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/pcg.bend as Pcg
import bend-collections-laws-crypto@1.0.0.0/src/math/random/rand.bend as Rand
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/random/rand.bend as Rand
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U64
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/u64.bend as U64
import bend-collections-laws-crypto@1.0.0.0/src/math/w64.bend as W64
import 0xa7e654f9780078ca65bf9e187da99d3e/src/math/w64.bend as W64

Modules

Other files

Dependencies

No imports from other hub packages.

Dependents

Status on bend 2.0.36

FileStatusChecker saysTime
laws_crypto.bendfails Error: the machine stack overflowed (a deep recursion, or a literal too large to expand)
output
Error: the machine stack overflowed (a deep recursion, or a literal too large to expand)
10.1 s
proofs/crypto/aead/chacha20poly1305.bendchecks ALL PROOFS CHECK17.1 s
proofs/crypto/aead/laws.bendopen laws/TODOs 20 TODOs found.
output
SOME PROOFS FAIL
Error: 20 TODOs found.
The code is incomplete, and not a valid proof yet.
1.3 s
proofs/crypto/aead/proof.bendchecks ALL PROOFS CHECK41.2 s
proofs/crypto/aead/sound.bendchecks ALL PROOFS CHECK5.1 s
proofs/crypto/aead/subtle_eq.bendchecks ALL PROOFS CHECK0.6 s
proofs/crypto/aes/aead.bendchecks ALL PROOFS CHECK2.5 s
proofs/crypto/aes/api.bendchecks ALL PROOFS CHECK26.4 s
proofs/crypto/aes/cipher.bendchecks ALL PROOFS CHECK24.3 s
proofs/crypto/aes/gcm.bendchecks ALL PROOFS CHECK26.5 s
proofs/crypto/aes/gf.bendchecks ALL PROOFS CHECK0.7 s
proofs/crypto/aes/ghash.bendchecks ALL PROOFS CHECK2.7 s
proofs/crypto/aes/ghash_bits.bendchecks ALL PROOFS CHECK2.2 s
proofs/crypto/aes/ghash_defs.bendchecks ALL PROOFS CHECK0.8 s
proofs/crypto/aes/inverse.bendchecks ALL PROOFS CHECK13.4 s
proofs/crypto/aes/laws.bendopen laws/TODOs 28 TODOs found.
output
SOME PROOFS FAIL
Error: 28 TODOs found.
The code is incomplete, and not a valid proof yet.
0.6 s
proofs/crypto/aes/proof.bendchecks ALL PROOFS CHECK41.9 s
proofs/crypto/aes/sbox.bendchecks ALL PROOFS CHECK26.7 s
proofs/crypto/argon2/blamka.bendchecks ALL PROOFS CHECK5.2 s
proofs/crypto/argon2/fill.bendchecks ALL PROOFS CHECK5.8 s
proofs/crypto/argon2/gb.bendchecks ALL PROOFS CHECK4.6 s
proofs/crypto/argon2/hash.bendchecks ALL PROOFS CHECK4.0 s
proofs/crypto/argon2/index.bendchecks ALL PROOFS CHECK5.6 s
proofs/crypto/argon2/laws.bendopen laws/TODOs 15 TODOs found.
output
SOME PROOFS FAIL
Error: 15 TODOs found.
The code is incomplete, and not a valid proof yet.
5.3 s
proofs/crypto/argon2/memory.bendchecks ALL PROOFS CHECK2.7 s
proofs/crypto/argon2/password.bendchecks ALL PROOFS CHECK6.0 s
proofs/crypto/argon2/phc.bendchecks ALL PROOFS CHECK4.1 s
proofs/crypto/argon2/proof.bendchecks ALL PROOFS CHECK12.4 s
proofs/crypto/argon2/run.bendchecks ALL PROOFS CHECK9.8 s
proofs/crypto/argon2/top.bendchecks ALL PROOFS CHECK10.2 s
proofs/crypto/argon2/words.bendchecks ALL PROOFS CHECK3.9 s
proofs/crypto/blake/blake2b/api.bendchecks ALL PROOFS CHECK1.1 s
proofs/crypto/blake/blake2b/array.bendchecks ALL PROOFS CHECK0.6 s
proofs/crypto/blake/blake2b/blocks.bendchecks ALL PROOFS CHECK5.0 s
proofs/crypto/blake/blake2b/compress.bendchecks ALL PROOFS CHECK3.8 s
proofs/crypto/blake/blake2b/laws.bendopen laws/TODOs 5 TODOs found.
output
SOME PROOFS FAIL
Error: 5 TODOs found.
The code is incomplete, and not a valid proof yet.
1.0 s
proofs/crypto/blake/blake2b/proof.bendchecks ALL PROOFS CHECK4.3 s
proofs/crypto/blake/blake2s/array.bendchecks ALL PROOFS CHECK0.7 s
proofs/crypto/blake/blake2s/bytes.bendchecks ALL PROOFS CHECK1.0 s
proofs/crypto/blake/blake2s/compress.bendchecks ALL PROOFS CHECK1.9 s
proofs/crypto/blake/blake2s/laws.bendopen laws/TODOs 4 TODOs found.
output
SOME PROOFS FAIL
Error: 4 TODOs found.
The code is incomplete, and not a valid proof yet.
0.5 s
proofs/crypto/blake/blake2s/proof.bendchecks ALL PROOFS CHECK3.3 s
proofs/crypto/blake/blake2s/reads.bendchecks ALL PROOFS CHECK3.9 s
proofs/crypto/blake/blake3/array.bendchecks ALL PROOFS CHECK0.6 s
proofs/crypto/blake/blake3/chunk.bendchecks ALL PROOFS CHECK1.2 s
proofs/crypto/blake/blake3/compress.bendchecks ALL PROOFS CHECK1.0 s
proofs/crypto/blake/blake3/lists.bendchecks ALL PROOFS CHECK0.8 s
proofs/crypto/blake/blake3/loop.bendchecks ALL PROOFS CHECK1.6 s
proofs/crypto/blake/blake3/proof.bendchecks ALL PROOFS CHECK1.7 s
proofs/crypto/blake/blake3/read.bendchecks ALL PROOFS CHECK1.0 s
proofs/crypto/blake/blake3/tree.bendchecks ALL PROOFS CHECK1.8 s
proofs/crypto/blake/proof.bendchecks ALL PROOFS CHECK7.9 s
proofs/crypto/chacha/core.bendchecks ALL PROOFS CHECK1.1 s
proofs/crypto/chacha/involution.bendchecks ALL PROOFS CHECK1.8 s
proofs/crypto/chacha/laws.bendopen laws/TODOs 18 TODOs found.
output
SOME PROOFS FAIL
Error: 18 TODOs found.
The code is incomplete, and not a valid proof yet.
0.7 s
proofs/crypto/chacha/proof.bendchecks ALL PROOFS CHECK1.8 s
proofs/crypto/chacha/stream.bendchecks ALL PROOFS CHECK1.3 s
proofs/crypto/chacha/xchacha.bendchecks ALL PROOFS CHECK1.6 s
proofs/crypto/curve25519/canon.bendchecks ALL PROOFS CHECK8.9 s
proofs/crypto/curve25519/cong.bendchecks ALL PROOFS CHECK1.8 s
proofs/crypto/curve25519/consts.bendchecks ALL PROOFS CHECK7.5 s
proofs/crypto/curve25519/eqf.bendchecks ALL PROOFS CHECK8.8 s
proofs/crypto/curve25519/fieldops.bendchecks ALL PROOFS CHECK8.0 s
proofs/crypto/curve25519/fold.bendchecks ALL PROOFS CHECK5.2 s
proofs/crypto/curve25519/freeze.bendchecks ALL PROOFS CHECK9.6 s
proofs/crypto/curve25519/ladder.bendchecks ALL PROOFS CHECK11.6 s
proofs/crypto/curve25519/limbs.bendchecks ALL PROOFS CHECK4.3 s
proofs/crypto/curve25519/mulw.bendchecks ALL PROOFS CHECK8.0 s
proofs/crypto/curve25519/num.bendchecks ALL PROOFS CHECK2.9 s
proofs/crypto/curve25519/poly.bendchecks ALL PROOFS CHECK5.3 s
proofs/crypto/curve25519/pow.bendchecks ALL PROOFS CHECK9.2 s
proofs/crypto/curve25519/prime.bendchecks ALL PROOFS CHECK4.4 s
proofs/crypto/curve25519/proof.bendchecks ALL PROOFS CHECK17.0 s
proofs/crypto/curve25519/reduce.bendchecks ALL PROOFS CHECK5.4 s
proofs/crypto/curve25519/rel.bendchecks ALL PROOFS CHECK9.0 s
proofs/crypto/curve25519/xbits.bendchecks ALL PROOFS CHECK8.9 s
proofs/crypto/ed25519/adc.bendchecks ALL PROOFS CHECK6.3 s
proofs/crypto/ed25519/bytes.bendchecks ALL PROOFS CHECK5.6 s
proofs/crypto/ed25519/pcodec.bendchecks ALL PROOFS CHECK13.5 s
proofs/crypto/ed25519/pdec.bendchecks ALL PROOFS CHECK14.7 s
proofs/crypto/ed25519/prel.bendchecks ALL PROOFS CHECK10.5 s
proofs/crypto/ed25519/proof.bendchecks ALL PROOFS CHECK22.2 s
proofs/crypto/ed25519/scalar.bendchecks ALL PROOFS CHECK9.3 s
proofs/crypto/ed25519/scalar2.bendchecks ALL PROOFS CHECK9.2 s
proofs/crypto/ed25519/scalar3.bendchecks ALL PROOFS CHECK10.8 s
proofs/crypto/ed25519/top.bendchecks ALL PROOFS CHECK18.1 s
proofs/crypto/hash/incremental.bendchecks ALL PROOFS CHECK31.6 s
proofs/crypto/hash/laws.bendopen laws/TODOs 12 TODOs found.
output
SOME PROOFS FAIL
Error: 12 TODOs found.
The code is incomplete, and not a valid proof yet.
1.0 s
proofs/crypto/hash/lists.bendchecks ALL PROOFS CHECK0.5 s
proofs/crypto/hash/proof.bendchecks ALL PROOFS CHECK33.5 s
proofs/crypto/kdf/laws.bendopen laws/TODOs 9 TODOs found.
output
SOME PROOFS FAIL
Error: 9 TODOs found.
The code is incomplete, and not a valid proof yet.
0.9 s
proofs/crypto/kdf/okm.bendchecks ALL PROOFS CHECK26.5 s
proofs/crypto/kdf/proof.bendchecks ALL PROOFS CHECK27.8 s
proofs/crypto/keccak/api.bendchecks ALL PROOFS CHECK0.9 s
proofs/crypto/keccak/array.bendchecks ALL PROOFS CHECK0.5 s
proofs/crypto/keccak/laws.bendopen laws/TODOs 6 TODOs found.
output
SOME PROOFS FAIL
Error: 6 TODOs found.
The code is incomplete, and not a valid proof yet.
0.9 s
proofs/crypto/keccak/permutation.bendchecks ALL PROOFS CHECK1.4 s
proofs/crypto/keccak/proof.bendchecks ALL PROOFS CHECK5.0 s
proofs/crypto/keccak/sponge.bendchecks ALL PROOFS CHECK4.8 s
proofs/crypto/mac/hmac.bendchecks ALL PROOFS CHECK29.4 s
proofs/crypto/mac/laws.bendopen laws/TODOs 6 TODOs found.
output
SOME PROOFS FAIL
Error: 6 TODOs found.
The code is incomplete, and not a valid proof yet.
1.1 s
proofs/crypto/mac/proof.bendchecks ALL PROOFS CHECK28.8 s
proofs/crypto/poly1305/arith.bendchecks ALL PROOFS CHECK6.2 s
proofs/crypto/poly1305/final.bendchecks ALL PROOFS CHECK13.0 s
proofs/crypto/poly1305/laws.bendopen laws/TODOs 9 TODOs found.
output
SOME PROOFS FAIL
Error: 9 TODOs found.
The code is incomplete, and not a valid proof yet.
0.5 s
proofs/crypto/poly1305/mac.bendchecks ALL PROOFS CHECK14.5 s
proofs/crypto/poly1305/modp.bendchecks ALL PROOFS CHECK7.3 s
proofs/crypto/poly1305/poly.bendchecks ALL PROOFS CHECK15.9 s
proofs/crypto/poly1305/proof.bendchecks ALL PROOFS CHECK17.4 s
proofs/crypto/poly1305/step.bendchecks ALL PROOFS CHECK11.9 s
proofs/crypto/poly1305/value.bendchecks ALL PROOFS CHECK7.1 s
proofs/crypto/random/bytes.bendchecks ALL PROOFS CHECK7.1 s
proofs/crypto/random/proof.bendchecks ALL PROOFS CHECK12.4 s
proofs/crypto/secp256k1/bitsrel.bendchecks ALL PROOFS CHECK4.8 s
proofs/crypto/secp256k1/bitsv.bendchecks ALL PROOFS CHECK4.1 s
proofs/crypto/secp256k1/blist.bendchecks ALL PROOFS CHECK4.4 s
proofs/crypto/secp256k1/bounds.bendchecks ALL PROOFS CHECK4.0 s
proofs/crypto/secp256k1/bytes.bendchecks ALL PROOFS CHECK4.5 s
proofs/crypto/secp256k1/consts.bendchecks ALL PROOFS CHECK6.2 s
proofs/crypto/secp256k1/fieldops.bendchecks ALL PROOFS CHECK10.4 s
proofs/crypto/secp256k1/fieldpow.bendchecks ALL PROOFS CHECK13.4 s
proofs/crypto/secp256k1/fprot.bendchecks ALL PROOFS CHECK0.6 s
proofs/crypto/secp256k1/fwrap.bendchecks ALL PROOFS CHECK8.2 s
proofs/crypto/secp256k1/ineq.bendchecks ALL PROOFS CHECK3.2 s
proofs/crypto/secp256k1/laws.bendopen laws/TODOs 3 TODOs found.
output
SOME PROOFS FAIL
Error: 3 TODOs found.
The code is incomplete, and not a valid proof yet.
1.0 s
proofs/crypto/secp256k1/laws_recover.bendopen laws/TODOs 2 TODOs found.
output
SOME PROOFS FAIL
Error: 2 TODOs found.
The code is incomplete, and not a valid proof yet.
1.3 s
proofs/crypto/secp256k1/laws_schnorr.bendopen laws/TODOs 3 TODOs found.
output
SOME PROOFS FAIL
Error: 3 TODOs found.
The code is incomplete, and not a valid proof yet.
1.5 s
proofs/crypto/secp256k1/laws_sign.bendopen laws/TODOs 1 TODO found.
output
SOME PROOFS FAIL
Error: 1 TODO found.
The code is incomplete, and not a valid proof yet.
1.6 s
proofs/crypto/secp256k1/laws_verify.bendopen laws/TODOs 2 TODOs found.
output
SOME PROOFS FAIL
Error: 2 TODOs found.
The code is incomplete, and not a valid proof yet.
1.7 s
proofs/crypto/secp256k1/limbs.bendchecks ALL PROOFS CHECK2.0 s
proofs/crypto/secp256k1/listops.bendchecks ALL PROOFS CHECK5.1 s
proofs/crypto/secp256k1/lits.bendchecks ALL PROOFS CHECK6.7 s
proofs/crypto/secp256k1/modexp.bendchecks ALL PROOFS CHECK1.4 s
proofs/crypto/secp256k1/negate.bendchecks ALL PROOFS CHECK4.4 s
proofs/crypto/secp256k1/paff.bendchecks ALL PROOFS CHECK33.9 s
proofs/crypto/secp256k1/pdec.bendchecks ALL PROOFS CHECK41.2 s
proofs/crypto/secp256k1/pecr.bendchecks ALL PROOFS CHECK70.8 s
proofs/crypto/secp256k1/penc.bendchecks ALL PROOFS CHECK38.2 s
proofs/crypto/secp256k1/peth.bendchecks ALL PROOFS CHECK9.4 s
proofs/crypto/secp256k1/pmul.bendchecks ALL PROOFS CHECK26.2 s
proofs/crypto/secp256k1/point.bendchecks ALL PROOFS CHECK13.8 s
proofs/crypto/secp256k1/ppub.bendchecks ALL PROOFS CHECK50.0 s
proofs/crypto/secp256k1/prec.bendchecks ALL PROOFS CHECK62.8 s
proofs/crypto/secp256k1/proof.bendchecks ALL PROOFS CHECK56.0 s
proofs/crypto/secp256k1/proof_recover.bendchecks ALL PROOFS CHECK66.5 s
proofs/crypto/secp256k1/proof_schnorr.bendtimeout no answer within 180 s180.1 s
proofs/crypto/secp256k1/proof_sign.bendtimeout no answer within 180 s180.1 s
proofs/crypto/secp256k1/proof_verify.bendchecks ALL PROOFS CHECK59.6 s
proofs/crypto/secp256k1/pscal.bendchecks ALL PROOFS CHECK10.6 s
proofs/crypto/secp256k1/pschn.bendtimeout no answer within 180 s180.1 s
proofs/crypto/secp256k1/psign.bendtimeout no answer within 180 s180.1 s
proofs/crypto/secp256k1/ptwo.bendchecks ALL PROOFS CHECK47.3 s
proofs/crypto/secp256k1/pver.bendchecks ALL PROOFS CHECK64.8 s
proofs/crypto/secp256k1/rconst.bendchecks ALL PROOFS CHECK20.6 s
proofs/crypto/secp256k1/reduce.bendchecks ALL PROOFS CHECK3.4 s
proofs/crypto/secp256k1/reducek.bendchecks ALL PROOFS CHECK4.0 s
proofs/crypto/secp256k1/scalarops.bendchecks ALL PROOFS CHECK9.2 s
proofs/crypto/secp256k1/scalarpow.bendchecks ALL PROOFS CHECK14.8 s
proofs/crypto/secp256k1/sel.bendchecks ALL PROOFS CHECK17.5 s
proofs/crypto/secp256k1/semiring.bendchecks ALL PROOFS CHECK1.3 s
proofs/crypto/secp256k1/u32and.bendchecks ALL PROOFS CHECK3.2 s
proofs/crypto/sha/conformance.bendchecks ALL PROOFS CHECK27.3 s
proofs/crypto/sha/correctness.bendchecks ALL PROOFS CHECK26.6 s
proofs/crypto/sha/laws.bendopen laws/TODOs 5 TODOs found.
output
SOME PROOFS FAIL
Error: 5 TODOs found.
The code is incomplete, and not a valid proof yet.
1.1 s
proofs/crypto/sha/list_proofs.bendchecks ALL PROOFS CHECK0.6 s
proofs/crypto/sha/packed/buffer_proof.bendchecks ALL PROOFS CHECK26.8 s
proofs/crypto/sha/packed/conformance.bendchecks ALL PROOFS CHECK24.9 s
proofs/crypto/sha/packed/core_model.bendchecks ALL PROOFS CHECK0.8 s
proofs/crypto/sha/packed/laws.bendopen laws/TODOs 7 TODOs found.
output
SOME PROOFS FAIL
Error: 7 TODOs found.
The code is incomplete, and not a valid proof yet.
25.7 s
proofs/crypto/sha/packed/legacy_model.bendchecks ALL PROOFS CHECK25.9 s
proofs/crypto/sha/packed/packed_array_proof.bendchecks ALL PROOFS CHECK0.5 s
proofs/crypto/sha/packed/packed_proof.bendchecks ALL PROOFS CHECK26.3 s
proofs/crypto/sha/packed/proof.bendchecks ALL PROOFS CHECK26.6 s
proofs/crypto/sha/padding.bendchecks ALL PROOFS CHECK0.8 s
proofs/crypto/sha/proof.bendchecks ALL PROOFS CHECK61.3 s
proofs/crypto/sha3/conformance.bendchecks ALL PROOFS CHECK1.2 s
proofs/crypto/sha3/laws.bendopen laws/TODOs 2 TODOs found.
output
SOME PROOFS FAIL
Error: 2 TODOs found.
The code is incomplete, and not a valid proof yet.
0.8 s
proofs/crypto/sha3/proof.bendchecks ALL PROOFS CHECK1.5 s
proofs/crypto/sha512/conformance.bendchecks ALL PROOFS CHECK1.3 s
proofs/crypto/sha512/laws.bendopen laws/TODOs 3 TODOs found.
output
SOME PROOFS FAIL
Error: 3 TODOs found.
The code is incomplete, and not a valid proof yet.
6.4 s
proofs/crypto/sha512/proof.bendchecks ALL PROOFS CHECK7.2 s
proofs/crypto/sha512/words.bendchecks ALL PROOFS CHECK6.7 s
proofs/crypto/subtle/laws.bendopen laws/TODOs 3 TODOs found.
output
SOME PROOFS FAIL
Error: 3 TODOs found.
The code is incomplete, and not a valid proof yet.
0.4 s
proofs/crypto/subtle/proof.bendchecks ALL PROOFS CHECK0.5 s
proofs/crypto/subtle/word.bendchecks ALL PROOFS CHECK0.5 s
proofs/lib/arith.bendchecks ALL PROOFS CHECK3.2 s
proofs/lib/array.bendchecks ALL PROOFS CHECK3.2 s
proofs/lib/lemmas/proofs/addition.bendchecks ALL PROOFS CHECK1.1 s
proofs/lib/lemmas/proofs/addition_bounds.bendchecks ALL PROOFS CHECK1.1 s
proofs/lib/lemmas/proofs/counter.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/proofs/division_bounds.bendchecks ALL PROOFS CHECK1.4 s
proofs/lib/lemmas/proofs/division_candidate.bendchecks ALL PROOFS CHECK2.4 s
proofs/lib/lemmas/proofs/division_candidate_bound.bendchecks ALL PROOFS CHECK2.4 s
proofs/lib/lemmas/proofs/division_invariant.bendchecks ALL PROOFS CHECK2.5 s
proofs/lib/lemmas/proofs/division_no_overflow.bendchecks ALL PROOFS CHECK2.3 s
proofs/lib/lemmas/proofs/division_quotient.bendchecks ALL PROOFS CHECK2.6 s
proofs/lib/lemmas/proofs/division_remainder.bendchecks ALL PROOFS CHECK2.3 s
proofs/lib/lemmas/proofs/division_shift.bendchecks ALL PROOFS CHECK2.0 s
proofs/lib/lemmas/proofs/division_value.bendchecks ALL PROOFS CHECK2.8 s
proofs/lib/lemmas/proofs/invariants.bendchecks ALL PROOFS CHECK0.7 s
proofs/lib/lemmas/proofs/map_bridge.bendchecks ALL PROOFS CHECK0.7 s
proofs/lib/lemmas/proofs/map_difference_order.bendchecks ALL PROOFS CHECK1.3 s
proofs/lib/lemmas/proofs/map_index.bendchecks ALL PROOFS CHECK1.1 s
proofs/lib/lemmas/proofs/map_insert.bendchecks ALL PROOFS CHECK0.9 s
proofs/lib/lemmas/proofs/map_lookup.bendchecks ALL PROOFS CHECK1.0 s
proofs/lib/lemmas/proofs/map_routing.bendchecks ALL PROOFS CHECK1.4 s
proofs/lib/lemmas/proofs/modular_addition.bendchecks ALL PROOFS CHECK2.3 s
proofs/lib/lemmas/proofs/modular_negation.bendchecks ALL PROOFS CHECK2.3 s
proofs/lib/lemmas/proofs/nat_algebra.bendchecks ALL PROOFS CHECK0.5 s
proofs/lib/lemmas/proofs/native_map.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/proofs/natural_division.bendchecks ALL PROOFS CHECK1.2 s
proofs/lib/lemmas/proofs/natural_products.bendchecks ALL PROOFS CHECK1.5 s
proofs/lib/lemmas/proofs/negation_magnitude.bendchecks ALL PROOFS CHECK2.6 s
proofs/lib/lemmas/proofs/numeric.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/proofs/string_compare.bendchecks ALL PROOFS CHECK0.5 s
proofs/lib/lemmas/proofs/subtraction_bounds.bendchecks ALL PROOFS CHECK2.6 s
proofs/lib/lemmas/proofs/word_addition.bendchecks ALL PROOFS CHECK2.0 s
proofs/lib/lemmas/proofs/word_bounds.bendchecks ALL PROOFS CHECK0.5 s
proofs/lib/lemmas/proofs/word_comparison.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/proofs/word_multiplication.bendchecks ALL PROOFS CHECK1.9 s
proofs/lib/lemmas/proofs/word_shift.bendchecks ALL PROOFS CHECK1.9 s
proofs/lib/lemmas/proofs/word_subtraction.bendchecks ALL PROOFS CHECK2.6 s
proofs/lib/lemmas/proofs/word_value.bendchecks ALL PROOFS CHECK1.1 s
proofs/lib/lemmas/spec/numeric.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/spec/unsigned_division.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/src/cache.bendchecks ALL PROOFS CHECK0.8 s
proofs/lib/lemmas/src/time.bendchecks ALL PROOFS CHECK0.8 s
proofs/lib/lemmas/src/wide.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/lemmas/types/model.bendchecks ALL PROOFS CHECK0.6 s
proofs/lib/list.bendchecks ALL PROOFS CHECK1.2 s
proofs/lib/logic.bendchecks ALL PROOFS CHECK0.7 s
proofs/lib/nat.bendchecks ALL PROOFS CHECK0.9 s
proofs/lib/u32.bendchecks ALL PROOFS CHECK2.9 s
proofs/lib/u32alg.bendchecks ALL PROOFS CHECK3.0 s
proofs/lib/u32div.bendchecks ALL PROOFS CHECK3.5 s
proofs/lib/u32half.bendchecks ALL PROOFS CHECK2.9 s
proofs/lib/word.bendchecks ALL PROOFS CHECK3.6 s
proofs/lib/words32.bendchecks ALL PROOFS CHECK3.4 s
proofs/math/hash/hash.bendchecks ALL PROOFS CHECK3.5 s
proofs/math/natural/arith.bendchecks ALL PROOFS CHECK1.3 s
proofs/math/natural/bits.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/natural/fact.bendchecks ALL PROOFS CHECK1.7 s
proofs/math/natural/gcd.bendchecks ALL PROOFS CHECK1.4 s
proofs/math/natural/inverse.bendchecks ALL PROOFS CHECK1.7 s
proofs/math/natural/lcm.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/natural/lists.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/natural/logs.bendchecks ALL PROOFS CHECK1.9 s
proofs/math/natural/misc.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/natural/modpow.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/natural/proof.bendchecks ALL PROOFS CHECK2.4 s
proofs/math/natural/roots.bendchecks ALL PROOFS CHECK2.0 s
proofs/math/natural/sqrtn.bendchecks ALL PROOFS CHECK2.1 s
proofs/math/pow2/pow2.bendchecks ALL PROOFS CHECK0.7 s
proofs/math/random/below.bendchecks ALL PROOFS CHECK7.4 s
proofs/math/random/bits.bendchecks ALL PROOFS CHECK6.5 s
proofs/math/random/bounded.bendchecks ALL PROOFS CHECK10.1 s
proofs/math/random/chacha8/block.bendchecks ALL PROOFS CHECK3.1 s
proofs/math/random/chacha8/rounds.bendchecks ALL PROOFS CHECK3.1 s
proofs/math/random/chacha8/seed.bendchecks ALL PROOFS CHECK4.6 s
proofs/math/random/chacha8/stream.bendchecks ALL PROOFS CHECK4.0 s
proofs/math/random/lemire.bendchecks ALL PROOFS CHECK4.1 s
proofs/math/random/shuffle.bendchecks ALL PROOFS CHECK2.9 s
proofs/math/random/uint64n.bendchecks ALL PROOFS CHECK11.1 s
proofs/math/typed/f64bits.bendchecks ALL PROOFS CHECK7.0 s
proofs/math/typed/f64bl.bendchecks ALL PROOFS CHECK8.1 s
proofs/math/typed/natcmp.bendchecks ALL PROOFS CHECK6.4 s
proofs/math/typed/natfuel.bendchecks ALL PROOFS CHECK3.8 s
proofs/math/typed/shrn.bendchecks ALL PROOFS CHECK5.0 s
proofs/math/typed/u32.bendchecks ALL PROOFS CHECK3.8 s
proofs/math/typed/u32laws.bendchecks ALL PROOFS CHECK6.2 s
proofs/math/typed/w64add.bendchecks ALL PROOFS CHECK6.7 s
proofs/math/typed/w64clz.bendchecks ALL PROOFS CHECK8.3 s
proofs/math/typed/w64div.bendchecks ALL PROOFS CHECK6.2 s
proofs/math/typed/w64dm.bendchecks ALL PROOFS CHECK7.7 s
proofs/math/typed/w64dmrem.bendchecks ALL PROOFS CHECK8.5 s
proofs/math/typed/w64est.bendchecks ALL PROOFS CHECK8.5 s
proofs/math/typed/w64m128.bendchecks ALL PROOFS CHECK7.0 s
proofs/math/typed/w64mul.bendchecks ALL PROOFS CHECK5.6 s
proofs/math/typed/w64sh.bendchecks ALL PROOFS CHECK7.8 s
proofs/math/typed/w64sqrt.bendchecks ALL PROOFS CHECK5.4 s
proofs/math/typed/width.bendchecks ALL PROOFS CHECK1.6 s
proofs/math/u64/u64.bendchecks ALL PROOFS CHECK3.7 s
proofs/math/u64/u64div.bendchecks ALL PROOFS CHECK5.9 s
spec/crypto/aes/aes.bendchecks ALL PROOFS CHECK0.5 s
spec/crypto/aes/gcm.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/aes/poly.bendchecks ALL PROOFS CHECK0.5 s
spec/crypto/argon2/argon2.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/argon2/blamka.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/blake/blake2b.bendchecks ALL PROOFS CHECK0.6 s
spec/crypto/blake/blake2s.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/blake/blake3.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/chacha.bendchecks ALL PROOFS CHECK0.6 s
spec/crypto/chacha20poly1305.bendchecks ALL PROOFS CHECK1.0 s
spec/crypto/curve25519/field.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/curve25519/x25519.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/ed25519.bendchecks ALL PROOFS CHECK2.2 s
spec/crypto/hkdf.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/hmac.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/keccak/main.bendchecks ALL PROOFS CHECK0.9 s
spec/crypto/keccak/permutation.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/kex.bendchecks ALL PROOFS CHECK1.0 s
spec/crypto/poly1305.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/random.bendchecks ALL PROOFS CHECK1.3 s
spec/crypto/secp256k1/curve.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/secp256k1/ecdsa.bendchecks ALL PROOFS CHECK0.9 s
spec/crypto/secp256k1/field.bendchecks ALL PROOFS CHECK0.7 s
spec/crypto/secp256k1/schnorr.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/sha.bendchecks ALL PROOFS CHECK0.9 s
spec/crypto/sha/packed.bendchecks ALL PROOFS CHECK1.1 s
spec/crypto/sha3.bendchecks ALL PROOFS CHECK0.9 s
spec/crypto/sha512.bendchecks ALL PROOFS CHECK0.8 s
spec/crypto/sign.bendchecks ALL PROOFS CHECK2.3 s
spec/crypto/subtle.bendchecks ALL PROOFS CHECK0.5 s
spec/lib/common.bendchecks ALL PROOFS CHECK0.8 s
spec/lib/numeric.bendchecks ALL PROOFS CHECK0.9 s
spec/math/f64.bendchecks ALL PROOFS CHECK1.2 s
spec/math/generic.bendchecks ALL PROOFS CHECK1.0 s
spec/math/instances.bendchecks ALL PROOFS CHECK0.8 s
spec/math/natural.bendchecks ALL PROOFS CHECK0.9 s
spec/math/random.bendchecks ALL PROOFS CHECK1.2 s
spec/math/random/chacha8rand.bendchecks ALL PROOFS CHECK1.0 s
spec/math/random/pcg.bendchecks ALL PROOFS CHECK0.8 s
spec/math/random/rand.bendchecks ALL PROOFS CHECK1.0 s
spec/math/random/source.bendchecks ALL PROOFS CHECK0.7 s
spec/math/u64.bendchecks ALL PROOFS CHECK0.8 s
spec/math/w64.bendchecks ALL PROOFS CHECK1.0 s
src/containers/hash_table.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/aead.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/aead/chacha20poly1305.bendchecks ALL PROOFS CHECK1.2 s
src/crypto/aes/aes.bendchecks ALL PROOFS CHECK1.2 s
src/crypto/aes/gcm.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/aes/sbox.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/aes/types.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/aesgcm.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/argon2/argon2.bendchecks ALL PROOFS CHECK1.6 s
src/crypto/argon2/blamka.bendchecks ALL PROOFS CHECK1.1 s
src/crypto/argon2/memory.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/argon2/phc.bendchecks ALL PROOFS CHECK0.6 s
src/crypto/argon2/sub.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/argon2/types.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/blake/blake2b/blake2b.bendchecks ALL PROOFS CHECK1.2 s
src/crypto/blake/blake2b/compress.bendchecks ALL PROOFS CHECK1.2 s
src/crypto/blake/blake2b/lane.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/blake/blake2b/sized.bendchecks ALL PROOFS CHECK1.2 s
src/crypto/blake/blake2b/types.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/blake/blake2s/blake2s.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/blake/blake2s/compress.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/blake/blake2s/types.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/blake/blake3/blake3.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/blake/blake3/compress.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/blake/blake3/types.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/chacha/chacha20.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/chacha/core.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/curve25519/field.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/curve25519/x25519.bendchecks ALL PROOFS CHECK0.6 s
src/crypto/ed25519/ed25519.bendchecks ALL PROOFS CHECK2.2 s
src/crypto/ed25519/point.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/ed25519/scalar.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/hash.bendchecks ALL PROOFS CHECK1.9 s
src/crypto/kdf.bendchecks ALL PROOFS CHECK1.3 s
src/crypto/keccak/keccak.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/keccak/lane.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/keccak/permutation.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/keccak/types.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/kex.bendchecks ALL PROOFS CHECK1.1 s
src/crypto/mac.bendchecks ALL PROOFS CHECK1.5 s
src/crypto/password.bendchecks ALL PROOFS CHECK1.6 s
src/crypto/poly1305/limbs.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/poly1305/poly1305.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/random.bendchecks ALL PROOFS CHECK1.1 s
src/crypto/secp256k1.bendchecks ALL PROOFS CHECK2.1 s
src/crypto/secp256k1/bytes.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/secp256k1/ecdsa.bendchecks ALL PROOFS CHECK1.9 s
src/crypto/secp256k1/field.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/secp256k1/limbs.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/secp256k1/point.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/secp256k1/scalar.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/secp256k1/schnorr.bendchecks ALL PROOFS CHECK1.7 s
src/crypto/sha/core.bendchecks ALL PROOFS CHECK1.5 s
src/crypto/sha/packed/buffer.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/sha/packed/core.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/sha/packed/packed.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/sha/packed/sha256.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/sha/sha256.bendchecks ALL PROOFS CHECK1.8 s
src/crypto/sha/state.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/sha3/core.bendchecks ALL PROOFS CHECK0.9 s
src/crypto/sha3/sha3_256.bendchecks ALL PROOFS CHECK1.0 s
src/crypto/sha512/core.bendchecks ALL PROOFS CHECK0.7 s
src/crypto/sha512/sha512.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/sha512/types.bendchecks ALL PROOFS CHECK0.8 s
src/crypto/sign.bendchecks ALL PROOFS CHECK2.2 s
src/crypto/subtle.bendchecks ALL PROOFS CHECK0.8 s
src/math/f64.bendchecks ALL PROOFS CHECK1.3 s
src/math/generic.bendchecks ALL PROOFS CHECK1.0 s
src/math/hash.bendchecks ALL PROOFS CHECK0.8 s
src/math/instances.bendchecks ALL PROOFS CHECK0.9 s
src/math/natural.bendchecks ALL PROOFS CHECK0.7 s
src/math/num.bendchecks ALL PROOFS CHECK0.7 s
src/math/pow2.bendchecks ALL PROOFS CHECK0.9 s
src/math/random/chacha8.bendchecks ALL PROOFS CHECK0.9 s
src/math/random/chacha8/block.bendchecks ALL PROOFS CHECK0.8 s
src/math/random/pcg.bendchecks ALL PROOFS CHECK0.9 s
src/math/random/rand.bendchecks ALL PROOFS CHECK0.8 s
src/math/u64.bendchecks ALL PROOFS CHECK1.0 s
src/math/w64.bendchecks ALL PROOFS CHECK1.0 s