laws.bend

bend-collections-laws@1.0.0.0 · 18 lines · 0 definitions

1import Base
2
3# bend-collections-laws: every proved clause of bend-collections, in one entry.
4#
5# The laws are published in three parts (BendHub caps a package at 16 MiB);
6# importing this file imports all three, which checks every proof root of the
7# library: the containers' SPARK-style contracts, the math contracts, and the
8# crypto and random refinements (each implementation equal to its standard's
9# executable specification, for every input). Import one part, or one
10# package's root inside it, when you need only those laws, e.g.
11#
12#   import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/aead/proof.bend as AeadLaws
13#
14# What is and is not proved is listed in docs/*_CONTRACTS.md.
15
16import bend-collections-laws-containers@1.0.0.0/laws_containers.bend as Containers
17import bend-collections-laws-math@1.0.0.0/laws_math.bend as Math
18import bend-collections-laws-crypto@1.0.0.0/laws_crypto.bend as Crypto