Numeric literals sampling

.gitignore

@@ -10,6 +10,7 @@ dist-newstyle
 .ghc.environment.*
 cabal.project.freeze
 cabal.project.local*
+.vscode
 
 # don't check in generated documentation
 #docs/CryptolPrims.pdf

LiteralSampling.md

@@ -0,0 +1,10 @@
+# Literal Sampling
+
+
+
+## TODO
+
+- [x] remove use of vector-sized and related dependencies -- its not worth it now that I have a good idea of what I'm doing
+  - this will require explicit nVars included in some places probably
+- [x] make sure to use the `SamplingM` monad basically everywhere -- so that you can reasonably throw errors without causing a crash
+- [ ] where to call `sample` from, so I know what type exactly it should have?

cryptol.cabal

@@ -78,7 +78,9 @@ library
                        mtl               >= 2.2.1,
                        time              >= 1.6.0.1,
                        panic             >= 0.3,
-                       what4             >= 1.3 && < 1.4
+                       what4             >= 1.3 && < 1.4,
+                       constraints,
+                       vector
 
   if impl(ghc >= 9.0)
     build-depends:     ghc-bignum        >= 1.0 && < 1.3
@@ -176,6 +178,15 @@ library
                        Cryptol.Transform.Specialize,
                        Cryptol.Transform.AddModParams,
 
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Base,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Constraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Exp,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Preconstraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.Sampling,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.SolvedConstraints,
+                       Cryptol.TypeCheck.Solver.Numeric.Sampling.System,
+
                        Cryptol.IR.FreeVars,
 
                        Cryptol.Backend,

docs/RefMan/Properties.rst

@@ -0,0 +1,182 @@
+
+Properties
+==========
+
+A _property_ is a Cryptol value of the form
+
+.. code-block:: cryptol
+
+  {A1, ..., AL} (C1, ..., CM) => T1 -> ... -> TN -> Bit
+
+
+where `L, M, N >= 0`.
+
+The user can annotated a declaration as a property with the `property` keyword,
+like so:
+
+.. code-block:: cryptol
+
+  property reverseInvolution xs = reverse (reverse xs) == xs
+
+There are several REPL commands that interact with declarations annotated as
+properties, such as `:check`, `:prove`, and `:sat`. If the user runs one of
+these commands without any arguments, then all such properties are used,
+sequentially, as an argument.
+
+For example, if the user loads the following module into the REPL,
+
+.. code-block:: cryptol
+
+  module Sort where
+
+  sort : {n} (Ord n) => [n] -> [n]
+  sort xs = ...
+
+  isSorted : {n} (Ord n) => [n] -> Bit
+  isSorted xs = ...
+
+  isPermutation : {n} (Eq n) => [n] -> [n] -> Bit
+  isPermutation xs ys = ...
+
+  property isSorted_sort xs = isSorted (sort xs)
+
+  property isPermutation_sort = isPermutation (sort xs)
+
+then they can run the REPL command
+
+.. code:: sh
+
+  Sort> :check
+
+To use random testing to check whether `isSorted_sort` and `isPermutation_sort`
+hold. In other words, it is the same as running
+
+.. code:: sh
+
+  Sort> :check isSorted_sort
+  Sort> :check isPermutation_sort
+
+
+Testing
+-------
+
+To test a property `prop`, the user enters the following command into the
+Cryptol REPL:
+
+.. code-block::sh
+
+  Cryptol> :check prop
+
+By default, this command performs the following: 
+
+#. Check the type of `prop`. For each type variable of kind `*`, choose a
+   default type that satisfies all its constraints. For the type numeric type
+   variables (of kind `#`), use numeric literal sampling to gather a collection
+   of type assignment, each of which is tested seperately. If numeric literal
+   sampling fails, then try to use a default assignment provided by the SMT
+   solver instead (this is likely to be a trivial solution).
+#. If `prop` is a valid property, compute the size of its input space, otherwise
+   fail. If the size is at most equal to the environment variable `tests`, then
+   use exhaustive checking, otherwise use random testing.
+#. If using exhaustive checking, then evaluate `prop` on every input. If using
+   random testing, evaluate `prop` on randomly sampled inputs.
+
+The REPL command `:exhaust` will test using exhaustive testing.
+
+Numeric Literal Sampling
+^^^^^^^^^^^^^^^^^^^^^^^^
+
+Numeric literal sampling attempts to find a well-distributed sampling of type
+assignments that satisfy a set of numeric type constriants.
+
+The subset of type constraints supported is defined by the following grammar:
+
+.. code
+
+  <cnstr>  ::=  fin <var>  |  <exp> <rel> <exp>
+    <rel>  ::=  =  |  <=
+    <exp>  ::=  <exp> + <exp>  |  <exp> - <exp>  
+             |  <exp> * <con>  |  <exp> / <con>  |  <exp> % <con>
+             |  <con> * <con>  |  <con> / <con>  |  <con> % <con>  |  <con> ^^ <con>
+
+    <var>  ::= <numeric type variable>
+    <con>  ::= <numeric constant>
+
+Note that type constraint synonyms are expanded, e.g. `x <= y` is expanded to `y
+>= x`.
+
+The following is a high-level description of the sampling algorithm:
+
+#. Check that the user's constraints fall into the domain of constraints handled
+   by this algorithm. Relations and operations handled by this algorithm are:
+
+#. Convert the constraints into a system of linear equations and a set of
+   typeclass constraints (such as `fin`).
+  - `e1 <= e2` converts to `e1 + n = e2` where `n` is a fresh numeric type
+    variable.
+  - `... e % n ...` converts to `(... m ..., n*l + m = e)` where `l` and `n` are
+    fresh numeric type variable.
+#. Solve the system using gaussian elimination.
+#. Eliminate the denomenators of coefficients in the system.
+  - If the denomenators of the coefficients of variable `n` have least common
+    multiple `d`, then replace each appearance of `a*n` with `a*d*n'` and
+    introduce a new variable `n'` to the system, and replace the solution for
+    `n` in the system with the equation `n = d*n`. If `n` was not free but was
+    solved for by `n = e`, then add the equation `n' = e/d`.
+  - The denomenators of variables are eliminated in order of dependency, which
+    is guaranteed to be acyclic by gaussian elimination.
+#. Sample values of free variables in the system.
+  - First, collect the upper bounds on variables. 
+    - If a variable is constrained by `fin n`, then the upper bound is the
+      largest finite value to test. 
+    - For an equation such as `n = 1*m + 2*l - 3*k - 4*j + 10`, the following
+      upper bounds are inferred: `m <= inf`, `l <= inf`, `k <= (1*m + 2*l)/3`, `j
+      <= (1*m + 2*l - 3*k + 10)/4`.
+  - Sample each variable: if a variale is upper-bounded by `inf` then sample
+    along an exponential distribution up to the maximum value to test and
+    additionally with some probability `inf`, if a variable is upper-bounded by
+    a finite value `c` then sample uniformly over the interval `[0, c]`.
+
+
+Configuration
+^^^^^^^^^^^^^
+
+The following environment variables configure testing:
+
+- `tests`: the total number of tests to do for a single `:check`
+- `literalSampling`: whether to try to use literal sampling
+- `literalSamplingBinSize`: number of tests to run for each sampling
+
+
+Proving
+-------
+
+The user can try to prove that a property holds by querying an SMT solver with
+the corresponding proposition. To try to prove a property `prop`, the user
+enters the following command into the Cryptol REPL: 
+
+.. code:: sh
+
+  Cryptol> :prove prop
+
+To try to check that `prop` is at least satisfiable, with a similar query to an
+SMT solver, the user enters the following command into the Cryptol REPL:
+
+.. code:: sh
+
+  Cryptol> :sat prop
+
+Alternatively, the user can run 
+
+Configuration
+^^^^^^^^^^^^^
+
+The following environment variables configure testing:
+
+- `prover`: name of SMT solver to use
+- `smtFile`: where to dump SMT output when using an offline solver; set to "-"
+  to ignore
+- `showExamples`: whether or not to print counterexamples
+- `ignoreSafety`: tell the prover to ignore safety
+- `hashConsing`: use hash caching
+- `warnUninterp`: warn when lifting uninterpreted functions

docs/RefMan/RefMan.rst

@@ -12,5 +12,6 @@ Cryptol Reference Manual
   OverloadedOperations
   TypeDeclarations
   Modules
+  Properties
   FFI