bend-collections-laws-crypto@1.0.0.0

0xa7e654f9780078ca65bf9e187da99d3e

Files (405)

laws_crypto.bend
proofs/crypto/aead/chacha20poly1305.bend27 definitions
proofs/crypto/aead/laws.bend22 definitions
proofs/crypto/aead/proof.bend17 definitions
proofs/crypto/aead/sound.bend12 definitions
proofs/crypto/aead/subtle_eq.bend5 definitions
proofs/crypto/aes/aead.bend52 definitions
proofs/crypto/aes/api.bend22 definitions
proofs/crypto/aes/cipher.bend24 definitions
proofs/crypto/aes/gcm.bend14 definitions
proofs/crypto/aes/gf.bend44 definitions
proofs/crypto/aes/ghash.bend10 definitions
proofs/crypto/aes/ghash_bits.bend12 definitions
proofs/crypto/aes/ghash_defs.bend4 definitions
proofs/crypto/aes/inverse.bend3 definitions
proofs/crypto/aes/laws.bend31 definitions
proofs/crypto/aes/proof.bend7 definitions
proofs/crypto/aes/sbox.bend7 definitions
proofs/crypto/argon2/blamka.bend16 definitions
proofs/crypto/argon2/fill.bend42 definitions
proofs/crypto/argon2/gb.bend17 definitions
proofs/crypto/argon2/hash.bend26 definitions
proofs/crypto/argon2/index.bend20 definitions
proofs/crypto/argon2/laws.bend15 definitions
proofs/crypto/argon2/memory.bend62 definitions
proofs/crypto/argon2/password.bend38 definitions
proofs/crypto/argon2/phc.bend45 definitions
proofs/crypto/argon2/proof.bend
proofs/crypto/argon2/run.bend6 definitions
proofs/crypto/argon2/top.bend28 definitions
proofs/crypto/argon2/words.bend8 definitions
proofs/crypto/blake/blake2b/api.bend2 definitions
proofs/crypto/blake/blake2b/array.bend4 definitions
proofs/crypto/blake/blake2b/blocks.bend76 definitions
proofs/crypto/blake/blake2b/compress.bend43 definitions
proofs/crypto/blake/blake2b/laws.bend5 definitions
proofs/crypto/blake/blake2b/proof.bend
proofs/crypto/blake/blake2s/array.bend4 definitions
proofs/crypto/blake/blake2s/bytes.bend13 definitions
proofs/crypto/blake/blake2s/compress.bend37 definitions
proofs/crypto/blake/blake2s/laws.bend4 definitions
proofs/crypto/blake/blake2s/proof.bend
proofs/crypto/blake/blake2s/reads.bend48 definitions
proofs/crypto/blake/blake3/array.bend4 definitions
proofs/crypto/blake/blake3/chunk.bend12 definitions
proofs/crypto/blake/blake3/compress.bend7 definitions
proofs/crypto/blake/blake3/lists.bend17 definitions
proofs/crypto/blake/blake3/loop.bend17 definitions
proofs/crypto/blake/blake3/proof.bend9 definitions
proofs/crypto/blake/blake3/read.bend21 definitions
proofs/crypto/blake/blake3/tree.bend40 definitions
proofs/crypto/blake/proof.bend
proofs/crypto/chacha/core.bend25 definitions
proofs/crypto/chacha/involution.bend13 definitions
proofs/crypto/chacha/laws.bend18 definitions
proofs/crypto/chacha/proof.bend4 definitions
proofs/crypto/chacha/stream.bend19 definitions
proofs/crypto/chacha/xchacha.bend6 definitions
proofs/crypto/curve25519/canon.bend24 definitions
proofs/crypto/curve25519/cong.bend16 definitions
proofs/crypto/curve25519/consts.bend12 definitions
proofs/crypto/curve25519/eqf.bend8 definitions
proofs/crypto/curve25519/fieldops.bend23 definitions
proofs/crypto/curve25519/fold.bend18 definitions
proofs/crypto/curve25519/freeze.bend15 definitions
proofs/crypto/curve25519/ladder.bend15 definitions
proofs/crypto/curve25519/limbs.bend37 definitions
proofs/crypto/curve25519/mulw.bend27 definitions
proofs/crypto/curve25519/num.bend18 definitions
proofs/crypto/curve25519/poly.bend32 definitions
proofs/crypto/curve25519/pow.bend37 definitions
proofs/crypto/curve25519/prime.bend5 definitions
proofs/crypto/curve25519/proof.bend42 definitions
proofs/crypto/curve25519/reduce.bend15 definitions
proofs/crypto/curve25519/rel.bend16 definitions
proofs/crypto/curve25519/xbits.bend22 definitions
proofs/crypto/ed25519/adc.bend8 definitions
proofs/crypto/ed25519/bytes.bend18 definitions
proofs/crypto/ed25519/pcodec.bend33 definitions
proofs/crypto/ed25519/pdec.bend16 definitions
proofs/crypto/ed25519/prel.bend22 definitions
proofs/crypto/ed25519/proof.bend21 definitions
proofs/crypto/ed25519/scalar.bend19 definitions
proofs/crypto/ed25519/scalar2.bend14 definitions
proofs/crypto/ed25519/scalar3.bend19 definitions
proofs/crypto/ed25519/top.bend26 definitions
proofs/crypto/hash/incremental.bend27 definitions
proofs/crypto/hash/laws.bend12 definitions
proofs/crypto/hash/lists.bend7 definitions
proofs/crypto/hash/proof.bend1 definition
proofs/crypto/kdf/laws.bend10 definitions
proofs/crypto/kdf/okm.bend16 definitions
proofs/crypto/kdf/proof.bend9 definitions
proofs/crypto/keccak/api.bend27 definitions
proofs/crypto/keccak/array.bend4 definitions
proofs/crypto/keccak/laws.bend6 definitions
proofs/crypto/keccak/permutation.bend7 definitions
proofs/crypto/keccak/proof.bend
proofs/crypto/keccak/sponge.bend84 definitions
proofs/crypto/mac/hmac.bend12 definitions
proofs/crypto/mac/laws.bend6 definitions
proofs/crypto/mac/proof.bend1 definition
proofs/crypto/poly1305/arith.bend32 definitions
proofs/crypto/poly1305/final.bend48 definitions
proofs/crypto/poly1305/laws.bend9 definitions
proofs/crypto/poly1305/mac.bend24 definitions
proofs/crypto/poly1305/modp.bend9 definitions
proofs/crypto/poly1305/poly.bend8 definitions
proofs/crypto/poly1305/proof.bend5 definitions
proofs/crypto/poly1305/step.bend27 definitions
proofs/crypto/poly1305/value.bend57 definitions
proofs/crypto/random/bytes.bend26 definitions
proofs/crypto/random/proof.bend10 definitions
proofs/crypto/secp256k1/bitsrel.bend12 definitions
proofs/crypto/secp256k1/bitsv.bend17 definitions
proofs/crypto/secp256k1/blist.bend12 definitions
proofs/crypto/secp256k1/bounds.bend9 definitions
proofs/crypto/secp256k1/bytes.bend33 definitions
proofs/crypto/secp256k1/consts.bend36 definitions
proofs/crypto/secp256k1/fieldops.bend33 definitions
proofs/crypto/secp256k1/fieldpow.bend36 definitions
proofs/crypto/secp256k1/fprot.bend22 definitions
proofs/crypto/secp256k1/fwrap.bend11 definitions
proofs/crypto/secp256k1/ineq.bend17 definitions
proofs/crypto/secp256k1/laws.bend3 definitions
proofs/crypto/secp256k1/laws_recover.bend2 definitions
proofs/crypto/secp256k1/laws_schnorr.bend3 definitions
proofs/crypto/secp256k1/laws_sign.bend1 definition
proofs/crypto/secp256k1/laws_verify.bend2 definitions
proofs/crypto/secp256k1/limbs.bend17 definitions
proofs/crypto/secp256k1/listops.bend26 definitions
proofs/crypto/secp256k1/lits.bend6 definitions
proofs/crypto/secp256k1/modexp.bend3 definitions
proofs/crypto/secp256k1/negate.bend16 definitions
proofs/crypto/secp256k1/paff.bend14 definitions
proofs/crypto/secp256k1/pdec.bend14 definitions
proofs/crypto/secp256k1/pecr.bend6 definitions
proofs/crypto/secp256k1/penc.bend22 definitions
proofs/crypto/secp256k1/peth.bend11 definitions
proofs/crypto/secp256k1/pmul.bend12 definitions
proofs/crypto/secp256k1/point.bend35 definitions
proofs/crypto/secp256k1/ppub.bend6 definitions
proofs/crypto/secp256k1/prec.bend27 definitions
proofs/crypto/secp256k1/proof.bend1 definition
proofs/crypto/secp256k1/proof_recover.bend
proofs/crypto/secp256k1/proof_schnorr.bend
proofs/crypto/secp256k1/proof_sign.bend2 definitions
proofs/crypto/secp256k1/proof_verify.bend
proofs/crypto/secp256k1/pscal.bend6 definitions
proofs/crypto/secp256k1/pschn.bend41 definitions
proofs/crypto/secp256k1/psign.bend27 definitions
proofs/crypto/secp256k1/ptwo.bend2 definitions
proofs/crypto/secp256k1/pver.bend9 definitions
proofs/crypto/secp256k1/rconst.bend23 definitions
proofs/crypto/secp256k1/reduce.bend30 definitions
proofs/crypto/secp256k1/reducek.bend19 definitions
proofs/crypto/secp256k1/scalarops.bend29 definitions
proofs/crypto/secp256k1/scalarpow.bend27 definitions
proofs/crypto/secp256k1/sel.bend15 definitions
proofs/crypto/secp256k1/semiring.bend7 definitions
proofs/crypto/secp256k1/u32and.bend5 definitions
proofs/crypto/sha/conformance.bend76 definitions
proofs/crypto/sha/correctness.bend1 definition
proofs/crypto/sha/laws.bend5 definitions
proofs/crypto/sha/list_proofs.bend7 definitions
proofs/crypto/sha/packed/buffer_proof.bend8 definitions
proofs/crypto/sha/packed/conformance.bend76 definitions
proofs/crypto/sha/packed/core_model.bend100 definitions
proofs/crypto/sha/packed/laws.bend7 definitions
proofs/crypto/sha/packed/legacy_model.bend8 definitions
proofs/crypto/sha/packed/packed_array_proof.bend4 definitions
proofs/crypto/sha/packed/packed_proof.bend49 definitions
proofs/crypto/sha/packed/proof.bend1 definition
proofs/crypto/sha/padding.bend1 definition
proofs/crypto/sha/proof.bend4 definitions
proofs/crypto/sha3/conformance.bend8 definitions
proofs/crypto/sha3/laws.bend2 definitions
proofs/crypto/sha3/proof.bend
proofs/crypto/sha512/conformance.bend15 definitions
proofs/crypto/sha512/laws.bend3 definitions
proofs/crypto/sha512/proof.bend
proofs/crypto/sha512/words.bend3 definitions
proofs/crypto/subtle/laws.bend3 definitions
proofs/crypto/subtle/proof.bend4 definitions
proofs/crypto/subtle/word.bend16 definitions
proofs/lib/arith.bend22 definitions
proofs/lib/array.bend38 definitions
proofs/lib/lemmas/proofs/addition.bend9 definitions
proofs/lib/lemmas/proofs/addition_bounds.bend3 definitions
proofs/lib/lemmas/proofs/counter.bend4 definitions
proofs/lib/lemmas/proofs/division_bounds.bend5 definitions
proofs/lib/lemmas/proofs/division_candidate.bend5 definitions
proofs/lib/lemmas/proofs/division_candidate_bound.bend4 definitions
proofs/lib/lemmas/proofs/division_invariant.bend6 definitions
proofs/lib/lemmas/proofs/division_no_overflow.bend11 definitions
proofs/lib/lemmas/proofs/division_quotient.bend12 definitions
proofs/lib/lemmas/proofs/division_remainder.bend4 definitions
proofs/lib/lemmas/proofs/division_shift.bend7 definitions
proofs/lib/lemmas/proofs/division_value.bend10 definitions
proofs/lib/lemmas/proofs/invariants.bend17 definitions
proofs/lib/lemmas/proofs/map_bridge.bend26 definitions
proofs/lib/lemmas/proofs/map_difference_order.bend10 definitions
proofs/lib/lemmas/proofs/map_index.bend9 definitions
proofs/lib/lemmas/proofs/map_insert.bend35 definitions
proofs/lib/lemmas/proofs/map_lookup.bend13 definitions
proofs/lib/lemmas/proofs/map_routing.bend18 definitions
proofs/lib/lemmas/proofs/modular_addition.bend13 definitions
proofs/lib/lemmas/proofs/modular_negation.bend6 definitions
proofs/lib/lemmas/proofs/nat_algebra.bend16 definitions
proofs/lib/lemmas/proofs/native_map.bend49 definitions
proofs/lib/lemmas/proofs/natural_division.bend6 definitions
proofs/lib/lemmas/proofs/natural_products.bend8 definitions
proofs/lib/lemmas/proofs/negation_magnitude.bend5 definitions
proofs/lib/lemmas/proofs/numeric.bend24 definitions
proofs/lib/lemmas/proofs/string_compare.bend21 definitions
proofs/lib/lemmas/proofs/subtraction_bounds.bend7 definitions
proofs/lib/lemmas/proofs/word_addition.bend3 definitions
proofs/lib/lemmas/proofs/word_bounds.bend2 definitions
proofs/lib/lemmas/proofs/word_comparison.bend5 definitions
proofs/lib/lemmas/proofs/word_multiplication.bend9 definitions
proofs/lib/lemmas/proofs/word_shift.bend6 definitions
proofs/lib/lemmas/proofs/word_subtraction.bend5 definitions
proofs/lib/lemmas/proofs/word_value.bend19 definitions
proofs/lib/lemmas/spec/numeric.bend17 definitions
proofs/lib/lemmas/spec/unsigned_division.bend1 definition
proofs/lib/lemmas/src/cache.bend58 definitions
proofs/lib/lemmas/src/time.bend8 definitions
proofs/lib/lemmas/src/wide.bend25 definitions
proofs/lib/lemmas/types/model.bend6 definitions
proofs/lib/list.bend46 definitions
proofs/lib/logic.bend24 definitions
proofs/lib/nat.bend75 definitions
proofs/lib/u32.bend43 definitions
proofs/lib/u32alg.bend36 definitions
proofs/lib/u32div.bend28 definitions
proofs/lib/u32half.bend15 definitions
proofs/lib/word.bend41 definitions
proofs/lib/words32.bend13 definitions
proofs/math/hash/hash.bend8 definitions
proofs/math/natural/arith.bend23 definitions
proofs/math/natural/bits.bend14 definitions
proofs/math/natural/fact.bend28 definitions
proofs/math/natural/gcd.bend17 definitions
proofs/math/natural/inverse.bend25 definitions
proofs/math/natural/lcm.bend22 definitions
proofs/math/natural/lists.bend24 definitions
proofs/math/natural/logs.bend17 definitions
proofs/math/natural/misc.bend14 definitions
proofs/math/natural/modpow.bend8 definitions
proofs/math/natural/proof.bend54 definitions
proofs/math/natural/roots.bend29 definitions
proofs/math/natural/sqrtn.bend13 definitions
proofs/math/pow2/pow2.bend2 definitions
proofs/math/random/below.bend15 definitions
proofs/math/random/bits.bend9 definitions
proofs/math/random/bounded.bend3 definitions
proofs/math/random/chacha8/block.bend5 definitions
proofs/math/random/chacha8/rounds.bend6 definitions
proofs/math/random/chacha8/seed.bend4 definitions
proofs/math/random/chacha8/stream.bend7 definitions
proofs/math/random/lemire.bend57 definitions
proofs/math/random/shuffle.bend18 definitions
proofs/math/random/uint64n.bend41 definitions
proofs/math/typed/f64bits.bend45 definitions
proofs/math/typed/f64bl.bend9 definitions
proofs/math/typed/natcmp.bend21 definitions
proofs/math/typed/natfuel.bend68 definitions
proofs/math/typed/shrn.bend12 definitions
proofs/math/typed/u32.bend23 definitions
proofs/math/typed/u32laws.bend45 definitions
proofs/math/typed/w64add.bend51 definitions
proofs/math/typed/w64clz.bend34 definitions
proofs/math/typed/w64div.bend26 definitions
proofs/math/typed/w64dm.bend30 definitions
proofs/math/typed/w64dmrem.bend10 definitions
proofs/math/typed/w64est.bend26 definitions
proofs/math/typed/w64m128.bend16 definitions
proofs/math/typed/w64mul.bend42 definitions
proofs/math/typed/w64sh.bend47 definitions
proofs/math/typed/w64sqrt.bend36 definitions
proofs/math/typed/width.bend60 definitions
proofs/math/u64/u64.bend31 definitions
proofs/math/u64/u64div.bend39 definitions
spec/crypto/aes/aes.bend43 definitions
spec/crypto/aes/gcm.bend30 definitions
spec/crypto/aes/poly.bend9 definitions
spec/crypto/argon2/argon2.bend62 definitions
spec/crypto/argon2/blamka.bend31 definitions
spec/crypto/blake/blake2b.bend35 definitions
spec/crypto/blake/blake2s.bend35 definitions
spec/crypto/blake/blake3.bend45 definitions
spec/crypto/chacha.bend30 definitions
spec/crypto/chacha20poly1305.bend12 definitions
spec/crypto/curve25519/field.bend33 definitions
spec/crypto/curve25519/x25519.bend22 definitions
spec/crypto/ed25519.bend42 definitions
spec/crypto/hkdf.bend9 definitions
spec/crypto/hmac.bend11 definitions
spec/crypto/keccak/main.bend17 definitions
spec/crypto/keccak/permutation.bend16 definitions
spec/crypto/kex.bend5 definitions
spec/crypto/poly1305.bend19 definitions
spec/crypto/random.bend14 definitions
spec/crypto/secp256k1/curve.bend53 definitions
spec/crypto/secp256k1/ecdsa.bend59 definitions
spec/crypto/secp256k1/field.bend16 definitions
spec/crypto/secp256k1/schnorr.bend32 definitions
spec/crypto/sha.bend35 definitions
spec/crypto/sha/packed.bend20 definitions
spec/crypto/sha3.bend15 definitions
spec/crypto/sha512.bend42 definitions
spec/crypto/sign.bend6 definitions
spec/crypto/subtle.bend1 definition
spec/lib/common.bend21 definitions
spec/lib/numeric.bend15 definitions
spec/math/f64.bend124 definitions
spec/math/generic.bend50 definitions
spec/math/instances.bend17 definitions
spec/math/natural.bend58 definitions
spec/math/random.bend23 definitions
spec/math/random/chacha8rand.bend32 definitions
spec/math/random/pcg.bend6 definitions
spec/math/random/rand.bend12 definitions
spec/math/random/source.bend3 definitions
spec/math/u64.bend9 definitions
spec/math/w64.bend27 definitions
src/containers/hash_table.bend103 definitions
src/crypto/aead.bend10 definitions
src/crypto/aead/chacha20poly1305.bend22 definitions
src/crypto/aes/aes.bend34 definitions
src/crypto/aes/gcm.bend34 definitions
src/crypto/aes/sbox.bend6 definitions
src/crypto/aes/types.bend2 definitions
src/crypto/aesgcm.bend4 definitions
src/crypto/argon2/argon2.bend46 definitions
src/crypto/argon2/blamka.bend34 definitions
src/crypto/argon2/memory.bend9 definitions
src/crypto/argon2/phc.bend61 definitions
src/crypto/argon2/sub.bend13 definitions
src/crypto/argon2/types.bend1 definition
src/crypto/blake/blake2b/blake2b.bend75 definitions
src/crypto/blake/blake2b/compress.bend140 definitions
src/crypto/blake/blake2b/lane.bend6 definitions
src/crypto/blake/blake2b/sized.bend13 definitions
src/crypto/blake/blake2b/types.bend5 definitions
src/crypto/blake/blake2s/blake2s.bend46 definitions
src/crypto/blake/blake2s/compress.bend5 definitions
src/crypto/blake/blake2s/types.bend2 definitions
src/crypto/blake/blake3/blake3.bend40 definitions
src/crypto/blake/blake3/compress.bend11 definitions
src/crypto/blake/blake3/types.bend4 definitions
src/crypto/chacha/chacha20.bend30 definitions
src/crypto/chacha/core.bend9 definitions
src/crypto/curve25519/field.bend44 definitions
src/crypto/curve25519/x25519.bend17 definitions
src/crypto/ed25519/ed25519.bend11 definitions
src/crypto/ed25519/point.bend27 definitions
src/crypto/ed25519/scalar.bend8 definitions
src/crypto/hash.bend78 definitions
src/crypto/kdf.bend7 definitions
src/crypto/keccak/keccak.bend81 definitions
src/crypto/keccak/lane.bend30 definitions
src/crypto/keccak/permutation.bend6 definitions
src/crypto/keccak/types.bend2 definitions
src/crypto/kex.bend9 definitions
src/crypto/mac.bend7 definitions
src/crypto/password.bend16 definitions
src/crypto/poly1305/limbs.bend19 definitions
src/crypto/poly1305/poly1305.bend14 definitions
src/crypto/random.bend19 definitions
src/crypto/secp256k1.bend19 definitions
src/crypto/secp256k1/bytes.bend10 definitions
src/crypto/secp256k1/ecdsa.bend65 definitions
src/crypto/secp256k1/field.bend29 definitions
src/crypto/secp256k1/limbs.bend34 definitions
src/crypto/secp256k1/point.bend43 definitions
src/crypto/secp256k1/scalar.bend26 definitions
src/crypto/secp256k1/schnorr.bend30 definitions
src/crypto/sha/core.bend163 definitions
src/crypto/sha/packed/buffer.bend3 definitions
src/crypto/sha/packed/core.bend63 definitions
src/crypto/sha/packed/packed.bend44 definitions
src/crypto/sha/packed/sha256.bend7 definitions
src/crypto/sha/sha256.bend6 definitions
src/crypto/sha/state.bend1 definition
src/crypto/sha3/core.bend12 definitions
src/crypto/sha3/sha3_256.bend1 definition
src/crypto/sha512/core.bend29 definitions
src/crypto/sha512/sha512.bend5 definitions
src/crypto/sha512/types.bend2 definitions
src/crypto/sign.bend10 definitions
src/crypto/subtle.bend2 definitions
src/math/f64.bend221 definitions
src/math/generic.bend97 definitions
src/math/hash.bend4 definitions
src/math/instances.bend11 definitions
src/math/natural.bend47 definitions
src/math/num.bend3 definitions
src/math/pow2.bend2 definitions
src/math/random/chacha8.bend15 definitions
src/math/random/chacha8/block.bend8 definitions
src/math/random/pcg.bend16 definitions
src/math/random/rand.bend52 definitions
src/math/u64.bend18 definitions
src/math/w64.bend131 definitions