Merge branch 'master' into ffi-integer

This commit is contained in:
Iavor Diatchki 2022-09-22 16:18:36 +03:00
commit 12f2bb086e
144 changed files with 21265 additions and 869 deletions

4
.gitignore vendored
View File

@ -10,6 +10,7 @@ dist-newstyle
.ghc.environment.*
cabal.project.freeze
cabal.project.local*
.vscode/
# don't check in generated documentation
#docs/CryptolPrims.pdf
@ -38,3 +39,6 @@ allfiles.wxs
cryptol.msi
cryptol.wixobj
cryptol.wixpdb
# happy-generated files
src/Cryptol/Parser.hs

View File

@ -2,6 +2,11 @@
## Language changes
* Declarations may now use *numeric constraint guards*. This is a feature
that allows a function to behave differently depending on its numeric
type parameters. See the [manual section](https://galoisinc.github.io/cryptol/RefMan/_build/html/BasicSyntax.html#numeric-constraint-guards))
for more information.
* The foreign function interface (FFI) has been added, which allows Cryptol to
call functions written in C. See the [manual section](https://galoisinc.github.io/cryptol/RefMan/_build/html/FFI.html)
for more information.
@ -23,6 +28,9 @@
* Fix a bug in the What4 backend that could cause applications of `(@)` with
symbolic `Integer` indices to become out of bounds (#1359).
* Fix a bug that caused finite bitvector enumerations to panic when used in
combination with `(#)` (e.g., `[0..1] # 0`).
# 2.13.0
## Language changes

55
ConditionalConstraints.md Normal file
View File

@ -0,0 +1,55 @@
# Conditional Constraints
## Syntax
The front-end AST has a new constructor:
```hs
data BindDef name = DPropGuards [([Prop name], Expr name)] | ...
```
which is parsed from the following syntax:
```
<name> : <signature>
<name> <pats>
[ | <props> => <expr> ]
```
## Expanding PropGuards
- Before renaming, a `Bind` with a `bDef = DPropGuards ...` will be expanded into several `Bind`s, one for each guard case.
- The generated `Bind`s will have fresh names, but the names will have the same location as the original function's name.
- These generated `Bind`'s will have the same type as the original function, except that the list of type constraints will also include the `Prop name`s that appeared on the LHS of the originating ase of `DPropGuards`.
- The original function will have the `Expr name` in each of the `DPropGuards` cases replaced with a function call the appropriate, generated function.
## Renaming
The new constructor of `BindDef` is traversed as normal during renaming. This ensures that a function with `DPropGuards` ends up in the same mutual-recursion group as the generated functions that it calls.
## Typechecking
The back-end AST has a new constructor:
```hs
data Expr = EPropGuards [([Prop], Expr)] | ...
```
During typechecking, a `BindDef` of the form
```
DPropGuards [(props1, f1 x y), (prop2, f2 x y)]
```
is processed into a `Decl` of the form
```
Decl
{ dDefinition =
DExpr (EPropGuards
[ (props1, f1 x y)
, (props2, f2 x y) ])
}
```
Each case of an `EPropGuards` is typechecked by first asssuming the `props` and then typechecking the expression. However, this typechecking isn't really that important because by construction the expression is just a simple application that is ensured to be well-typed. But we can use this structure for more general purposes.

View File

@ -79,6 +79,11 @@ cryptolError modErr warns =
(20710, [ ("source", jsonPretty src)
, ("errors", jsonList (map jsonPretty errs))
])
ExpandPropGuardsError src err ->
(20711, [ ("source", jsonPretty src)
, ("errors", jsonPretty err)
])
NoIncludeErrors src errs ->
-- TODO: structured error here
(20720, [ ("source", jsonPretty src)

View File

@ -62,11 +62,14 @@ library
ghc-prim,
GraphSCC >= 1.0.4,
heredoc >= 0.2,
language-c99,
language-c99-simple,
libBF >= 0.6 && < 0.7,
MemoTrie >= 0.6 && < 0.7,
monad-control >= 1.0,
monadLib >= 3.7.2,
parameterized-utils >= 2.0.2,
pretty,
prettyprinter >= 1.7.0,
process >= 1.2,
sbv >= 8.10 && < 9.1,
@ -105,6 +108,7 @@ library
Cryptol.Parser.Names,
Cryptol.Parser.Name,
Cryptol.Parser.NoPat,
Cryptol.Parser.ExpandPropGuards,
Cryptol.Parser.NoInclude,
Cryptol.Parser.Selector,
Cryptol.Parser.Utils,
@ -199,6 +203,7 @@ library
Cryptol.Eval.Concrete,
Cryptol.Eval.Env,
Cryptol.Eval.FFI,
Cryptol.Eval.FFI.GenHeader,
Cryptol.Eval.Generic,
Cryptol.Eval.Prims,
Cryptol.Eval.Reference,

View File

@ -19,6 +19,54 @@ Type Signatures
f,g : {a,b} (fin a) => [a] b
Numeric Constraint Guards
-------------------------
A declaration with a signature can use *numeric constraint guards*,
which are used to change the behavior of a functoin depending on its
numeric type parameters. For example:
.. code-block:: cryptol
len : {n} (fin n) => [n]a -> Integer
len xs | n == 0 => 0
| n > 0 => 1 + len (drop `{1} xs)
Each behavior starts with ``|`` and lists some constraints on the numeric
parameters to a declaration. When applied, the function will use the first
definition that satisfies the provided numeric parameters.
Numeric constraint guards are quite similar to an ``if`` expression,
except that decisions are based on *types* rather than values. There
is also an important difference to simply using demotion and an
actual ``if`` statement:
.. code-block:: cryptol
len' : {n} (fin n) => [n]a -> Integer
len' xs = if `n == 0 => 0
| `n > 0 => 1 + len (drop `{1} xs)
The definition of ``len'`` is rejected, because the *value based* ``if``
expression does provide the *type based* fact ``n >= 1`` which is
required by ``drop `{1} xs``, while in ``len``, the type-checker
locally-assumes the constraint ``n > 0`` in that constraint-guarded branch
and so it can in fact determine that ``n >= 1``.
Requirements:
- Numeric constraint guards only support constraints over numeric literals,
such as ``fin``, ``<=``, ``==``, etc.
Type constraint aliases can also be used as long as they only constrain
numeric literals.
- The numeric constraint guards of a declaration should be exhaustive. The
type-checker will attempt to prove that the set of constraint guards is
exhaustive, but if it can't then it will issue a non-exhaustive constraint
guards warning. This warning is controlled by the environmental option
``warnNonExhaustiveConstraintGuards``.
- Each constraint guard is checked *independently* of the others, and there
are no implict assumptions that the previous behaviors do not match---
instead the programmer needs to specify all constraints explicitly
in the guard.
Layout
------

View File

@ -13,7 +13,19 @@ systems (macOS and Linux).
Basic usage
-----------
Suppose we want to call the following C function:
Suppose we want to implement the following function in C:
.. code-block:: cryptol
add : [32] -> [32] -> [32]
In our Cryptol file, we declare it as a ``foreign`` function with no body:
.. code-block:: cryptol
foreign add : [32] -> [32] -> [32]
Then we write the following C function:
.. code-block:: c
@ -21,11 +33,16 @@ Suppose we want to call the following C function:
return x + y;
}
In our Cryptol file, we write a ``foreign`` declaration with no body:
Cryptol can generate a C header file containing the appropriate function
prototypes given the corresponding Cryptol ``foreign`` declarations with the
``:generate-foreign-header`` command. You can then ``#include`` the generated
header file in your C file to help write the C implementation.
.. code-block:: cryptol
.. code-block::
foreign add : [32] -> [32] -> [32]
Cryptol> :generate-foreign-header Example.cry
Loading module Example
Writing header to Example.h
The C code must first be compiled into a dynamically loaded shared library. When
Cryptol loads the module containing the ``foreign`` declaration, it will look
@ -61,9 +78,9 @@ The whole process would look something like this:
Note: Since Cryptol currently only accesses the compiled binary and not the C
source, it has no way of checking that the Cryptol function type you declare in
your Cryptol code actually matches the type of the C function. **It is your
responsibility to make sure the types match up**. If they do not then there may
be undefined behavior.
your Cryptol code actually matches the type of the C function. It can generate
the correct C headers but if the actual implementation does not match it there
may be undefined behavior.
Compiling C code
----------------
@ -81,6 +98,10 @@ This section describes how a given Cryptol function signature maps to a C
function prototype. The FFI only supports a limited set of Cryptol types which
have a clear translation into C.
This mapping can now be done automatically with the ``:generate-foreign-header``
command mentioned above; however, this section is still worth reading to
understand the supported types and what the resulting C parameters mean.
Overall structure
~~~~~~~~~~~~~~~~~
@ -305,5 +326,5 @@ corresponds to the C signature
.. code-block:: c
void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
double *out0, uint32_t *out1);
void f(size_t n, uint16_t *in0, uint8_t in1_a, uint64_t in1_b,
double *out_0, uint32_t *out_1);

View File

@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 12febdda05646d6655d93ce350355f10
config: 41758cdb8fafe65367e2aa727ac7d826
tags: 645f666f9bcd5a90fca523b33c5a78b7

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -43,6 +42,7 @@
<li class="toctree-l1 current"><a class="current reference internal" href="#">Basic Syntax</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#declarations">Declarations</a></li>
<li class="toctree-l2"><a class="reference internal" href="#type-signatures">Type Signatures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#numeric-constraint-guards">Numeric Constraint Guards</a></li>
<li class="toctree-l2"><a class="reference internal" href="#layout">Layout</a></li>
<li class="toctree-l2"><a class="reference internal" href="#comments">Comments</a></li>
<li class="toctree-l2"><a class="reference internal" href="#identifiers">Identifiers</a></li>
@ -84,21 +84,67 @@
<div itemprop="articleBody">
<section id="basic-syntax">
<h1>Basic Syntax<a class="headerlink" href="#basic-syntax" title="Permalink to this heading"></a></h1>
<h1>Basic Syntax<a class="headerlink" href="#basic-syntax" title="Permalink to this headline"></a></h1>
<section id="declarations">
<h2>Declarations<a class="headerlink" href="#declarations" title="Permalink to this heading"></a></h2>
<h2>Declarations<a class="headerlink" href="#declarations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">z</span><span class="w"></span>
</pre></div>
</div>
</section>
<section id="type-signatures">
<h2>Type Signatures<a class="headerlink" href="#type-signatures" title="Permalink to this heading"></a></h2>
<h2>Type Signatures<a class="headerlink" href="#type-signatures" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="p">,</span><span class="n">g</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">,</span><span class="n">b</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="w"> </span><span class="n">b</span><span class="w"></span>
</pre></div>
</div>
</section>
<section id="numeric-constraint-guards">
<h2>Numeric Constraint Guards<a class="headerlink" href="#numeric-constraint-guards" title="Permalink to this headline"></a></h2>
<p>A declaration with a signature can use <em>numeric constraint guards</em>,
which are used to change the behavior of a functoin depending on its
numeric type parameters. For example:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
<span class="nf">len</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
</pre></div>
</div>
<p>Each behavior starts with <code class="docutils literal notranslate"><span class="pre">|</span></code> and lists some constraints on the numeric
parameters to a declaration. When applied, the function will use the first
definition that satisfies the provided numeric parameters.</p>
<p>Numeric constraint guards are quite similar to an <code class="docutils literal notranslate"><span class="pre">if</span></code> expression,
except that decisions are based on <em>types</em> rather than values. There
is also an important difference to simply using demotion and an
actual <code class="docutils literal notranslate"><span class="pre">if</span></code> statement:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">len&#39;</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">]</span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
<span class="nf">len&#39;</span><span class="w"> </span><span class="n">xs</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kr">if</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="mi">0</span><span class="w"></span>
<span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="p">`</span><span class="n">n</span><span class="w"> </span><span class="o">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">len</span><span class="w"> </span><span class="p">(</span><span class="n">drop</span><span class="w"> </span><span class="p">`{</span><span class="mi">1</span><span class="p">}</span><span class="w"> </span><span class="n">xs</span><span class="p">)</span><span class="w"></span>
</pre></div>
</div>
<p>The definition of <code class="docutils literal notranslate"><span class="pre">len'</span></code> is rejected, because the <em>value based</em> <code class="docutils literal notranslate"><span class="pre">if</span></code>
expression does provide the <em>type based</em> fact <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&gt;=</span> <span class="pre">1</span></code> which is
required by <code class="docutils literal notranslate"><span class="pre">drop</span> <span class="pre">`{1}</span> <span class="pre">xs</span></code>, while in <code class="docutils literal notranslate"><span class="pre">len</span></code>, the type-checker
locally-assumes the constraint <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&gt;</span> <span class="pre">0</span></code> in that constraint-guarded branch
and so it can in fact determine that <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">&gt;=</span> <span class="pre">1</span></code>.</p>
<dl class="simple">
<dt>Requirements:</dt><dd><ul class="simple">
<li><p>Numeric constraint guards only support constraints over numeric literals,
such as <code class="docutils literal notranslate"><span class="pre">fin</span></code>, <code class="docutils literal notranslate"><span class="pre">&lt;=</span></code>, <code class="docutils literal notranslate"><span class="pre">==</span></code>, etc.
Type constraint aliases can also be used as long as they only constrain
numeric literals.</p></li>
<li><p>The numeric constraint guards of a declaration should be exhaustive. The
type-checker will attempt to prove that the set of constraint guards is
exhaustive, but if it cant then it will issue a non-exhaustive constraint
guards warning. This warning is controlled by the environmental option
<code class="docutils literal notranslate"><span class="pre">warnNonExhaustiveConstraintGuards</span></code>.</p></li>
<li><p>Each constraint guard is checked <em>independently</em> of the others, and there
are no implict assumptions that the previous behaviors do not match—
instead the programmer needs to specify all constraints explicitly
in the guard.</p></li>
</ul>
</dd>
</dl>
</section>
<section id="layout">
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this heading"></a></h2>
<h2>Layout<a class="headerlink" href="#layout" title="Permalink to this headline"></a></h2>
<p>Groups of declarations are organized based on indentation.
Declarations with the same indentation belong to the same group.
Lines of text that are indented more than the beginning of a
@ -119,7 +165,7 @@ lines between <cite>f</cite> and <cite>g</cite> that are indented more than <cit
of <cite>f</cite>, which defines two more local names, <cite>y</cite> and <cite>z</cite>.</p>
</section>
<section id="comments">
<h2>Comments<a class="headerlink" href="#comments" title="Permalink to this heading"></a></h2>
<h2>Comments<a class="headerlink" href="#comments" title="Permalink to this headline"></a></h2>
<p>Cryptol supports block comments, which start with <code class="docutils literal notranslate"><span class="pre">/*</span></code> and end with
<code class="docutils literal notranslate"><span class="pre">*/</span></code>, and line comments, which start with <code class="docutils literal notranslate"><span class="pre">//</span></code> and terminate at the
end of the line. Block comments may be nested arbitrarily.</p>
@ -134,7 +180,7 @@ end of the line. Block comments may be nested arbitrarily.</p>
</div>
</section>
<section id="identifiers">
<h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to this heading"></a></h2>
<h2>Identifiers<a class="headerlink" href="#identifiers" title="Permalink to this headline"></a></h2>
<p>Cryptol identifiers consist of one or more characters. The first
character must be either an English letter or underscore (<code class="docutils literal notranslate"><span class="pre">_</span></code>). The
following characters may be an English letter, a decimal digit,
@ -150,7 +196,7 @@ names (see <a class="reference internal" href="#keywords-and-built-in-operators"
</div>
</section>
<section id="keywords-and-built-in-operators">
<h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-built-in-operators" title="Permalink to this heading"></a></h2>
<h2>Keywords and Built-in Operators<a class="headerlink" href="#keywords-and-built-in-operators" title="Permalink to this headline"></a></h2>
<p>The following identifiers have special meanings in Cryptol, and may
not be used for programmer defined names:</p>
<div class="literal-block-wrapper docutils container" id="id3">
@ -227,7 +273,7 @@ precedence last.</p>
</table>
</section>
<section id="built-in-type-level-operators">
<h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-level-operators" title="Permalink to this heading"></a></h2>
<h2>Built-in Type-level Operators<a class="headerlink" href="#built-in-type-level-operators" title="Permalink to this headline"></a></h2>
<p>Cryptol includes a variety of operators that allow computations on
the numeric types used to specify the sizes of sequences.</p>
<table class="docutils align-default" id="id5">
@ -282,7 +328,7 @@ the numeric types used to specify the sizes of sequences.</p>
</table>
</section>
<section id="numeric-literals">
<h2>Numeric Literals<a class="headerlink" href="#numeric-literals" title="Permalink to this heading"></a></h2>
<h2>Numeric Literals<a class="headerlink" href="#numeric-literals" title="Permalink to this headline"></a></h2>
<p>Numeric literals may be written in binary, octal, decimal, or
hexadecimal notation. The base of a literal is determined by its prefix:
<code class="docutils literal notranslate"><span class="pre">0b</span></code> for binary, <code class="docutils literal notranslate"><span class="pre">0o</span></code> for octal, no special prefix for

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -83,9 +82,9 @@
<div itemprop="articleBody">
<section id="basic-types">
<h1>Basic Types<a class="headerlink" href="#basic-types" title="Permalink to this heading"></a></h1>
<h1>Basic Types<a class="headerlink" href="#basic-types" title="Permalink to this headline"></a></h1>
<section id="tuples-and-records">
<h2>Tuples and Records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h2>
<h2>Tuples and Records<a class="headerlink" href="#tuples-and-records" title="Permalink to this headline"></a></h2>
<p>Tuples and records are used for packaging multiple values together.
Tuples are enclosed in parentheses, while records are enclosed in
curly braces. The components of both tuples and records are separated by
@ -114,7 +113,7 @@ Examples:</p>
components are compared in the order they appear, whereas record
fields are compared in alphabetical order of field names.</p>
<section id="accessing-fields">
<h3>Accessing Fields<a class="headerlink" href="#accessing-fields" title="Permalink to this heading"></a></h3>
<h3>Accessing Fields<a class="headerlink" href="#accessing-fields" title="Permalink to this headline"></a></h3>
<p>The components of a record or a tuple may be accessed in two ways: via
pattern matching or by using explicit component selectors. Explicit
component selectors are written as follows:</p>
@ -165,7 +164,7 @@ entry in the tuple.</p>
<p>This behavior is quite handy when examining complex data at the REPL.</p>
</section>
<section id="updating-fields">
<h3>Updating Fields<a class="headerlink" href="#updating-fields" title="Permalink to this heading"></a></h3>
<h3>Updating Fields<a class="headerlink" href="#updating-fields" title="Permalink to this headline"></a></h3>
<p>The components of a record or a tuple may be updated using the following
notation:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="c1">// Example values</span><span class="w"></span>
@ -188,7 +187,7 @@ notation:</p>
</section>
</section>
<section id="sequences">
<h2>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h2>
<h2>Sequences<a class="headerlink" href="#sequences" title="Permalink to this headline"></a></h2>
<p>A sequence is a fixed-length collection of elements of the same type.
The type of a finite sequence of length <cite>n</cite>, with elements of type <cite>a</cite>
is <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">a</span></code>. Often, a finite sequence of bits, <code class="docutils literal notranslate"><span class="pre">[n]</span> <span class="pre">Bit</span></code>, is called a
@ -267,7 +266,7 @@ a location
</div>
</section>
<section id="functions">
<h2>Functions<a class="headerlink" href="#functions" title="Permalink to this heading"></a></h2>
<h2>Functions<a class="headerlink" href="#functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">\</span><span class="n">p1</span><span class="w"> </span><span class="n">p2</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="c1">// Lambda expression</span><span class="w"></span>
<span class="nf">f</span><span class="w"> </span><span class="n">p1</span><span class="w"> </span><span class="n">p2</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="c1">// Function definition</span><span class="w"></span>
</pre></div>

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -85,10 +84,10 @@
<div itemprop="articleBody">
<section id="expressions">
<h1>Expressions<a class="headerlink" href="#expressions" title="Permalink to this heading"></a></h1>
<h1>Expressions<a class="headerlink" href="#expressions" title="Permalink to this headline"></a></h1>
<p>This section provides an overview of the Cryptols expression syntax.</p>
<section id="calling-functions">
<h2>Calling Functions<a class="headerlink" href="#calling-functions" title="Permalink to this heading"></a></h2>
<h2>Calling Functions<a class="headerlink" href="#calling-functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="c1">// call `f` with parameter `2`</span><span class="w"></span>
<span class="nf">g</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="c1">// call `g` with two parameters: `x` and `y`</span><span class="w"></span>
<span class="nf">h</span><span class="w"> </span><span class="p">(</span><span class="n">x</span><span class="p">,</span><span class="n">y</span><span class="p">)</span><span class="w"> </span><span class="c1">// call `h` with one parameter, the pair `(x,y)`</span><span class="w"></span>
@ -96,7 +95,7 @@
</div>
</section>
<section id="prefix-operators">
<h2>Prefix Operators<a class="headerlink" href="#prefix-operators" title="Permalink to this heading"></a></h2>
<h2>Prefix Operators<a class="headerlink" href="#prefix-operators" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="o">-</span><span class="mi">2</span><span class="w"> </span><span class="c1">// call unary `-` with parameter `2`</span><span class="w"></span>
<span class="o">-</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="c1">// call unary `-` with parameter `2`</span><span class="w"></span>
<span class="nf">f</span><span class="w"> </span><span class="p">(</span><span class="o">-</span><span class="mi">2</span><span class="p">)</span><span class="w"> </span><span class="c1">// call `f` with one argument: `-2`, parens are important</span><span class="w"></span>
@ -106,7 +105,7 @@
</div>
</section>
<section id="infix-functions">
<h2>Infix Functions<a class="headerlink" href="#infix-functions" title="Permalink to this heading"></a></h2>
<h2>Infix Functions<a class="headerlink" href="#infix-functions" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3`</span><span class="w"></span>
<span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="o">*</span><span class="w"> </span><span class="mi">5</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3 * 5`</span><span class="w"></span>
<span class="p">(</span><span class="o">+</span><span class="p">)</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="c1">// call `+` with two parameters: `2` and `3`</span><span class="w"></span>
@ -117,7 +116,7 @@
</div>
</section>
<section id="type-annotations">
<h2>Type Annotations<a class="headerlink" href="#type-annotations" title="Permalink to this heading"></a></h2>
<h2>Type Annotations<a class="headerlink" href="#type-annotations" title="Permalink to this headline"></a></h2>
<p>Explicit type annotations may be added on expressions, patterns, and
in argument definitions.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kr">Bit</span><span class="w"> </span><span class="c1">// specify that `x` has type `Bit`</span><span class="w"></span>
@ -139,7 +138,7 @@ in argument definitions.</p>
</div>
</section>
<section id="explicit-type-instantiation">
<h2>Explicit Type Instantiation<a class="headerlink" href="#explicit-type-instantiation" title="Permalink to this heading"></a></h2>
<h2>Explicit Type Instantiation<a class="headerlink" href="#explicit-type-instantiation" title="Permalink to this headline"></a></h2>
<p>If <code class="docutils literal notranslate"><span class="pre">f</span></code> is a polymorphic value with type:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="n">tyParam</span><span class="w"> </span><span class="p">}</span><span class="w"> </span><span class="n">tyParam</span><span class="w"></span>
<span class="nf">f</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="n">zero</span><span class="w"></span>
@ -151,7 +150,7 @@ in argument definitions.</p>
</div>
</section>
<section id="local-declarations">
<h2>Local Declarations<a class="headerlink" href="#local-declarations" title="Permalink to this heading"></a></h2>
<h2>Local Declarations<a class="headerlink" href="#local-declarations" title="Permalink to this headline"></a></h2>
<p>Local declarations have the weakest precedence of all expressions.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="mi">2</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="kt">T</span><span class="p">]</span><span class="w"></span>
<span class="w"> </span><span class="kr">where</span><span class="w"></span>
@ -167,7 +166,7 @@ in argument definitions.</p>
</div>
</section>
<section id="block-arguments">
<h2>Block Arguments<a class="headerlink" href="#block-arguments" title="Permalink to this heading"></a></h2>
<h2>Block Arguments<a class="headerlink" href="#block-arguments" title="Permalink to this headline"></a></h2>
<p>When used as the last argument to a function call,
<code class="docutils literal notranslate"><span class="pre">if</span></code> and lambda expressions do not need parens:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">f</span><span class="w"> </span><span class="nf">\</span><span class="n">x</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="c1">// call `f` with one argument `x -&gt; x`</span><span class="w"></span>
@ -178,7 +177,7 @@ in argument definitions.</p>
</div>
</section>
<section id="conditionals">
<h2>Conditionals<a class="headerlink" href="#conditionals" title="Permalink to this heading"></a></h2>
<h2>Conditionals<a class="headerlink" href="#conditionals" title="Permalink to this headline"></a></h2>
<p>The <code class="docutils literal notranslate"><span class="pre">if</span> <span class="pre">...</span> <span class="pre">then</span> <span class="pre">...</span> <span class="pre">else</span></code> construct can be used with
multiple branches. For example:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">x</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="kr">if</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">%</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">==</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="kr">then</span><span class="w"> </span><span class="mi">22</span><span class="w"> </span><span class="kr">else</span><span class="w"> </span><span class="mi">33</span><span class="w"></span>
@ -191,7 +190,7 @@ multiple branches. For example:</p>
</div>
</section>
<section id="demoting-numeric-types-to-values">
<h2>Demoting Numeric Types to Values<a class="headerlink" href="#demoting-numeric-types-to-values" title="Permalink to this heading"></a></h2>
<h2>Demoting Numeric Types to Values<a class="headerlink" href="#demoting-numeric-types-to-values" title="Permalink to this headline"></a></h2>
<p>The value corresponding to a numeric type may be accessed using the
following notation:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="p">`</span><span class="n">t</span><span class="w"></span>

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -94,24 +93,37 @@
<div itemprop="articleBody">
<section id="foreign-function-interface">
<h1>Foreign Function Interface<a class="headerlink" href="#foreign-function-interface" title="Permalink to this heading"></a></h1>
<h1>Foreign Function Interface<a class="headerlink" href="#foreign-function-interface" title="Permalink to this headline"></a></h1>
<p>The foreign function interface (FFI) allows Cryptol to call functions written in
C (or other languages that use the C calling convention).</p>
<section id="platform-support">
<h2>Platform support<a class="headerlink" href="#platform-support" title="Permalink to this heading"></a></h2>
<h2>Platform support<a class="headerlink" href="#platform-support" title="Permalink to this headline"></a></h2>
<p>The FFI is currently <strong>not supported on Windows</strong>, and only works on Unix-like
systems (macOS and Linux).</p>
</section>
<section id="basic-usage">
<h2>Basic usage<a class="headerlink" href="#basic-usage" title="Permalink to this heading"></a></h2>
<p>Suppose we want to call the following C function:</p>
<h2>Basic usage<a class="headerlink" href="#basic-usage" title="Permalink to this headline"></a></h2>
<p>Suppose we want to implement the following function in C:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">add</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"></span>
</pre></div>
</div>
<p>In our Cryptol file, we declare it as a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> function with no body:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"></span>
</pre></div>
</div>
<p>Then we write the following C function:</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">uint32_t</span><span class="w"> </span><span class="nf">add</span><span class="p">(</span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">x</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="n">y</span><span class="p">)</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w"> </span><span class="k">return</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="n">y</span><span class="p">;</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>
</div>
<p>In our Cryptol file, we write a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration with no body:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">add</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">[</span><span class="mi">32</span><span class="p">]</span><span class="w"></span>
<p>Cryptol can generate a C header file containing the appropriate function
prototypes given the corresponding Cryptol <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declarations with the
<code class="docutils literal notranslate"><span class="pre">:generate-foreign-header</span></code> command. You can then <code class="docutils literal notranslate"><span class="pre">#include</span></code> the generated
header file in your C file to help write the C implementation.</p>
<div class="highlight-default notranslate"><div class="highlight"><pre><span></span><span class="n">Cryptol</span><span class="o">&gt;</span> <span class="p">:</span><span class="n">generate</span><span class="o">-</span><span class="n">foreign</span><span class="o">-</span><span class="n">header</span> <span class="n">Example</span><span class="o">.</span><span class="n">cry</span>
<span class="n">Loading</span> <span class="n">module</span> <span class="n">Example</span>
<span class="n">Writing</span> <span class="n">header</span> <span class="n">to</span> <span class="n">Example</span><span class="o">.</span><span class="n">h</span>
</pre></div>
</div>
<p>The C code must first be compiled into a dynamically loaded shared library. When
@ -144,12 +156,12 @@ Main&gt; add 1 2
</div>
<p>Note: Since Cryptol currently only accesses the compiled binary and not the C
source, it has no way of checking that the Cryptol function type you declare in
your Cryptol code actually matches the type of the C function. <strong>It is your
responsibility to make sure the types match up</strong>. If they do not then there may
be undefined behavior.</p>
your Cryptol code actually matches the type of the C function. It can generate
the correct C headers but if the actual implementation does not match it there
may be undefined behavior.</p>
</section>
<section id="compiling-c-code">
<h2>Compiling C code<a class="headerlink" href="#compiling-c-code" title="Permalink to this heading"></a></h2>
<h2>Compiling C code<a class="headerlink" href="#compiling-c-code" title="Permalink to this headline"></a></h2>
<p>Cryptol currently does not handle compilation of C code to shared libraries. For
simple usages, you can do this manually with the following commands:</p>
<ul class="simple">
@ -158,12 +170,15 @@ simple usages, you can do this manually with the following commands:</p>
</ul>
</section>
<section id="converting-between-cryptol-and-c-types">
<h2>Converting between Cryptol and C types<a class="headerlink" href="#converting-between-cryptol-and-c-types" title="Permalink to this heading"></a></h2>
<h2>Converting between Cryptol and C types<a class="headerlink" href="#converting-between-cryptol-and-c-types" title="Permalink to this headline"></a></h2>
<p>This section describes how a given Cryptol function signature maps to a C
function prototype. The FFI only supports a limited set of Cryptol types which
have a clear translation into C.</p>
<p>This mapping can now be done automatically with the <code class="docutils literal notranslate"><span class="pre">:generate-foreign-header</span></code>
command mentioned above; however, this section is still worth reading to
understand the supported types and what the resulting C parameters mean.</p>
<section id="overall-structure">
<h3>Overall structure<a class="headerlink" href="#overall-structure" title="Permalink to this heading"></a></h3>
<h3>Overall structure<a class="headerlink" href="#overall-structure" title="Permalink to this headline"></a></h3>
<p>Cryptol <code class="docutils literal notranslate"><span class="pre">foreign</span></code> bindings must be functions. These functions may have
multiple (curried) arguments; they may also be polymorphic, with certain
limitations. That is, the general structure of a <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declaration would
@ -190,7 +205,7 @@ Cryptol arguments.</p>
corresponds to.</p>
</section>
<section id="type-parameters">
<h3>Type parameters<a class="headerlink" href="#type-parameters" title="Permalink to this heading"></a></h3>
<h3>Type parameters<a class="headerlink" href="#type-parameters" title="Permalink to this headline"></a></h3>
<table class="docutils align-default">
<colgroup>
<col style="width: 55%" />
@ -217,7 +232,7 @@ satisfy <code class="docutils literal notranslate"><span class="pre">&lt;</span>
cumbersome.)</p>
</section>
<section id="bit">
<h3>Bit<a class="headerlink" href="#bit" title="Permalink to this heading"></a></h3>
<h3>Bit<a class="headerlink" href="#bit" title="Permalink to this headline"></a></h3>
<table class="docutils align-default">
<colgroup>
<col style="width: 52%" />
@ -239,7 +254,7 @@ When converting to Cryptol, any nonzero number is converted to <code class="docu
<code class="docutils literal notranslate"><span class="pre">0</span></code> is converted to <code class="docutils literal notranslate"><span class="pre">False</span></code>.</p>
</section>
<section id="integral-types">
<h3>Integral types<a class="headerlink" href="#integral-types" title="Permalink to this heading"></a></h3>
<h3>Integral types<a class="headerlink" href="#integral-types" title="Permalink to this headline"></a></h3>
<p>Let <code class="docutils literal notranslate"><span class="pre">K</span> <span class="pre">:</span> <span class="pre">#</span></code> be a Cryptol type. Note <code class="docutils literal notranslate"><span class="pre">K</span></code> must be an actual fixed numeric type
and not a type variable.</p>
<table class="docutils align-default">
@ -278,7 +293,7 @@ words first in Cryptol, then use the FFI conversion for sequences of words to
handle it in C as an array.</p>
</section>
<section id="floating-point-types">
<h3>Floating point types<a class="headerlink" href="#floating-point-types" title="Permalink to this heading"></a></h3>
<h3>Floating point types<a class="headerlink" href="#floating-point-types" title="Permalink to this headline"></a></h3>
<table class="docutils align-default">
<colgroup>
<col style="width: 55%" />
@ -302,7 +317,7 @@ handle it in C as an array.</p>
Other sizes of floating points are not supported.</p>
</section>
<section id="sequences">
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this heading"></a></h3>
<h3>Sequences<a class="headerlink" href="#sequences" title="Permalink to this headline"></a></h3>
<p>Let <code class="docutils literal notranslate"><span class="pre">n1,</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">nk</span> <span class="pre">:</span> <span class="pre">#</span></code> be Cryptol types (with <code class="docutils literal notranslate"><span class="pre">k</span> <span class="pre">&gt;=</span> <span class="pre">1</span></code>), possibly
containing type variables, that satisfy <code class="docutils literal notranslate"><span class="pre">fin</span> <span class="pre">n1,</span> <span class="pre">fin</span> <span class="pre">n2,</span> <span class="pre">...,</span> <span class="pre">fin</span> <span class="pre">nk</span></code>, and
<code class="docutils literal notranslate"><span class="pre">T</span></code> be one of the above Cryptol <em>integral types</em> or <em>floating point types</em>.
@ -331,7 +346,7 @@ along with the pointer, any type arguments contained in the size are passed as C
<code class="docutils literal notranslate"><span class="pre">size_t</span></code>s earlier, so the C code can always know the dimensions of the array.</p>
</section>
<section id="tuples-and-records">
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this heading"></a></h3>
<h3>Tuples and records<a class="headerlink" href="#tuples-and-records" title="Permalink to this headline"></a></h3>
<p>Let <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> be Cryptol types supported by the FFI (which may be any
of the types mentioned above, or tuples and records themselves). Let
<code class="docutils literal notranslate"><span class="pre">U1,</span> <span class="pre">U2,</span> <span class="pre">...,</span> <span class="pre">Un</span></code> be the C types that <code class="docutils literal notranslate"><span class="pre">T1,</span> <span class="pre">T2,</span> <span class="pre">...,</span> <span class="pre">Tn</span></code> respectively
@ -361,12 +376,12 @@ flattening is applied recursively for nested tuples and records. Note that this
means empty tuples dont map to any C values at all.</p>
</section>
<section id="type-synonyms">
<h3>Type synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this heading"></a></h3>
<h3>Type synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this headline"></a></h3>
<p>All type synonyms are expanded before applying the above rules, so you can use
type synonyms in <code class="docutils literal notranslate"><span class="pre">foreign</span></code> declarations to improve readability.</p>
</section>
<section id="return-values">
<h3>Return values<a class="headerlink" href="#return-values" title="Permalink to this heading"></a></h3>
<h3>Return values<a class="headerlink" href="#return-values" title="Permalink to this headline"></a></h3>
<p>If the Cryptol return type is <code class="docutils literal notranslate"><span class="pre">Bit</span></code> or one of the above <em>integral types</em> or
<em>floating point types</em>, the value is returned directly from the C function. In
that case, the return type of the C function will be the C type corresponding to
@ -379,7 +394,7 @@ a pointer <code class="docutils literal notranslate"><span class="pre">U*</span>
input versions are the same type, because it is already a pointer.</p>
</section>
<section id="quick-reference">
<h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalink to this heading"></a></h3>
<h3>Quick reference<a class="headerlink" href="#quick-reference" title="Permalink to this headline"></a></h3>
<table class="docutils align-default">
<colgroup>
<col style="width: 37%" />
@ -457,7 +472,7 @@ input versions are the same type, because it is already a pointer.</p>
</section>
</section>
<section id="memory">
<h2>Memory<a class="headerlink" href="#memory" title="Permalink to this heading"></a></h2>
<h2>Memory<a class="headerlink" href="#memory" title="Permalink to this headline"></a></h2>
<p>When pointers are involved, namely in the cases of sequences and output
arguments, they point to memory. This memory is always allocated and deallocated
by Cryptol; the C code does not need to manage this memory.</p>
@ -471,19 +486,19 @@ memory may be uninitialized when passed to C, and the C code should not read
from it. It must write to the memory the value it is returning.</p>
</section>
<section id="evaluation">
<h2>Evaluation<a class="headerlink" href="#evaluation" title="Permalink to this heading"></a></h2>
<h2>Evaluation<a class="headerlink" href="#evaluation" title="Permalink to this headline"></a></h2>
<p>All Cryptol arguments are fully evaluated when a foreign function is called.</p>
</section>
<section id="example">
<h2>Example<a class="headerlink" href="#example" title="Permalink to this heading"></a></h2>
<h2>Example<a class="headerlink" href="#example" title="Permalink to this headline"></a></h2>
<p>The Cryptol signature</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">foreign</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">n</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">fin</span><span class="w"> </span><span class="n">n</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="p">][</span><span class="mi">10</span><span class="p">]</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="kr">Bit</span><span class="p">,</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="mi">64</span><span class="p">]}</span><span class="w"></span>
<span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="p">(</span><span class="kt">Float64</span><span class="p">,</span><span class="w"> </span><span class="p">[</span><span class="n">n</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="mi">1</span><span class="p">][</span><span class="mi">20</span><span class="p">])</span><span class="w"></span>
</pre></div>
</div>
<p>corresponds to the C signature</p>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">void</span><span class="w"> </span><span class="nf">f</span><span class="p">(</span><span class="kt">size_t</span><span class="w"> </span><span class="n">n</span><span class="p">,</span><span class="w"> </span><span class="kt">uint16_t</span><span class="w"> </span><span class="o">*</span><span class="n">in0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="n">in1</span><span class="p">,</span><span class="w"> </span><span class="kt">uint64_t</span><span class="w"> </span><span class="n">in2</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">double</span><span class="w"> </span><span class="o">*</span><span class="n">out0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="o">*</span><span class="n">out1</span><span class="p">);</span><span class="w"></span>
<div class="highlight-c notranslate"><div class="highlight"><pre><span></span><span class="kt">void</span><span class="w"> </span><span class="nf">f</span><span class="p">(</span><span class="kt">size_t</span><span class="w"> </span><span class="n">n</span><span class="p">,</span><span class="w"> </span><span class="kt">uint16_t</span><span class="w"> </span><span class="o">*</span><span class="n">in0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint8_t</span><span class="w"> </span><span class="n">in1_a</span><span class="p">,</span><span class="w"> </span><span class="kt">uint64_t</span><span class="w"> </span><span class="n">in1_b</span><span class="p">,</span><span class="w"></span>
<span class="w"> </span><span class="kt">double</span><span class="w"> </span><span class="o">*</span><span class="n">out_0</span><span class="p">,</span><span class="w"> </span><span class="kt">uint32_t</span><span class="w"> </span><span class="o">*</span><span class="n">out_1</span><span class="p">);</span><span class="w"></span>
</pre></div>
</div>
</section>

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -100,7 +99,7 @@
<div itemprop="articleBody">
<section id="modules">
<h1>Modules<a class="headerlink" href="#modules" title="Permalink to this heading"></a></h1>
<h1>Modules<a class="headerlink" href="#modules" title="Permalink to this headline"></a></h1>
<p>A <em>module</em> is used to group some related definitions. Each file may
contain at most one top-level module.</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">module</span><span class="w"> </span><span class="nn">M</span><span class="w"> </span><span class="kr">where</span><span class="w"></span>
@ -112,7 +111,7 @@ contain at most one top-level module.</p>
</pre></div>
</div>
<section id="hierarchical-module-names">
<h2>Hierarchical Module Names<a class="headerlink" href="#hierarchical-module-names" title="Permalink to this heading"></a></h2>
<h2>Hierarchical Module Names<a class="headerlink" href="#hierarchical-module-names" title="Permalink to this headline"></a></h2>
<p>Module may have either simple or <em>hierarchical</em> names.
Hierarchical names are constructed by gluing together ordinary
identifiers using the symbol <code class="docutils literal notranslate"><span class="pre">::</span></code>.</p>
@ -129,7 +128,7 @@ will look for a file named <code class="docutils literal notranslate"><span clas
<code class="docutils literal notranslate"><span class="pre">Hash</span></code>, contained in one of the directories specified by <code class="docutils literal notranslate"><span class="pre">CRYPTOLPATH</span></code>.</p>
</section>
<section id="module-imports">
<h2>Module Imports<a class="headerlink" href="#module-imports" title="Permalink to this heading"></a></h2>
<h2>Module Imports<a class="headerlink" href="#module-imports" title="Permalink to this headline"></a></h2>
<p>To use the definitions from one module in another module, we use
<code class="docutils literal notranslate"><span class="pre">import</span></code> declarations:</p>
<div class="literal-block-wrapper docutils container" id="id1">
@ -154,7 +153,7 @@ will look for a file named <code class="docutils literal notranslate"><span clas
</div>
</div>
<section id="import-lists">
<h3>Import Lists<a class="headerlink" href="#import-lists" title="Permalink to this heading"></a></h3>
<h3>Import Lists<a class="headerlink" href="#import-lists" title="Permalink to this headline"></a></h3>
<p>Sometimes, we may want to import only some of the definitions
from a module. To do so, we use an import declaration with
an <em>import list</em>.</p>
@ -177,7 +176,7 @@ It also tends to make code easier to understand, because
it makes it easy to see the source of definitions.</p>
</section>
<section id="hiding-imports">
<h3>Hiding Imports<a class="headerlink" href="#hiding-imports" title="Permalink to this heading"></a></h3>
<h3>Hiding Imports<a class="headerlink" href="#hiding-imports" title="Permalink to this headline"></a></h3>
<p>Sometimes a module may provide many definitions, and we want to use
most of them but with a few exceptions (e.g., because those would
result to a name clash). In such situations it is convenient
@ -204,7 +203,7 @@ to use a <em>hiding</em> import:</p>
</div>
</section>
<section id="qualified-module-imports">
<h3>Qualified Module Imports<a class="headerlink" href="#qualified-module-imports" title="Permalink to this heading"></a></h3>
<h3>Qualified Module Imports<a class="headerlink" href="#qualified-module-imports" title="Permalink to this headline"></a></h3>
<p>Another way to avoid name collisions is by using a
<em>qualified</em> import.</p>
<div class="literal-block-wrapper docutils container" id="id5">
@ -253,7 +252,7 @@ but to use them, you would have to qualify using the prefix <code class="docutil
</section>
</section>
<section id="private-blocks">
<h2>Private Blocks<a class="headerlink" href="#private-blocks" title="Permalink to this heading"></a></h2>
<h2>Private Blocks<a class="headerlink" href="#private-blocks" title="Permalink to this headline"></a></h2>
<p>In some cases, definitions in a module might use helper
functions that are not intended to be used outside the module.
It is good practice to place such declarations in <em>private blocks</em>:</p>
@ -318,7 +317,7 @@ is equivalent to the previous one:</p>
</div>
</section>
<section id="nested-modules">
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this heading"></a></h2>
<h2>Nested Modules<a class="headerlink" href="#nested-modules" title="Permalink to this headline"></a></h2>
<p>Module may be declared withing other modules, using the <code class="docutils literal notranslate"><span class="pre">submodule</span></code> keword.</p>
<div class="literal-block-wrapper docutils container" id="id12">
<div class="code-block-caption"><span class="caption-text">Declaring a nested module called N</span><a class="headerlink" href="#id12" title="Permalink to this code"></a></div>
@ -355,7 +354,7 @@ to the name of a submodule.</p>
So, in the previous example, it would be an error if <code class="docutils literal notranslate"><span class="pre">y</span></code> was
to try to use <code class="docutils literal notranslate"><span class="pre">z</span></code> in its definition.</p>
<section id="implicit-imports">
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this heading"></a></h3>
<h3>Implicit Imports<a class="headerlink" href="#implicit-imports" title="Permalink to this headline"></a></h3>
<p>For convenience, we add an implicit qualified submodule import for
each locally defined submodules.</p>
<div class="literal-block-wrapper docutils container" id="id14">
@ -375,7 +374,7 @@ each locally defined submodules.</p>
an implicit import <code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">submoulde</span> <span class="pre">N</span> <span class="pre">as</span> <span class="pre">N</span></code>.</p>
</section>
<section id="managing-module-names">
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this heading"></a></h3>
<h3>Managing Module Names<a class="headerlink" href="#managing-module-names" title="Permalink to this headline"></a></h3>
<p>The names of nested modules are managed by the module system just
like the name of any other declaration in Cryptol. Thus, nested
modules may declared in the public or private sections of their
@ -407,14 +406,14 @@ another top-level module <code class="docutils literal notranslate"><span class=
</section>
</section>
<section id="parameterized-modules">
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this heading"></a></h2>
<h2>Parameterized Modules<a class="headerlink" href="#parameterized-modules" title="Permalink to this headline"></a></h2>
<div class="admonition warning">
<p class="admonition-title">Warning</p>
<p>The documentation in this section is for the upcoming variant of
the feature, which is not yet part of main line Cryptol.</p>
</div>
<section id="interface-modules">
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this heading"></a></h3>
<h3>Interface Modules<a class="headerlink" href="#interface-modules" title="Permalink to this headline"></a></h3>
<p>An <em>interface module</em> describes the content of a module
without providing a concrete implementation.</p>
<div class="literal-block-wrapper docutils container" id="id16">
@ -449,7 +448,7 @@ other modules:</p>
</div>
</section>
<section id="importing-an-interface-module">
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this heading"></a></h3>
<h3>Importing an Interface Module<a class="headerlink" href="#importing-an-interface-module" title="Permalink to this headline"></a></h3>
<p>A module may be parameterized by importing an interface,
instead of a concrete module</p>
<div class="literal-block-wrapper docutils container" id="id18">
@ -498,7 +497,7 @@ module, as described in <a class="reference internal" href="#instantiating-modul
</div>
</section>
<section id="interface-constraints">
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this heading"></a></h3>
<h3>Interface Constraints<a class="headerlink" href="#interface-constraints" title="Permalink to this headline"></a></h3>
<p>When working with multiple interfaces, it is to useful
to be able to impose additional constraints on the
types imported from the interface.</p>
@ -527,7 +526,7 @@ same. Note that, of course, the two instantiations
may provide different values for <code class="docutils literal notranslate"><span class="pre">x</span></code>.</p>
</section>
<section id="instantiating-a-parameterized-module">
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this heading"></a></h3>
<span id="instantiating-modules"></span><h3>Instantiating a Parameterized Module<a class="headerlink" href="#instantiating-a-parameterized-module" title="Permalink to this headline"></a></h3>
<p>To use a parameterized module we need to provide concrete
implementations for the interfaces that it uses, and provide
a name for the resulting module. This is done as follows:</p>
@ -622,7 +621,7 @@ use <code class="docutils literal notranslate"><span class="pre">submodule</span
</div>
</section>
<section id="anonymous-interface-modules">
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this heading"></a></h3>
<h3>Anonymous Interface Modules<a class="headerlink" href="#anonymous-interface-modules" title="Permalink to this headline"></a></h3>
<p>If we need to just parameterize a module by a couple of types/values,
it is quite cumbersome to have to define a whole separate interface module.
To make this more convenient we provide the following notation for defining
@ -646,7 +645,7 @@ Note that the parameters may not use things defined in <code class="docutils lit
the interface is declared outside of <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
</section>
<section id="anonymous-instantiation-arguments">
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this heading"></a></h3>
<h3>Anonymous Instantiation Arguments<a class="headerlink" href="#anonymous-instantiation-arguments" title="Permalink to this headline"></a></h3>
<p>Sometimes it is also a bit cumbersome to have to define a whole
separate module just to pass it as an argument to some parameterized
module. To make this more convenient we support the following notion
@ -678,7 +677,7 @@ definition of an anonymous module which is passed as the argument
to parameterized module <code class="docutils literal notranslate"><span class="pre">M</span></code>.</p>
</section>
<section id="anonymous-import-instantiations">
<h3>Anonymous Import Instantiations<a class="headerlink" href="#anonymous-import-instantiations" title="Permalink to this heading"></a></h3>
<h3>Anonymous Import Instantiations<a class="headerlink" href="#anonymous-import-instantiations" title="Permalink to this headline"></a></h3>
<p>We provide syntactic sugar for importing and instantiating a functor
at the same time:</p>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="nf">submodule</span><span class="w"> </span><span class="kt">F</span><span class="w"> </span><span class="kr">where</span><span class="w"></span>
@ -729,7 +728,7 @@ to the following declarations:</p>
</div>
</section>
<section id="passing-through-module-parameters">
<h3>Passing Through Module Parameters<a class="headerlink" href="#passing-through-module-parameters" title="Permalink to this heading"></a></h3>
<h3>Passing Through Module Parameters<a class="headerlink" href="#passing-through-module-parameters" title="Permalink to this headline"></a></h3>
<p>Occasionally it is useful to define a functor that instantiates <em>another</em>
functor using the same parameters as the functor being defined
(i.e., a functor parameter is passed on to another functor). This can

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -85,9 +84,9 @@
<div itemprop="articleBody">
<section id="overloaded-operations">
<h1>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this heading"></a></h1>
<h1>Overloaded Operations<a class="headerlink" href="#overloaded-operations" title="Permalink to this headline"></a></h1>
<section id="equality">
<h2>Equality<a class="headerlink" href="#equality" title="Permalink to this heading"></a></h2>
<h2>Equality<a class="headerlink" href="#equality" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Eq</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">==</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Eq</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">!=</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Eq</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
@ -97,7 +96,7 @@
</div>
</section>
<section id="comparisons">
<h2>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this heading"></a></h2>
<h2>Comparisons<a class="headerlink" href="#comparisons" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">Cmp</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">&lt;</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">Cmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">&gt;</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kr">Cmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
@ -110,7 +109,7 @@
</div>
</section>
<section id="signed-comparisons">
<h2>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this heading"></a></h2>
<h2>Signed Comparisons<a class="headerlink" href="#signed-comparisons" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">SignedCmp</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">&lt;$</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">SignedCmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">&gt;$</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">SignedCmp</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kr">Bit</span><span class="w"></span>
@ -120,14 +119,14 @@
</div>
</section>
<section id="zero">
<h2>Zero<a class="headerlink" href="#zero" title="Permalink to this heading"></a></h2>
<h2>Zero<a class="headerlink" href="#zero" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Zero</span><span class="w"></span>
<span class="w"> </span><span class="n">zero</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Zero</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
</pre></div>
</div>
</section>
<section id="logical-operations">
<h2>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this heading"></a></h2>
<h2>Logical Operations<a class="headerlink" href="#logical-operations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Logic</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">&amp;&amp;</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Logic</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">||</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Logic</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
@ -137,7 +136,7 @@
</div>
</section>
<section id="basic-arithmetic">
<h2>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this heading"></a></h2>
<h2>Basic Arithmetic<a class="headerlink" href="#basic-arithmetic" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Ring</span><span class="w"></span>
<span class="w"> </span><span class="n">fromInteger</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Ring</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">+</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Ring</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
@ -149,7 +148,7 @@
</div>
</section>
<section id="integral-operations">
<h2>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this heading"></a></h2>
<h2>Integral Operations<a class="headerlink" href="#integral-operations" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Integral</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">/</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Integral</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">%</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Integral</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
@ -161,7 +160,7 @@
</div>
</section>
<section id="division">
<h2>Division<a class="headerlink" href="#division" title="Permalink to this heading"></a></h2>
<h2>Division<a class="headerlink" href="#division" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Field</span><span class="w"></span>
<span class="w"> </span><span class="n">recip</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Field</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
<span class="w"> </span><span class="p">(</span><span class="o">/.</span><span class="p">)</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Field</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"></span>
@ -169,7 +168,7 @@
</div>
</section>
<section id="rounding">
<h2>Rounding<a class="headerlink" href="#rounding" title="Permalink to this heading"></a></h2>
<h2>Rounding<a class="headerlink" href="#rounding" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kt">Round</span><span class="w"></span>
<span class="w"> </span><span class="n">ceiling</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Round</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>
<span class="w"> </span><span class="n">floor</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">{</span><span class="n">a</span><span class="p">}</span><span class="w"> </span><span class="p">(</span><span class="kt">Round</span><span class="w"> </span><span class="n">a</span><span class="p">)</span><span class="w"> </span><span class="ow">=&gt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="ow">-&gt;</span><span class="w"> </span><span class="kt">Integer</span><span class="w"></span>

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -73,13 +72,14 @@
<div itemprop="articleBody">
<section id="cryptol-reference-manual">
<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this heading"></a></h1>
<h1>Cryptol Reference Manual<a class="headerlink" href="#cryptol-reference-manual" title="Permalink to this headline"></a></h1>
<div class="toctree-wrapper compound">
<p class="caption" role="heading"><span class="caption-text">Cryptol Reference Manual</span></p>
<ul>
<li class="toctree-l1"><a class="reference internal" href="BasicSyntax.html">Basic Syntax</a><ul>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#declarations">Declarations</a></li>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#type-signatures">Type Signatures</a></li>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#numeric-constraint-guards">Numeric Constraint Guards</a></li>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#layout">Layout</a></li>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#comments">Comments</a></li>
<li class="toctree-l2"><a class="reference internal" href="BasicSyntax.html#identifiers">Identifiers</a></li>

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="genindex.html" />
@ -78,9 +77,9 @@
<div itemprop="articleBody">
<section id="type-declarations">
<h1>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this heading"></a></h1>
<h1>Type Declarations<a class="headerlink" href="#type-declarations" title="Permalink to this headline"></a></h1>
<section id="type-synonyms">
<h2>Type Synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this heading"></a></h2>
<h2>Type Synonyms<a class="headerlink" href="#type-synonyms" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">type</span><span class="w"> </span><span class="kt">T</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="w"> </span><span class="n">b</span><span class="w"></span>
</pre></div>
</div>
@ -93,7 +92,7 @@ Type synonyms may mention other synonyms, but it is not
allowed to create a recursive collection of type synonyms.</p>
</section>
<section id="newtypes">
<h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this heading"></a></h2>
<h2>Newtypes<a class="headerlink" href="#newtypes" title="Permalink to this headline"></a></h2>
<div class="highlight-cryptol notranslate"><div class="highlight"><pre><span></span><span class="kr">newtype</span><span class="w"> </span><span class="kt">NewT</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="ow">=</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="nb">seq</span><span class="w"> </span><span class="kt">:</span><span class="w"> </span><span class="p">[</span><span class="n">a</span><span class="p">]</span><span class="n">b</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>
</div>

View File

@ -19,6 +19,54 @@ Type Signatures
f,g : {a,b} (fin a) => [a] b
Numeric Constraint Guards
-------------------------
A declaration with a signature can use *numeric constraint guards*,
which are used to change the behavior of a functoin depending on its
numeric type parameters. For example:
.. code-block:: cryptol
len : {n} (fin n) => [n]a -> Integer
len xs | n == 0 => 0
| n > 0 => 1 + len (drop `{1} xs)
Each behavior starts with ``|`` and lists some constraints on the numeric
parameters to a declaration. When applied, the function will use the first
definition that satisfies the provided numeric parameters.
Numeric constraint guards are quite similar to an ``if`` expression,
except that decisions are based on *types* rather than values. There
is also an important difference to simply using demotion and an
actual ``if`` statement:
.. code-block:: cryptol
len' : {n} (fin n) => [n]a -> Integer
len' xs = if `n == 0 => 0
| `n > 0 => 1 + len (drop `{1} xs)
The definition of ``len'`` is rejected, because the *value based* ``if``
expression does provide the *type based* fact ``n >= 1`` which is
required by ``drop `{1} xs``, while in ``len``, the type-checker
locally-assumes the constraint ``n > 0`` in that constraint-guarded branch
and so it can in fact determine that ``n >= 1``.
Requirements:
- Numeric constraint guards only support constraints over numeric literals,
such as ``fin``, ``<=``, ``==``, etc.
Type constraint aliases can also be used as long as they only constrain
numeric literals.
- The numeric constraint guards of a declaration should be exhaustive. The
type-checker will attempt to prove that the set of constraint guards is
exhaustive, but if it can't then it will issue a non-exhaustive constraint
guards warning. This warning is controlled by the environmental option
``warnNonExhaustiveConstraintGuards``.
- Each constraint guard is checked *independently* of the others, and there
are no implict assumptions that the previous behaviors do not match---
instead the programmer needs to specify all constraints explicitly
in the guard.
Layout
------

View File

@ -13,7 +13,19 @@ systems (macOS and Linux).
Basic usage
-----------
Suppose we want to call the following C function:
Suppose we want to implement the following function in C:
.. code-block:: cryptol
add : [32] -> [32] -> [32]
In our Cryptol file, we declare it as a ``foreign`` function with no body:
.. code-block:: cryptol
foreign add : [32] -> [32] -> [32]
Then we write the following C function:
.. code-block:: c
@ -21,11 +33,16 @@ Suppose we want to call the following C function:
return x + y;
}
In our Cryptol file, we write a ``foreign`` declaration with no body:
Cryptol can generate a C header file containing the appropriate function
prototypes given the corresponding Cryptol ``foreign`` declarations with the
``:generate-foreign-header`` command. You can then ``#include`` the generated
header file in your C file to help write the C implementation.
.. code-block:: cryptol
.. code-block::
foreign add : [32] -> [32] -> [32]
Cryptol> :generate-foreign-header Example.cry
Loading module Example
Writing header to Example.h
The C code must first be compiled into a dynamically loaded shared library. When
Cryptol loads the module containing the ``foreign`` declaration, it will look
@ -61,9 +78,9 @@ The whole process would look something like this:
Note: Since Cryptol currently only accesses the compiled binary and not the C
source, it has no way of checking that the Cryptol function type you declare in
your Cryptol code actually matches the type of the C function. **It is your
responsibility to make sure the types match up**. If they do not then there may
be undefined behavior.
your Cryptol code actually matches the type of the C function. It can generate
the correct C headers but if the actual implementation does not match it there
may be undefined behavior.
Compiling C code
----------------
@ -81,6 +98,10 @@ This section describes how a given Cryptol function signature maps to a C
function prototype. The FFI only supports a limited set of Cryptol types which
have a clear translation into C.
This mapping can now be done automatically with the ``:generate-foreign-header``
command mentioned above; however, this section is still worth reading to
understand the supported types and what the resulting C parameters mean.
Overall structure
~~~~~~~~~~~~~~~~~
@ -305,5 +326,5 @@ corresponds to the C signature
.. code-block:: c
void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
double *out0, uint32_t *out1);
void f(size_t n, uint16_t *in0, uint8_t in1_a, uint64_t in1_b,
double *out_0, uint32_t *out_1);

View File

@ -4,7 +4,7 @@
*
* Sphinx stylesheet -- basic theme.
*
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
@ -222,7 +222,7 @@ table.modindextable td {
/* -- general body styles --------------------------------------------------- */
div.body {
min-width: 360px;
min-width: 450px;
max-width: 800px;
}
@ -236,6 +236,7 @@ div.body p, div.body dd, div.body li, div.body blockquote {
a.headerlink {
visibility: hidden;
}
a.brackets:before,
span.brackets > a:before{
content: "[";
@ -246,7 +247,6 @@ span.brackets > a:after {
content: "]";
}
h1:hover > a.headerlink,
h2:hover > a.headerlink,
h3:hover > a.headerlink,
@ -334,11 +334,13 @@ aside.sidebar {
p.sidebar-title {
font-weight: bold;
}
div.admonition, div.topic, blockquote {
clear: left;
}
/* -- topics ---------------------------------------------------------------- */
div.topic {
border: 1px solid #ccc;
padding: 7px;
@ -426,6 +428,10 @@ table.docutils td, table.docutils th {
border-bottom: 1px solid #aaa;
}
table.footnote td, table.footnote th {
border: 0 !important;
}
th {
text-align: left;
padding-right: 5px;
@ -608,6 +614,7 @@ ol.simple p,
ul.simple p {
margin-bottom: 0;
}
dl.footnote > dt,
dl.citation > dt {
float: left;
@ -636,11 +643,11 @@ dl.field-list > dt {
padding-left: 0.5em;
padding-right: 5px;
}
dl.field-list > dt:after {
content: ":";
}
dl.field-list > dd {
padding-left: 0.5em;
margin-top: 0em;
@ -750,7 +757,6 @@ span.pre {
-ms-hyphens: none;
-webkit-hyphens: none;
hyphens: none;
white-space: nowrap;
}
div[class*="highlight-"] {

View File

@ -2,263 +2,322 @@
* doctools.js
* ~~~~~~~~~~~
*
* Base JavaScript utilities for all Sphinx HTML documentation.
* Sphinx JavaScript utilities for all documentation.
*
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
"use strict";
const _ready = (callback) => {
if (document.readyState !== "loading") {
callback();
} else {
document.addEventListener("DOMContentLoaded", callback);
/**
* select a different prefix for underscore
*/
$u = _.noConflict();
/**
* make the code below compatible with browsers without
* an installed firebug like debugger
if (!window.console || !console.firebug) {
var names = ["log", "debug", "info", "warn", "error", "assert", "dir",
"dirxml", "group", "groupEnd", "time", "timeEnd", "count", "trace",
"profile", "profileEnd"];
window.console = {};
for (var i = 0; i < names.length; ++i)
window.console[names[i]] = function() {};
}
*/
/**
* small helper function to urldecode strings
*
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/decodeURIComponent#Decoding_query_parameters_from_a_URL
*/
jQuery.urldecode = function(x) {
if (!x) {
return x
}
return decodeURIComponent(x.replace(/\+/g, ' '));
};
/**
* highlight a given string on a node by wrapping it in
* small helper function to urlencode strings
*/
jQuery.urlencode = encodeURIComponent;
/**
* This function returns the parsed url parameters of the
* current request. Multiple values per key are supported,
* it will always return arrays of strings for the value parts.
*/
jQuery.getQueryParameters = function(s) {
if (typeof s === 'undefined')
s = document.location.search;
var parts = s.substr(s.indexOf('?') + 1).split('&');
var result = {};
for (var i = 0; i < parts.length; i++) {
var tmp = parts[i].split('=', 2);
var key = jQuery.urldecode(tmp[0]);
var value = jQuery.urldecode(tmp[1]);
if (key in result)
result[key].push(value);
else
result[key] = [value];
}
return result;
};
/**
* highlight a given string on a jquery object by wrapping it in
* span elements with the given class name.
*/
const _highlight = (node, addItems, text, className) => {
if (node.nodeType === Node.TEXT_NODE) {
const val = node.nodeValue;
const parent = node.parentNode;
const pos = val.toLowerCase().indexOf(text);
if (
pos >= 0 &&
!parent.classList.contains(className) &&
!parent.classList.contains("nohighlight")
) {
let span;
const closestNode = parent.closest("body, svg, foreignObject");
const isInSVG = closestNode && closestNode.matches("svg");
if (isInSVG) {
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
} else {
span = document.createElement("span");
span.classList.add(className);
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
parent.insertBefore(
span,
parent.insertBefore(
jQuery.fn.highlightText = function(text, className) {
function highlight(node, addItems) {
if (node.nodeType === 3) {
var val = node.nodeValue;
var pos = val.toLowerCase().indexOf(text);
if (pos >= 0 &&
!jQuery(node.parentNode).hasClass(className) &&
!jQuery(node.parentNode).hasClass("nohighlight")) {
var span;
var isInSVG = jQuery(node).closest("body, svg, foreignObject").is("svg");
if (isInSVG) {
span = document.createElementNS("http://www.w3.org/2000/svg", "tspan");
} else {
span = document.createElement("span");
span.className = className;
}
span.appendChild(document.createTextNode(val.substr(pos, text.length)));
node.parentNode.insertBefore(span, node.parentNode.insertBefore(
document.createTextNode(val.substr(pos + text.length)),
node.nextSibling
)
);
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
const rect = document.createElementNS(
"http://www.w3.org/2000/svg",
"rect"
);
const bbox = parent.getBBox();
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute("class", className);
addItems.push({ parent: parent, target: rect });
node.nextSibling));
node.nodeValue = val.substr(0, pos);
if (isInSVG) {
var rect = document.createElementNS("http://www.w3.org/2000/svg", "rect");
var bbox = node.parentElement.getBBox();
rect.x.baseVal.value = bbox.x;
rect.y.baseVal.value = bbox.y;
rect.width.baseVal.value = bbox.width;
rect.height.baseVal.value = bbox.height;
rect.setAttribute('class', className);
addItems.push({
"parent": node.parentNode,
"target": rect});
}
}
}
} else if (node.matches && !node.matches("button, select, textarea")) {
node.childNodes.forEach((el) => _highlight(el, addItems, text, className));
else if (!jQuery(node).is("button, select, textarea")) {
jQuery.each(node.childNodes, function() {
highlight(this, addItems);
});
}
}
var addItems = [];
var result = this.each(function() {
highlight(this, addItems);
});
for (var i = 0; i < addItems.length; ++i) {
jQuery(addItems[i].parent).before(addItems[i].target);
}
return result;
};
const _highlightText = (thisNode, text, className) => {
let addItems = [];
_highlight(thisNode, addItems, text, className);
addItems.forEach((obj) =>
obj.parent.insertAdjacentElement("beforebegin", obj.target)
);
};
/*
* backward compatibility for jQuery.browser
* This will be supported until firefox bug is fixed.
*/
if (!jQuery.browser) {
jQuery.uaMatch = function(ua) {
ua = ua.toLowerCase();
var match = /(chrome)[ \/]([\w.]+)/.exec(ua) ||
/(webkit)[ \/]([\w.]+)/.exec(ua) ||
/(opera)(?:.*version|)[ \/]([\w.]+)/.exec(ua) ||
/(msie) ([\w.]+)/.exec(ua) ||
ua.indexOf("compatible") < 0 && /(mozilla)(?:.*? rv:([\w.]+)|)/.exec(ua) ||
[];
return {
browser: match[ 1 ] || "",
version: match[ 2 ] || "0"
};
};
jQuery.browser = {};
jQuery.browser[jQuery.uaMatch(navigator.userAgent).browser] = true;
}
/**
* Small JavaScript module for the documentation.
*/
const Documentation = {
init: () => {
Documentation.highlightSearchWords();
Documentation.initDomainIndexTable();
Documentation.initOnKeyListeners();
var Documentation = {
init : function() {
this.fixFirefoxAnchorBug();
this.highlightSearchWords();
this.initIndexTable();
if (DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) {
this.initOnKeyListeners();
}
},
/**
* i18n support
*/
TRANSLATIONS: {},
PLURAL_EXPR: (n) => (n === 1 ? 0 : 1),
LOCALE: "unknown",
TRANSLATIONS : {},
PLURAL_EXPR : function(n) { return n === 1 ? 0 : 1; },
LOCALE : 'unknown',
// gettext and ngettext don't access this so that the functions
// can safely bound to a different name (_ = Documentation.gettext)
gettext: (string) => {
const translated = Documentation.TRANSLATIONS[string];
switch (typeof translated) {
case "undefined":
return string; // no translation
case "string":
return translated; // translation exists
default:
return translated[0]; // (singular, plural) translation tuple exists
}
gettext : function(string) {
var translated = Documentation.TRANSLATIONS[string];
if (typeof translated === 'undefined')
return string;
return (typeof translated === 'string') ? translated : translated[0];
},
ngettext: (singular, plural, n) => {
const translated = Documentation.TRANSLATIONS[singular];
if (typeof translated !== "undefined")
return translated[Documentation.PLURAL_EXPR(n)];
return n === 1 ? singular : plural;
ngettext : function(singular, plural, n) {
var translated = Documentation.TRANSLATIONS[singular];
if (typeof translated === 'undefined')
return (n == 1) ? singular : plural;
return translated[Documentation.PLURALEXPR(n)];
},
addTranslations: (catalog) => {
Object.assign(Documentation.TRANSLATIONS, catalog.messages);
Documentation.PLURAL_EXPR = new Function(
"n",
`return (${catalog.plural_expr})`
);
Documentation.LOCALE = catalog.locale;
addTranslations : function(catalog) {
for (var key in catalog.messages)
this.TRANSLATIONS[key] = catalog.messages[key];
this.PLURAL_EXPR = new Function('n', 'return +(' + catalog.plural_expr + ')');
this.LOCALE = catalog.locale;
},
/**
* add context elements like header anchor links
*/
addContextElements : function() {
$('div[id] > :header:first').each(function() {
$('<a class="headerlink">\u00B6</a>').
attr('href', '#' + this.id).
attr('title', _('Permalink to this headline')).
appendTo(this);
});
$('dt[id]').each(function() {
$('<a class="headerlink">\u00B6</a>').
attr('href', '#' + this.id).
attr('title', _('Permalink to this definition')).
appendTo(this);
});
},
/**
* workaround a firefox stupidity
* see: https://bugzilla.mozilla.org/show_bug.cgi?id=645075
*/
fixFirefoxAnchorBug : function() {
if (document.location.hash && $.browser.mozilla)
window.setTimeout(function() {
document.location.href += '';
}, 10);
},
/**
* highlight the search words provided in the url in the text
*/
highlightSearchWords: () => {
const highlight =
new URLSearchParams(window.location.search).get("highlight") || "";
const terms = highlight.toLowerCase().split(/\s+/).filter(x => x);
if (terms.length === 0) return; // nothing to do
highlightSearchWords : function() {
var params = $.getQueryParameters();
var terms = (params.highlight) ? params.highlight[0].split(/\s+/) : [];
if (terms.length) {
var body = $('div.body');
if (!body.length) {
body = $('body');
}
window.setTimeout(function() {
$.each(terms, function() {
body.highlightText(this.toLowerCase(), 'highlighted');
});
}, 10);
$('<p class="highlight-link"><a href="javascript:Documentation.' +
'hideSearchWords()">' + _('Hide Search Matches') + '</a></p>')
.appendTo($('#searchbox'));
}
},
// There should never be more than one element matching "div.body"
const divBody = document.querySelectorAll("div.body");
const body = divBody.length ? divBody[0] : document.querySelector("body");
window.setTimeout(() => {
terms.forEach((term) => _highlightText(body, term, "highlighted"));
}, 10);
const searchBox = document.getElementById("searchbox");
if (searchBox === null) return;
searchBox.appendChild(
document
.createRange()
.createContextualFragment(
'<p class="highlight-link">' +
'<a href="javascript:Documentation.hideSearchWords()">' +
Documentation.gettext("Hide Search Matches") +
"</a></p>"
)
);
/**
* init the domain index toggle buttons
*/
initIndexTable : function() {
var togglers = $('img.toggler').click(function() {
var src = $(this).attr('src');
var idnum = $(this).attr('id').substr(7);
$('tr.cg-' + idnum).toggle();
if (src.substr(-9) === 'minus.png')
$(this).attr('src', src.substr(0, src.length-9) + 'plus.png');
else
$(this).attr('src', src.substr(0, src.length-8) + 'minus.png');
}).css('display', '');
if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) {
togglers.click();
}
},
/**
* helper function to hide the search marks again
*/
hideSearchWords: () => {
document
.querySelectorAll("#searchbox .highlight-link")
.forEach((el) => el.remove());
document
.querySelectorAll("span.highlighted")
.forEach((el) => el.classList.remove("highlighted"));
const url = new URL(window.location);
url.searchParams.delete("highlight");
window.history.replaceState({}, "", url);
hideSearchWords : function() {
$('#searchbox .highlight-link').fadeOut(300);
$('span.highlighted').removeClass('highlighted');
},
/**
* helper function to focus on search bar
* make the url absolute
*/
focusSearchBar: () => {
document.querySelectorAll("input[name=q]")[0]?.focus();
makeURL : function(relativeURL) {
return DOCUMENTATION_OPTIONS.URL_ROOT + '/' + relativeURL;
},
/**
* Initialise the domain index toggle buttons
* get the current relative url
*/
initDomainIndexTable: () => {
const toggler = (el) => {
const idNumber = el.id.substr(7);
const toggledRows = document.querySelectorAll(`tr.cg-${idNumber}`);
if (el.src.substr(-9) === "minus.png") {
el.src = `${el.src.substr(0, el.src.length - 9)}plus.png`;
toggledRows.forEach((el) => (el.style.display = "none"));
} else {
el.src = `${el.src.substr(0, el.src.length - 8)}minus.png`;
toggledRows.forEach((el) => (el.style.display = ""));
}
};
const togglerElements = document.querySelectorAll("img.toggler");
togglerElements.forEach((el) =>
el.addEventListener("click", (event) => toggler(event.currentTarget))
);
togglerElements.forEach((el) => (el.style.display = ""));
if (DOCUMENTATION_OPTIONS.COLLAPSE_INDEX) togglerElements.forEach(toggler);
getCurrentURL : function() {
var path = document.location.pathname;
var parts = path.split(/\//);
$.each(DOCUMENTATION_OPTIONS.URL_ROOT.split(/\//), function() {
if (this === '..')
parts.pop();
});
var url = parts.join('/');
return path.substring(url.lastIndexOf('/') + 1, path.length - 1);
},
initOnKeyListeners: () => {
// only install a listener if it is really needed
if (
!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS &&
!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS
)
return;
const blacklistedElements = new Set([
"TEXTAREA",
"INPUT",
"SELECT",
"BUTTON",
]);
document.addEventListener("keydown", (event) => {
if (blacklistedElements.has(document.activeElement.tagName)) return; // bail for input elements
if (event.altKey || event.ctrlKey || event.metaKey) return; // bail with special keys
if (!event.shiftKey) {
switch (event.key) {
case "ArrowLeft":
if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break;
const prevLink = document.querySelector('link[rel="prev"]');
if (prevLink && prevLink.href) {
window.location.href = prevLink.href;
event.preventDefault();
initOnKeyListeners: function() {
$(document).keydown(function(event) {
var activeElementType = document.activeElement.tagName;
// don't navigate when in search box, textarea, dropdown or button
if (activeElementType !== 'TEXTAREA' && activeElementType !== 'INPUT' && activeElementType !== 'SELECT'
&& activeElementType !== 'BUTTON' && !event.altKey && !event.ctrlKey && !event.metaKey
&& !event.shiftKey) {
switch (event.keyCode) {
case 37: // left
var prevHref = $('link[rel="prev"]').prop('href');
if (prevHref) {
window.location.href = prevHref;
return false;
}
break;
case "ArrowRight":
if (!DOCUMENTATION_OPTIONS.NAVIGATION_WITH_KEYS) break;
const nextLink = document.querySelector('link[rel="next"]');
if (nextLink && nextLink.href) {
window.location.href = nextLink.href;
event.preventDefault();
case 39: // right
var nextHref = $('link[rel="next"]').prop('href');
if (nextHref) {
window.location.href = nextHref;
return false;
}
break;
case "Escape":
if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break;
Documentation.hideSearchWords();
event.preventDefault();
}
}
// some keyboard layouts may need Shift to get /
switch (event.key) {
case "/":
if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) break;
Documentation.focusSearchBar();
event.preventDefault();
}
});
},
}
};
// quick alias for translations
const _ = Documentation.gettext;
_ = Documentation.gettext;
_ready(Documentation.init);
$(document).ready(function() {
Documentation.init();
});

View File

@ -1,14 +1,12 @@
var DOCUMENTATION_OPTIONS = {
URL_ROOT: document.getElementById("documentation_options").getAttribute('data-url_root'),
VERSION: '2.11.0',
LANGUAGE: 'en',
LANGUAGE: 'None',
COLLAPSE_INDEX: false,
BUILDER: 'html',
FILE_SUFFIX: '.html',
LINK_SUFFIX: '.html',
HAS_SOURCE: true,
SOURCELINK_SUFFIX: '.txt',
NAVIGATION_WITH_KEYS: false,
SHOW_SEARCH_SUMMARY: true,
ENABLE_SEARCH_SHORTCUTS: true,
NAVIGATION_WITH_KEYS: false
};

File diff suppressed because one or more lines are too long

View File

@ -5,12 +5,12 @@
* This script contains the language-specific data used by searchtools.js,
* namely the list of stopwords, stemmer, scorer and splitter.
*
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
var stopwords = ["a", "and", "are", "as", "at", "be", "but", "by", "for", "if", "in", "into", "is", "it", "near", "no", "not", "of", "on", "or", "such", "that", "the", "their", "then", "there", "these", "they", "this", "to", "was", "will", "with"];
var stopwords = ["a","and","are","as","at","be","but","by","for","if","in","into","is","it","near","no","not","of","on","or","such","that","the","their","then","there","these","they","this","to","was","will","with"];
/* Non-minified version is copied as a separate JS file, is available */
@ -197,3 +197,101 @@ var Stemmer = function() {
}
}
var splitChars = (function() {
var result = {};
var singles = [96, 180, 187, 191, 215, 247, 749, 885, 903, 907, 909, 930, 1014, 1648,
1748, 1809, 2416, 2473, 2481, 2526, 2601, 2609, 2612, 2615, 2653, 2702,
2706, 2729, 2737, 2740, 2857, 2865, 2868, 2910, 2928, 2948, 2961, 2971,
2973, 3085, 3089, 3113, 3124, 3213, 3217, 3241, 3252, 3295, 3341, 3345,
3369, 3506, 3516, 3633, 3715, 3721, 3736, 3744, 3748, 3750, 3756, 3761,
3781, 3912, 4239, 4347, 4681, 4695, 4697, 4745, 4785, 4799, 4801, 4823,
4881, 5760, 5901, 5997, 6313, 7405, 8024, 8026, 8028, 8030, 8117, 8125,
8133, 8181, 8468, 8485, 8487, 8489, 8494, 8527, 11311, 11359, 11687, 11695,
11703, 11711, 11719, 11727, 11735, 12448, 12539, 43010, 43014, 43019, 43587,
43696, 43713, 64286, 64297, 64311, 64317, 64319, 64322, 64325, 65141];
var i, j, start, end;
for (i = 0; i < singles.length; i++) {
result[singles[i]] = true;
}
var ranges = [[0, 47], [58, 64], [91, 94], [123, 169], [171, 177], [182, 184], [706, 709],
[722, 735], [741, 747], [751, 879], [888, 889], [894, 901], [1154, 1161],
[1318, 1328], [1367, 1368], [1370, 1376], [1416, 1487], [1515, 1519], [1523, 1568],
[1611, 1631], [1642, 1645], [1750, 1764], [1767, 1773], [1789, 1790], [1792, 1807],
[1840, 1868], [1958, 1968], [1970, 1983], [2027, 2035], [2038, 2041], [2043, 2047],
[2070, 2073], [2075, 2083], [2085, 2087], [2089, 2307], [2362, 2364], [2366, 2383],
[2385, 2391], [2402, 2405], [2419, 2424], [2432, 2436], [2445, 2446], [2449, 2450],
[2483, 2485], [2490, 2492], [2494, 2509], [2511, 2523], [2530, 2533], [2546, 2547],
[2554, 2564], [2571, 2574], [2577, 2578], [2618, 2648], [2655, 2661], [2672, 2673],
[2677, 2692], [2746, 2748], [2750, 2767], [2769, 2783], [2786, 2789], [2800, 2820],
[2829, 2830], [2833, 2834], [2874, 2876], [2878, 2907], [2914, 2917], [2930, 2946],
[2955, 2957], [2966, 2968], [2976, 2978], [2981, 2983], [2987, 2989], [3002, 3023],
[3025, 3045], [3059, 3076], [3130, 3132], [3134, 3159], [3162, 3167], [3170, 3173],
[3184, 3191], [3199, 3204], [3258, 3260], [3262, 3293], [3298, 3301], [3312, 3332],
[3386, 3388], [3390, 3423], [3426, 3429], [3446, 3449], [3456, 3460], [3479, 3481],
[3518, 3519], [3527, 3584], [3636, 3647], [3655, 3663], [3674, 3712], [3717, 3718],
[3723, 3724], [3726, 3731], [3752, 3753], [3764, 3772], [3774, 3775], [3783, 3791],
[3802, 3803], [3806, 3839], [3841, 3871], [3892, 3903], [3949, 3975], [3980, 4095],
[4139, 4158], [4170, 4175], [4182, 4185], [4190, 4192], [4194, 4196], [4199, 4205],
[4209, 4212], [4226, 4237], [4250, 4255], [4294, 4303], [4349, 4351], [4686, 4687],
[4702, 4703], [4750, 4751], [4790, 4791], [4806, 4807], [4886, 4887], [4955, 4968],
[4989, 4991], [5008, 5023], [5109, 5120], [5741, 5742], [5787, 5791], [5867, 5869],
[5873, 5887], [5906, 5919], [5938, 5951], [5970, 5983], [6001, 6015], [6068, 6102],
[6104, 6107], [6109, 6111], [6122, 6127], [6138, 6159], [6170, 6175], [6264, 6271],
[6315, 6319], [6390, 6399], [6429, 6469], [6510, 6511], [6517, 6527], [6572, 6592],
[6600, 6607], [6619, 6655], [6679, 6687], [6741, 6783], [6794, 6799], [6810, 6822],
[6824, 6916], [6964, 6980], [6988, 6991], [7002, 7042], [7073, 7085], [7098, 7167],
[7204, 7231], [7242, 7244], [7294, 7400], [7410, 7423], [7616, 7679], [7958, 7959],
[7966, 7967], [8006, 8007], [8014, 8015], [8062, 8063], [8127, 8129], [8141, 8143],
[8148, 8149], [8156, 8159], [8173, 8177], [8189, 8303], [8306, 8307], [8314, 8318],
[8330, 8335], [8341, 8449], [8451, 8454], [8456, 8457], [8470, 8472], [8478, 8483],
[8506, 8507], [8512, 8516], [8522, 8525], [8586, 9311], [9372, 9449], [9472, 10101],
[10132, 11263], [11493, 11498], [11503, 11516], [11518, 11519], [11558, 11567],
[11622, 11630], [11632, 11647], [11671, 11679], [11743, 11822], [11824, 12292],
[12296, 12320], [12330, 12336], [12342, 12343], [12349, 12352], [12439, 12444],
[12544, 12548], [12590, 12592], [12687, 12689], [12694, 12703], [12728, 12783],
[12800, 12831], [12842, 12880], [12896, 12927], [12938, 12976], [12992, 13311],
[19894, 19967], [40908, 40959], [42125, 42191], [42238, 42239], [42509, 42511],
[42540, 42559], [42592, 42593], [42607, 42622], [42648, 42655], [42736, 42774],
[42784, 42785], [42889, 42890], [42893, 43002], [43043, 43055], [43062, 43071],
[43124, 43137], [43188, 43215], [43226, 43249], [43256, 43258], [43260, 43263],
[43302, 43311], [43335, 43359], [43389, 43395], [43443, 43470], [43482, 43519],
[43561, 43583], [43596, 43599], [43610, 43615], [43639, 43641], [43643, 43647],
[43698, 43700], [43703, 43704], [43710, 43711], [43715, 43738], [43742, 43967],
[44003, 44015], [44026, 44031], [55204, 55215], [55239, 55242], [55292, 55295],
[57344, 63743], [64046, 64047], [64110, 64111], [64218, 64255], [64263, 64274],
[64280, 64284], [64434, 64466], [64830, 64847], [64912, 64913], [64968, 65007],
[65020, 65135], [65277, 65295], [65306, 65312], [65339, 65344], [65371, 65381],
[65471, 65473], [65480, 65481], [65488, 65489], [65496, 65497]];
for (i = 0; i < ranges.length; i++) {
start = ranges[i][0];
end = ranges[i][1];
for (j = start; j <= end; j++) {
result[j] = true;
}
}
return result;
})();
function splitQuery(query) {
var result = [];
var start = -1;
for (var i = 0; i < query.length; i++) {
if (splitChars[query.charCodeAt(i)]) {
if (start !== -1) {
result.push(query.slice(start, i));
start = -1;
}
} else if (start === -1) {
start = i;
}
}
if (start !== -1) {
result.push(query.slice(start));
}
return result;
}

View File

@ -4,24 +4,22 @@
*
* Sphinx JavaScript utilities for the full-text search.
*
* :copyright: Copyright 2007-2022 by the Sphinx team, see AUTHORS.
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
* :license: BSD, see LICENSE for details.
*
*/
"use strict";
/**
* Simple result scoring code.
*/
if (typeof Scorer === "undefined") {
if (!Scorer) {
/**
* Simple result scoring code.
*/
var Scorer = {
// Implement the following function to further tweak the score for each result
// The function takes a result array [docname, title, anchor, descr, score, filename]
// The function takes a result array [filename, title, anchor, descr, score]
// and returns the new score.
/*
score: result => {
const [docname, title, anchor, descr, score, filename] = result
return score
score: function(result) {
return result[4];
},
*/
@ -30,11 +28,9 @@ if (typeof Scorer === "undefined") {
// or matches in the last dotted part of the object name
objPartialMatch: 6,
// Additive scores depending on the priority of the object
objPrio: {
0: 15, // used to be importantResults
1: 5, // used to be objectResults
2: -5, // used to be unimportantResults
},
objPrio: {0: 15, // used to be importantResults
1: 5, // used to be objectResults
2: -5}, // used to be unimportantResults
// Used when the priority is not in the mapping.
objPrioDefault: 0,
@ -43,453 +39,459 @@ if (typeof Scorer === "undefined") {
partialTitle: 7,
// query found in terms
term: 5,
partialTerm: 2,
partialTerm: 2
};
}
const _removeChildren = (element) => {
while (element && element.lastChild) element.removeChild(element.lastChild);
};
/**
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions#escaping
*/
const _escapeRegExp = (string) =>
string.replace(/[.*+\-?^${}()|[\]\\]/g, "\\$&"); // $& means the whole matched string
const _displayItem = (item, highlightTerms, searchTerms) => {
const docBuilder = DOCUMENTATION_OPTIONS.BUILDER;
const docUrlRoot = DOCUMENTATION_OPTIONS.URL_ROOT;
const docFileSuffix = DOCUMENTATION_OPTIONS.FILE_SUFFIX;
const docLinkSuffix = DOCUMENTATION_OPTIONS.LINK_SUFFIX;
const showSearchSummary = DOCUMENTATION_OPTIONS.SHOW_SEARCH_SUMMARY;
const [docName, title, anchor, descr] = item;
let listItem = document.createElement("li");
let requestUrl;
let linkUrl;
if (docBuilder === "dirhtml") {
// dirhtml builder
let dirname = docName + "/";
if (dirname.match(/\/index\/$/))
dirname = dirname.substring(0, dirname.length - 6);
else if (dirname === "index/") dirname = "";
requestUrl = docUrlRoot + dirname;
linkUrl = requestUrl;
} else {
// normal html builders
requestUrl = docUrlRoot + docName + docFileSuffix;
linkUrl = docName + docLinkSuffix;
if (!splitQuery) {
function splitQuery(query) {
return query.split(/\s+/);
}
const params = new URLSearchParams();
params.set("highlight", [...highlightTerms].join(" "));
let linkEl = listItem.appendChild(document.createElement("a"));
linkEl.href = linkUrl + "?" + params.toString() + anchor;
linkEl.innerHTML = title;
if (descr)
listItem.appendChild(document.createElement("span")).innerHTML =
" (" + descr + ")";
else if (showSearchSummary)
fetch(requestUrl)
.then((responseData) => responseData.text())
.then((data) => {
if (data)
listItem.appendChild(
Search.makeSearchSummary(data, searchTerms, highlightTerms)
);
});
Search.output.appendChild(listItem);
};
const _finishSearch = (resultCount) => {
Search.stopPulse();
Search.title.innerText = _("Search Results");
if (!resultCount)
Search.status.innerText = Documentation.gettext(
"Your search did not match any documents. Please make sure that all words are spelled correctly and that you've selected enough categories."
);
else
Search.status.innerText = _(
`Search finished, found ${resultCount} page(s) matching the search query.`
);
};
const _displayNextItem = (
results,
resultCount,
highlightTerms,
searchTerms
) => {
// results left, load the summary and display it
// this is intended to be dynamic (don't sub resultsCount)
if (results.length) {
_displayItem(results.pop(), highlightTerms, searchTerms);
setTimeout(
() => _displayNextItem(results, resultCount, highlightTerms, searchTerms),
5
);
}
// search finished, update title and status message
else _finishSearch(resultCount);
};
/**
* Default splitQuery function. Can be overridden in ``sphinx.search`` with a
* custom function per language.
*
* The regular expression works by splitting the string on consecutive characters
* that are not Unicode letters, numbers, underscores, or emoji characters.
* This is the same as ``\W+`` in Python, preserving the surrogate pair area.
*/
if (typeof splitQuery === "undefined") {
var splitQuery = (query) => query
.split(/[^\p{Letter}\p{Number}_\p{Emoji_Presentation}]+/gu)
.filter(term => term) // remove remaining empty strings
}
/**
* Search Module
*/
const Search = {
_index: null,
_queued_query: null,
_pulse_status: -1,
var Search = {
htmlToText: (htmlString) => {
const htmlElement = new DOMParser().parseFromString(htmlString, 'text/html');
htmlElement.querySelectorAll(".headerlink").forEach((el) => { el.remove() });
const docContent = htmlElement.querySelector('[role="main"]');
if (docContent !== undefined) return docContent.textContent;
console.warn(
"Content block not found. Sphinx search tries to obtain it via '[role=main]'. Could you check your theme or template."
);
return "";
_index : null,
_queued_query : null,
_pulse_status : -1,
htmlToText : function(htmlString) {
var virtualDocument = document.implementation.createHTMLDocument('virtual');
var htmlElement = $(htmlString, virtualDocument);
htmlElement.find('.headerlink').remove();
docContent = htmlElement.find('[role=main]')[0];
if(docContent === undefined) {
console.warn("Content block not found. Sphinx search tries to obtain it " +
"via '[role=main]'. Could you check your theme or template.");
return "";
}
return docContent.textContent || docContent.innerText;
},
init: () => {
const query = new URLSearchParams(window.location.search).get("q");
document
.querySelectorAll('input[name="q"]')
.forEach((el) => (el.value = query));
if (query) Search.performSearch(query);
init : function() {
var params = $.getQueryParameters();
if (params.q) {
var query = params.q[0];
$('input[name="q"]')[0].value = query;
this.performSearch(query);
}
},
loadIndex: (url) =>
(document.body.appendChild(document.createElement("script")).src = url),
loadIndex : function(url) {
$.ajax({type: "GET", url: url, data: null,
dataType: "script", cache: true,
complete: function(jqxhr, textstatus) {
if (textstatus != "success") {
document.getElementById("searchindexloader").src = url;
}
}});
},
setIndex: (index) => {
Search._index = index;
if (Search._queued_query !== null) {
const query = Search._queued_query;
Search._queued_query = null;
Search.query(query);
setIndex : function(index) {
var q;
this._index = index;
if ((q = this._queued_query) !== null) {
this._queued_query = null;
Search.query(q);
}
},
hasIndex: () => Search._index !== null,
hasIndex : function() {
return this._index !== null;
},
deferQuery: (query) => (Search._queued_query = query),
deferQuery : function(query) {
this._queued_query = query;
},
stopPulse: () => (Search._pulse_status = -1),
stopPulse : function() {
this._pulse_status = 0;
},
startPulse: () => {
if (Search._pulse_status >= 0) return;
const pulse = () => {
startPulse : function() {
if (this._pulse_status >= 0)
return;
function pulse() {
var i;
Search._pulse_status = (Search._pulse_status + 1) % 4;
Search.dots.innerText = ".".repeat(Search._pulse_status);
if (Search._pulse_status >= 0) window.setTimeout(pulse, 500);
};
var dotString = '';
for (i = 0; i < Search._pulse_status; i++)
dotString += '.';
Search.dots.text(dotString);
if (Search._pulse_status > -1)
window.setTimeout(pulse, 500);
}
pulse();
},
/**
* perform a search for something (or wait until index is loaded)
*/
performSearch: (query) => {
performSearch : function(query) {
// create the required interface elements
const searchText = document.createElement("h2");
searchText.textContent = _("Searching");
const searchSummary = document.createElement("p");
searchSummary.classList.add("search-summary");
searchSummary.innerText = "";
const searchList = document.createElement("ul");
searchList.classList.add("search");
this.out = $('#search-results');
this.title = $('<h2>' + _('Searching') + '</h2>').appendTo(this.out);
this.dots = $('<span></span>').appendTo(this.title);
this.status = $('<p class="search-summary">&nbsp;</p>').appendTo(this.out);
this.output = $('<ul class="search"/>').appendTo(this.out);
const out = document.getElementById("search-results");
Search.title = out.appendChild(searchText);
Search.dots = Search.title.appendChild(document.createElement("span"));
Search.status = out.appendChild(searchSummary);
Search.output = out.appendChild(searchList);
const searchProgress = document.getElementById("search-progress");
// Some themes don't use the search progress node
if (searchProgress) {
searchProgress.innerText = _("Preparing search...");
}
Search.startPulse();
$('#search-progress').text(_('Preparing search...'));
this.startPulse();
// index already loaded, the browser was quick!
if (Search.hasIndex()) Search.query(query);
else Search.deferQuery(query);
if (this.hasIndex())
this.query(query);
else
this.deferQuery(query);
},
/**
* execute search (requires search index to be loaded)
*/
query: (query) => {
// stem the search terms and add them to the correct list
const stemmer = new Stemmer();
const searchTerms = new Set();
const excludedTerms = new Set();
const highlightTerms = new Set();
const objectTerms = new Set(splitQuery(query.toLowerCase().trim()));
splitQuery(query.trim()).forEach((queryTerm) => {
const queryTermLower = queryTerm.toLowerCase();
query : function(query) {
var i;
// maybe skip this "word"
// stopwords array is from language_data.js
if (
stopwords.indexOf(queryTermLower) !== -1 ||
queryTerm.match(/^\d+$/)
)
return;
// stem the word
let word = stemmer.stemWord(queryTermLower);
// select the correct list
if (word[0] === "-") excludedTerms.add(word.substr(1));
else {
searchTerms.add(word);
highlightTerms.add(queryTermLower);
// stem the searchterms and add them to the correct list
var stemmer = new Stemmer();
var searchterms = [];
var excluded = [];
var hlterms = [];
var tmp = splitQuery(query);
var objectterms = [];
for (i = 0; i < tmp.length; i++) {
if (tmp[i] !== "") {
objectterms.push(tmp[i].toLowerCase());
}
});
// console.debug("SEARCH: searching for:");
// console.info("required: ", [...searchTerms]);
// console.info("excluded: ", [...excludedTerms]);
if ($u.indexOf(stopwords, tmp[i].toLowerCase()) != -1 || tmp[i] === "") {
// skip this "word"
continue;
}
// stem the word
var word = stemmer.stemWord(tmp[i].toLowerCase());
// prevent stemmer from cutting word smaller than two chars
if(word.length < 3 && tmp[i].length >= 3) {
word = tmp[i];
}
var toAppend;
// select the correct list
if (word[0] == '-') {
toAppend = excluded;
word = word.substr(1);
}
else {
toAppend = searchterms;
hlterms.push(tmp[i].toLowerCase());
}
// only add if not already in the list
if (!$u.contains(toAppend, word))
toAppend.push(word);
}
var highlightstring = '?highlight=' + $.urlencode(hlterms.join(" "));
// array of [docname, title, anchor, descr, score, filename]
let results = [];
_removeChildren(document.getElementById("search-progress"));
// console.debug('SEARCH: searching for:');
// console.info('required: ', searchterms);
// console.info('excluded: ', excluded);
// prepare search
var terms = this._index.terms;
var titleterms = this._index.titleterms;
// array of [filename, title, anchor, descr, score]
var results = [];
$('#search-progress').empty();
// lookup as object
objectTerms.forEach((term) =>
results.push(...Search.performObjectSearch(term, objectTerms))
);
for (i = 0; i < objectterms.length; i++) {
var others = [].concat(objectterms.slice(0, i),
objectterms.slice(i+1, objectterms.length));
results = results.concat(this.performObjectSearch(objectterms[i], others));
}
// lookup as search terms in fulltext
results.push(...Search.performTermsSearch(searchTerms, excludedTerms));
results = results.concat(this.performTermsSearch(searchterms, excluded, terms, titleterms));
// let the scorer override scores with a custom scoring function
if (Scorer.score) results.forEach((item) => (item[4] = Scorer.score(item)));
if (Scorer.score) {
for (i = 0; i < results.length; i++)
results[i][4] = Scorer.score(results[i]);
}
// now sort the results by score (in opposite order of appearance, since the
// display function below uses pop() to retrieve items) and then
// alphabetically
results.sort((a, b) => {
const leftScore = a[4];
const rightScore = b[4];
if (leftScore === rightScore) {
results.sort(function(a, b) {
var left = a[4];
var right = b[4];
if (left > right) {
return 1;
} else if (left < right) {
return -1;
} else {
// same score: sort alphabetically
const leftTitle = a[1].toLowerCase();
const rightTitle = b[1].toLowerCase();
if (leftTitle === rightTitle) return 0;
return leftTitle > rightTitle ? -1 : 1; // inverted is intentional
left = a[1].toLowerCase();
right = b[1].toLowerCase();
return (left > right) ? -1 : ((left < right) ? 1 : 0);
}
return leftScore > rightScore ? 1 : -1;
});
// remove duplicate search results
// note the reversing of results, so that in the case of duplicates, the highest-scoring entry is kept
let seen = new Set();
results = results.reverse().reduce((acc, result) => {
let resultStr = result.slice(0, 4).concat([result[5]]).map(v => String(v)).join(',');
if (!seen.has(resultStr)) {
acc.push(result);
seen.add(resultStr);
}
return acc;
}, []);
results = results.reverse();
// for debugging
//Search.lastresults = results.slice(); // a copy
// console.info("search results:", Search.lastresults);
//console.info('search results:', Search.lastresults);
// print the results
_displayNextItem(results, results.length, highlightTerms, searchTerms);
var resultCount = results.length;
function displayNextItem() {
// results left, load the summary and display it
if (results.length) {
var item = results.pop();
var listItem = $('<li></li>');
var requestUrl = "";
var linkUrl = "";
if (DOCUMENTATION_OPTIONS.BUILDER === 'dirhtml') {
// dirhtml builder
var dirname = item[0] + '/';
if (dirname.match(/\/index\/$/)) {
dirname = dirname.substring(0, dirname.length-6);
} else if (dirname == 'index/') {
dirname = '';
}
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + dirname;
linkUrl = requestUrl;
} else {
// normal html builders
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + item[0] + DOCUMENTATION_OPTIONS.FILE_SUFFIX;
linkUrl = item[0] + DOCUMENTATION_OPTIONS.LINK_SUFFIX;
}
listItem.append($('<a/>').attr('href',
linkUrl +
highlightstring + item[2]).html(item[1]));
if (item[3]) {
listItem.append($('<span> (' + item[3] + ')</span>'));
Search.output.append(listItem);
setTimeout(function() {
displayNextItem();
}, 5);
} else if (DOCUMENTATION_OPTIONS.HAS_SOURCE) {
$.ajax({url: requestUrl,
dataType: "text",
complete: function(jqxhr, textstatus) {
var data = jqxhr.responseText;
if (data !== '' && data !== undefined) {
var summary = Search.makeSearchSummary(data, searchterms, hlterms);
if (summary) {
listItem.append(summary);
}
}
Search.output.append(listItem);
setTimeout(function() {
displayNextItem();
}, 5);
}});
} else {
// no source available, just display title
Search.output.append(listItem);
setTimeout(function() {
displayNextItem();
}, 5);
}
}
// search finished, update title and status message
else {
Search.stopPulse();
Search.title.text(_('Search Results'));
if (!resultCount)
Search.status.text(_('Your search did not match any documents. Please make sure that all words are spelled correctly and that you\'ve selected enough categories.'));
else
Search.status.text(_('Search finished, found %s page(s) matching the search query.').replace('%s', resultCount));
Search.status.fadeIn(500);
}
}
displayNextItem();
},
/**
* search for object names
*/
performObjectSearch: (object, objectTerms) => {
const filenames = Search._index.filenames;
const docNames = Search._index.docnames;
const objects = Search._index.objects;
const objNames = Search._index.objnames;
const titles = Search._index.titles;
performObjectSearch : function(object, otherterms) {
var filenames = this._index.filenames;
var docnames = this._index.docnames;
var objects = this._index.objects;
var objnames = this._index.objnames;
var titles = this._index.titles;
const results = [];
var i;
var results = [];
const objectSearchCallback = (prefix, match) => {
const name = match[4]
const fullname = (prefix ? prefix + "." : "") + name;
const fullnameLower = fullname.toLowerCase();
if (fullnameLower.indexOf(object) < 0) return;
let score = 0;
const parts = fullnameLower.split(".");
// check for different match types: exact matches of full name or
// "last name" (i.e. last dotted part)
if (fullnameLower === object || parts.slice(-1)[0] === object)
score += Scorer.objNameMatch;
else if (parts.slice(-1)[0].indexOf(object) > -1)
score += Scorer.objPartialMatch; // matches in last name
const objName = objNames[match[1]][2];
const title = titles[match[0]];
// If more than one term searched for, we require other words to be
// found in the name/title/description
const otherTerms = new Set(objectTerms);
otherTerms.delete(object);
if (otherTerms.size > 0) {
const haystack = `${prefix} ${name} ${objName} ${title}`.toLowerCase();
if (
[...otherTerms].some((otherTerm) => haystack.indexOf(otherTerm) < 0)
)
return;
for (var prefix in objects) {
if (!(objects[prefix] instanceof Array)) {
objects[prefix] = Object.entries(objects[prefix]).map(([name, match]) => [...match, name]);
}
for (var iMatch = 0; iMatch != objects[prefix].length; ++iMatch) {
var match = objects[prefix][iMatch];
var name = match[4];
var fullname = (prefix ? prefix + '.' : '') + name;
var fullnameLower = fullname.toLowerCase()
if (fullnameLower.indexOf(object) > -1) {
var score = 0;
var parts = fullnameLower.split('.');
// check for different match types: exact matches of full name or
// "last name" (i.e. last dotted part)
if (fullnameLower == object || parts[parts.length - 1] == object) {
score += Scorer.objNameMatch;
// matches in last name
} else if (parts[parts.length - 1].indexOf(object) > -1) {
score += Scorer.objPartialMatch;
}
var objname = objnames[match[1]][2];
var title = titles[match[0]];
// If more than one term searched for, we require other words to be
// found in the name/title/description
if (otherterms.length > 0) {
var haystack = (prefix + ' ' + name + ' ' +
objname + ' ' + title).toLowerCase();
var allfound = true;
for (i = 0; i < otherterms.length; i++) {
if (haystack.indexOf(otherterms[i]) == -1) {
allfound = false;
break;
}
}
if (!allfound) {
continue;
}
}
var descr = objname + _(', in ') + title;
let anchor = match[3];
if (anchor === "") anchor = fullname;
else if (anchor === "-") anchor = objNames[match[1]][1] + "-" + fullname;
var anchor = match[3];
if (anchor === '')
anchor = fullname;
else if (anchor == '-')
anchor = objnames[match[1]][1] + '-' + fullname;
// add custom score for some objects according to scorer
if (Scorer.objPrio.hasOwnProperty(match[2])) {
score += Scorer.objPrio[match[2]];
} else {
score += Scorer.objPrioDefault;
}
results.push([docnames[match[0]], fullname, '#'+anchor, descr, score, filenames[match[0]]]);
}
}
}
const descr = objName + _(", in ") + title;
// add custom score for some objects according to scorer
if (Scorer.objPrio.hasOwnProperty(match[2]))
score += Scorer.objPrio[match[2]];
else score += Scorer.objPrioDefault;
results.push([
docNames[match[0]],
fullname,
"#" + anchor,
descr,
score,
filenames[match[0]],
]);
};
Object.keys(objects).forEach((prefix) =>
objects[prefix].forEach((array) =>
objectSearchCallback(prefix, array)
)
);
return results;
},
/**
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions
*/
escapeRegExp : function(string) {
return string.replace(/[.*+\-?^${}()|[\]\\]/g, '\\$&'); // $& means the whole matched string
},
/**
* search for full-text terms in the index
*/
performTermsSearch: (searchTerms, excludedTerms) => {
// prepare search
const terms = Search._index.terms;
const titleTerms = Search._index.titleterms;
const docNames = Search._index.docnames;
const filenames = Search._index.filenames;
const titles = Search._index.titles;
performTermsSearch : function(searchterms, excluded, terms, titleterms) {
var docnames = this._index.docnames;
var filenames = this._index.filenames;
var titles = this._index.titles;
const scoreMap = new Map();
const fileMap = new Map();
var i, j, file;
var fileMap = {};
var scoreMap = {};
var results = [];
// perform the search on the required terms
searchTerms.forEach((word) => {
const files = [];
const arr = [
{ files: terms[word], score: Scorer.term },
{ files: titleTerms[word], score: Scorer.title },
for (i = 0; i < searchterms.length; i++) {
var word = searchterms[i];
var files = [];
var _o = [
{files: terms[word], score: Scorer.term},
{files: titleterms[word], score: Scorer.title}
];
// add support for partial matches
if (word.length > 2) {
const escapedWord = _escapeRegExp(word);
Object.keys(terms).forEach((term) => {
if (term.match(escapedWord) && !terms[word])
arr.push({ files: terms[term], score: Scorer.partialTerm });
});
Object.keys(titleTerms).forEach((term) => {
if (term.match(escapedWord) && !titleTerms[word])
arr.push({ files: titleTerms[word], score: Scorer.partialTitle });
});
var word_regex = this.escapeRegExp(word);
for (var w in terms) {
if (w.match(word_regex) && !terms[word]) {
_o.push({files: terms[w], score: Scorer.partialTerm})
}
}
for (var w in titleterms) {
if (w.match(word_regex) && !titleterms[word]) {
_o.push({files: titleterms[w], score: Scorer.partialTitle})
}
}
}
// no match but word was a required one
if (arr.every((record) => record.files === undefined)) return;
if ($u.every(_o, function(o){return o.files === undefined;})) {
break;
}
// found search word in contents
arr.forEach((record) => {
if (record.files === undefined) return;
$u.each(_o, function(o) {
var _files = o.files;
if (_files === undefined)
return
let recordFiles = record.files;
if (recordFiles.length === undefined) recordFiles = [recordFiles];
files.push(...recordFiles);
if (_files.length === undefined)
_files = [_files];
files = files.concat(_files);
// set score for the word in each file
recordFiles.forEach((file) => {
if (!scoreMap.has(file)) scoreMap.set(file, {});
scoreMap.get(file)[word] = record.score;
});
// set score for the word in each file to Scorer.term
for (j = 0; j < _files.length; j++) {
file = _files[j];
if (!(file in scoreMap))
scoreMap[file] = {};
scoreMap[file][word] = o.score;
}
});
// create the mapping
files.forEach((file) => {
if (fileMap.has(file) && fileMap.get(file).indexOf(word) === -1)
fileMap.get(file).push(word);
else fileMap.set(file, [word]);
});
});
for (j = 0; j < files.length; j++) {
file = files[j];
if (file in fileMap && fileMap[file].indexOf(word) === -1)
fileMap[file].push(word);
else
fileMap[file] = [word];
}
}
// now check if the files don't contain excluded terms
const results = [];
for (const [file, wordList] of fileMap) {
// check if all requirements are matched
for (file in fileMap) {
var valid = true;
// as search terms with length < 3 are discarded
const filteredTermCount = [...searchTerms].filter(
(term) => term.length > 2
).length;
// check if all requirements are matched
var filteredTermCount = // as search terms with length < 3 are discarded: ignore
searchterms.filter(function(term){return term.length > 2}).length
if (
wordList.length !== searchTerms.size &&
wordList.length !== filteredTermCount
)
continue;
fileMap[file].length != searchterms.length &&
fileMap[file].length != filteredTermCount
) continue;
// ensure that none of the excluded terms is in the search result
if (
[...excludedTerms].some(
(term) =>
terms[term] === file ||
titleTerms[term] === file ||
(terms[term] || []).includes(file) ||
(titleTerms[term] || []).includes(file)
)
)
break;
for (i = 0; i < excluded.length; i++) {
if (terms[excluded[i]] == file ||
titleterms[excluded[i]] == file ||
$u.contains(terms[excluded[i]] || [], file) ||
$u.contains(titleterms[excluded[i]] || [], file)) {
valid = false;
break;
}
}
// select one (max) score for the file.
const score = Math.max(...wordList.map((w) => scoreMap.get(file)[w]));
// add result to the result list
results.push([
docNames[file],
titles[file],
"",
null,
score,
filenames[file],
]);
// if we have still a valid result we can add it to the result list
if (valid) {
// select one (max) score for the file.
// for better ranking, we should calculate ranking by using words statistics like basic tf-idf...
var score = $u.max($u.map(fileMap[file], function(w){return scoreMap[file][w]}));
results.push([docnames[file], titles[file], '', null, score, filenames[file]]);
}
}
return results;
},
@ -497,34 +499,34 @@ const Search = {
/**
* helper function to return a node containing the
* search summary for a given text. keywords is a list
* of stemmed words, highlightWords is the list of normal, unstemmed
* of stemmed words, hlwords is the list of normal, unstemmed
* words. the first one is used to find the occurrence, the
* latter for highlighting it.
*/
makeSearchSummary: (htmlText, keywords, highlightWords) => {
const text = Search.htmlToText(htmlText);
if (text === "") return null;
const textLower = text.toLowerCase();
const actualStartPosition = [...keywords]
.map((k) => textLower.indexOf(k.toLowerCase()))
.filter((i) => i > -1)
.slice(-1)[0];
const startWithContext = Math.max(actualStartPosition - 120, 0);
const top = startWithContext === 0 ? "" : "...";
const tail = startWithContext + 240 < text.length ? "..." : "";
let summary = document.createElement("p");
summary.classList.add("context");
summary.textContent = top + text.substr(startWithContext, 240).trim() + tail;
highlightWords.forEach((highlightWord) =>
_highlightText(summary, highlightWord, "highlighted")
);
return summary;
},
makeSearchSummary : function(htmlText, keywords, hlwords) {
var text = Search.htmlToText(htmlText);
if (text == "") {
return null;
}
var textLower = text.toLowerCase();
var start = 0;
$.each(keywords, function() {
var i = textLower.indexOf(this.toLowerCase());
if (i > -1)
start = i;
});
start = Math.max(start - 120, 0);
var excerpt = ((start > 0) ? '...' : '') +
$.trim(text.substr(start, 240)) +
((start + 240 - text.length) ? '...' : '');
var rv = $('<p class="context"></p>').text(excerpt);
$.each(hlwords, function() {
rv = rv.highlightText(this, 'highlighted');
});
return rv;
}
};
_ready(Search.init);
$(document).ready(function() {
Search.init();
});

File diff suppressed because one or more lines are too long

View File

@ -13,7 +13,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<link rel="index" title="Index" href="#" />

View File

@ -14,7 +14,6 @@
<script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
<script src="_static/jquery.js"></script>
<script src="_static/underscore.js"></script>
<script src="_static/_sphinx_javascript_frameworks_compat.js"></script>
<script src="_static/doctools.js"></script>
<script src="_static/js/theme.js"></script>
<script src="_static/searchtools.js"></script>

File diff suppressed because one or more lines are too long

313
docs/ffi-presentation.md Normal file
View File

@ -0,0 +1,313 @@
---
title: Cryptol FFI
author: Bretton
date: 2022-09-02
---
# Cryptol FFI
- Call functions written in C
---
# Why?
- Performance
- Use existing code in C
- Do things that Cryptol can't do?
---
# What does it look like?
```cry
foreign add : [32] -> [32] -> [32]
```
```c
uint32_t add(uint32_t x, uint32_t y) {
return x + y;
}
```
```
Main> add 1 2
0x00000003
```
---
# How do you use it?
```
+-------------+
| Example.cry | ------------------------+ +---------------Cryptol---------------+
+-------------+ | | Cryptol> :l Example.cry |
| | Loading module Cryptol |
+-----------+ +---------------+ +------>| Loading module Example |
| Example.c | =====> | Example.so | -------->| Loading dynamic library Example.so |
+-----------+ cc | Example.dylib | dlopen | Example> add 1 2 |
+---------------+ | 0x00000003 |
+-------------------------------------+
```
- Find shared library with same name as Cryptol file
- Dynamically load with `dlopen`
- Bind each `foreign` function with `dlsym`
- Windows not supported yet
- Compile it yourself (for now...)
- `cc -fPIC -shared Example.c -o Example.so`
- `cc -dynamiclib Example.c -o Example.dylib`
---
# How does it work?
- Since Cryptol is interpreted, number/types of arguments to foreign functions are not known statically
- `libffi` calls functions with the right calling conventions given interface at runtime
- Rant about `libffi` in Haskell
---
# Supported types
## Basic types
Cryptol | C
--- | ---
Bit | uint8_t
[K]Bit, 0 <= K <= 8 | uint8_t
[K]Bit, 8 < K <= 16 | uint16_t
[K]Bit, 16 < K <= 32 | uint32_t
[K]Bit, 32 < K <= 64 | uint64_t
Float32 | float
Float64 | double
---
# Supported types
## Multiple arguments?
Cryptol | C
--- | ---
A -> B -> ... -> Z | Z' (A', B', ...)
---
# Supported types
## More complex types
- So far it has been pretty simple
- How about sequences? I guess we need arrays
- Who allocates the memory?
- Who owns the memory?
- How are they passed vs returned?
---
# Supported types
## Sequences
Cryptol | C
--- | ---
[n1][n2]...[nk]T | U*
where
T | U
--- | ---
[K]Bit, 0 <= K <= 8 | uint8_t
[K]Bit, 8 < K <= 16 | uint16_t
[K]Bit, 16 < K <= 32 | uint32_t
[K]Bit, 32 < K <= 64 | uint64_t
Float32 | float
Float64 | double
- Cryptol allocates and owns all memory
- Sequence as Cryptol parameter: `const U*` C parameter
- Sequence as Cryptol return type: `U*` C output parameter
- Passed after Cryptol parameters
- Return type of C function is `void`
- Multidimensional sequences: flatten (except the [K]Bit part)
- How about n1, n2, ..., nk?
- Must be `fin`
---
# Supported ~~types~~ kinds?
## Numeric type arguments
Cryptol | C
--- | ---
\# | size_t
- Must be `fin`
- Type arguments are passed before any value arguments
---
# Supported types
## Tuples and records as parameters
- Passed as separate arguments
Cryptol | C (multiple!)
--- | ---
(T1, T2, ..., Tn) | U1, U2, ..., Un
{s1: T1, s2: T2, ..., sn: Tn} | U1, U2, ..., Un
where
Cryptol | C
--- | ---
Ti | Ui
Note:
- Order of record fields is however it's written in the type in the source code
- Uncurried and curried Cryptol functions correspond to the same C function
- () corresponds to no arguments at all
- Can be nested
---
# Supported types
## Tuples and records as return types
- Returned as separate output parameters
- This means the component types need to become pointers
- Except for sequences which are already pointers
Cryptol | C (multiple!)
--- | ---
(T1, T2, ..., Tn) | V1, V2, ..., Vn
{s1: T1, s2: T2, ..., sn: Tn} | V1, V2, ..., Vn
where
Cryptol parameter | C
--- | ---
Ti | Ui
and Vi = if Ui is a pointer type then Ui else Ui*
Note:
- Return type of C function is `void`
- () corresponds to no return value and no output arguments
- Can be nested
---
# Supported types
## Type synonyms
- Type synonyms are expanded before applying the previous rules
---
# Examples
```cry
foreign f : {n} (fin n) => [n][10] -> {a : Bit, b : [64]} -> (Float64, [n + 1][20])
```
```c
void f(size_t n, uint16_t *in0, uint8_t in1, uint64_t in2,
double *out0, uint32_t *out1);
```
- More examples in FFI tests
---
# Evaluation
- All arguments are fully evaluated
- Result will be fully evaluated too (of course)
---
# Questionable uses of FFI
```cry
foreign print : {n} (fin n) => [n][8] -> ()
```
```c
void print(size_t n, char *s) {
printf("%.*s\n", (int) n, s);
}
```
```
Main> print "Hello world!"
Hello world!
()
```
```cry
foreign launchMissiles : ()
```
etc
- Cryptol functions should be pure
- Beware of laziness
---
# AES example
- Replacement for `SuiteB` module using AES-NI for AES functions
- ~5.5x faster
- But could actually be much faster, if not limited to 1 block
---
# Somewhat interesting(?) implementation details
- `ForeignPtr` for `dlclose`
- Interesting types in FFI marshalling
```hs
getMarshalBasicArg :: FFIBasicType ->
(forall a. FFIArg a => (GenValue Concrete -> Eval a) -> b) -> b
data GetRet = GetRet
{ getRetAsValue :: forall a. FFIRet a => IO a
, getRetAsOutArgs :: [SomeFFIArg] -> IO () }
```
---
# Future work
- Automatically generate header files from `foreign` declarations
- Support Windows
- Support Integer/Z
- Cryptol implementation of `foreign` functions + SAW integration
---
# Other stuff (not FFI)
- `:time` command for benchmarking evaluation of Cryptol expressions
- Evaluates it a bunch of times and reports the average time
- Import specific operators
- `import M ((<+>))`
- Fixed fixity (fixedity?) of prefix operators
- `-x**2` parses as `-(x**2)` not `(-x)**2`
---
# Thank you!
- Iavor, Eddy, Ryan
# Questions?
- Why is the Cryptol logo a water drop

2
examples/SuiteB_FFI/.gitignore vendored Normal file
View File

@ -0,0 +1,2 @@
*.so
*.dylib

View File

@ -0,0 +1,46 @@
SHELL = /bin/bash
CFLAGS = -O3 -Wall -Wextra -Werror
.PHONY: test perf-test perf-bench clean
ifeq ($(shell uname -m),x86_64)
ifdef PORTABLE
CFLAGS += -maes -mssse3
else
CFLAGS += -march=native
endif
endif
ifeq ($(shell uname),Darwin)
SO = SuiteB_FFI.dylib
TEST_OUT_EXT = .stdout.darwin
$(SO): SuiteB_FFI.c
$(CC) $(CFLAGS) -dynamiclib $< -o $@
else
SO = SuiteB_FFI.so
TEST_OUT_EXT = .stdout
$(SO): SuiteB_FFI.c
$(CC) $(CFLAGS) -fPIC -shared $< -o $@
endif
test: $(SO)
diff tests/aes-vectors.icry$(TEST_OUT_EXT) <(cryptol -b tests/aes-vectors.icry)
diff tests/aes-mct-ecb.icry$(TEST_OUT_EXT) <(cryptol -b tests/aes-mct-ecb.icry)
perf-test: $(SO)
time cryptol -b tests/aes-mct-ecb.icry
time cryptol -b ../../tests/suiteb/aes-mct-ecb.icry
perf-bench: $(SO)
cryptol -b perf-bench.icry
clean:
rm $(SO)

View File

@ -0,0 +1,58 @@
# `SuiteB_FFI`
`SuiteB_FFI` is a drop-in replacement for the builtin `SuiteB` module, using the
FFI to implement AES operations with hardware AES-NI instructions when
available, and falling back to the `SuiteB` software implementation in Cryptol
and Haskell otherwise.
When AES-NI is available, it is several times faster than `SuiteB`; on a Linux
machine with an Intel i7-10510U it is about 5.5x faster. Note that AES-NI is
only available on modern x86-64 processors, but you could modify this to support
similar instructions for other architectures or bind to a portable C library
instead.
The actual AES implementation is written with x86-64 intrinsics in C and based
on Intel's [AES-NI
whitepaper](https://www.intel.com/content/dam/doc/white-paper/advanced-encryption-standard-new-instructions-set-paper.pdf)
but with modifications to support how the `SuiteB` module's API is structured.
In particular, the representation of round keys as `[4][32]` in `SuiteB` means
that we need to do a byte swap every time we access memory to correct for
endianness.
Maintaining compatibility with `SuiteB` actually severely limits the speedup
that we can achieve: right now about 96% of the time spent calling the encrypt
function in Cryptol is spent doing the Cryptol evaluation surrounding the FFI
call and the actual AES computation only takes up less than 4% of the total
time. This is because the encrypt function in `SuiteB` only encrypts one block,
so if you were to create a foreign function that encrypted many blocks at once,
the overhead would be much smaller relative to the work done in the foreign
function and you would achieve a much greater speedup.
The implementation passes the AES tests from the Cryptol SuiteB test suite
(`aes-mct-ecb` and `aes-vectors`) but has not been verified beyond that.
## Usage
Run `make` to build the C code. The code checks for hardware AES-NI support at
runtime with `cpuid` when any AES function is first used. On non-x86-64
platforms, running `make` will build a dummy implementation that always falls
back to software `SuiteB`. On x86-64, `make` uses `-march=native` to build an
optimized version for running on the current machine. To build a (somewhat)
portable version that will run on any x86-64 machine with AES-NI and SSSE3, use
`make PORTABLE=1`. Once it is built, loading the `SuiteB_FFI` Cryptol module
will automatically load the shared library.
Run `make test` to test correctness. This runs the tests in the `tests/`
directory which are copied from Cryptol's `/tests/suiteb/` but using the
`SuiteB_FFI` module instead of `SuiteB`.
Run `make perf-test` to test performance on the `aes-mct-ecb` test. This prints
out the time it takes to run the test with the FFI version and the Cryptol
version.
Run `make perf-bench` to test the performance of the individual AES-128
functions with Cryptol's `:time` benchmarking command. This prints out the
benchmarked time for the key expansion and encryption functions for both
implementations, and the speedup in both cases.
Run `make clean` to delete generated files.

View File

@ -0,0 +1,384 @@
// Based on sample code from the Intel AES-NI whitepaper
// https://www.intel.com/content/dam/doc/white-paper/advanced-encryption-standard-new-instructions-set-paper.pdf
#include <stdint.h>
#include <string.h>
#ifdef __x86_64__
#include <cpuid.h>
#include <immintrin.h>
// Since Cryptol represents the round keys using [4][32], we need to do a byte
// swap every time we write/read the keys to/from memory to correct for
// endianness.
#define BSWAP32_128 _mm_set_epi64x(0x0c0d0e0f08090a0b, 0x0405060700010203)
uint8_t checkAESNISupported() {
unsigned int eax, ebx, ecx, edx;
if (!__get_cpuid(1, &eax, &ebx, &ecx, &edx)) {
return 0;
}
return (ecx & bit_AES) != 0;
}
static inline void invert_schedule(unsigned int roundKeysLength,
const uint32_t *encInitialKey, const uint32_t *encRoundKeys,
const uint32_t *encFinalKey, uint32_t *decInitialKey, uint32_t *decRoundKeys,
uint32_t *decFinalKey) {
__m128i tmp;
__m128i bswap32 = BSWAP32_128;
__m128i *encRoundKeys128 = (__m128i *) encRoundKeys;
__m128i *decRoundKeys128 = (__m128i *) decRoundKeys;
memcpy(decInitialKey, encFinalKey, 16);
for (unsigned int i = 0; i < roundKeysLength; ++i) {
tmp = _mm_loadu_si128(encRoundKeys128 + roundKeysLength - 1 - i);
tmp = _mm_shuffle_epi8(tmp, bswap32);
tmp = _mm_aesimc_si128(tmp);
tmp = _mm_shuffle_epi8(tmp, bswap32);
_mm_storeu_si128(decRoundKeys128 + i, tmp);
}
memcpy(decFinalKey, encInitialKey, 16);
}
static inline __m128i prepare_roundkey_128(__m128i tmp1, __m128i tmp2) {
__m128i tmp3;
tmp2 = _mm_shuffle_epi32(tmp2, 0xff);
tmp3 = _mm_slli_si128(tmp1, 0x4);
tmp1 = _mm_xor_si128(tmp1, tmp3);
tmp3 = _mm_slli_si128(tmp3, 0x4);
tmp1 = _mm_xor_si128(tmp1, tmp3);
tmp3 = _mm_slli_si128(tmp3, 0x4);
tmp1 = _mm_xor_si128(tmp1, tmp3);
tmp1 = _mm_xor_si128(tmp1, tmp2);
return tmp1;
}
void aesniExpandEncrypt128(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey) {
__m128i tmp1, tmp2, tmp3;
__m128i bswap32 = BSWAP32_128;
__m128i *encRoundKeys128 = (__m128i *) encRoundKeys;
tmp1 = _mm_loadu_si128((__m128i *) key);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encInitialKey, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x1);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x2);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 1, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x4);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 2, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x8);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 3, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x10);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 4, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x20);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 5, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x40);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 6, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x80);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 7, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x1b);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 8, tmp3);
tmp2 = _mm_aeskeygenassist_si128(tmp1, 0x36);
tmp1 = prepare_roundkey_128(tmp1, tmp2);
tmp3 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encFinalKey, tmp3);
}
void aesniExpandEncryptDecrypt128(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
aesniExpandEncrypt128(key, encInitialKey, encRoundKeys, encFinalKey);
invert_schedule(9, encInitialKey, encRoundKeys, encFinalKey, decInitialKey,
decRoundKeys, decFinalKey);
}
void aesniExpandDecrypt128(const uint8_t *key, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
uint32_t encInitialKey[4];
uint32_t encRoundKeys[4 * 9];
uint32_t encFinalKey[4];
aesniExpandEncryptDecrypt128(key, encInitialKey, encRoundKeys, encFinalKey,
decInitialKey, decRoundKeys, decFinalKey);
}
static inline void prepare_roundkey_192(__m128i *tmp1, __m128i *tmp2,
__m128i *tmp3) {
__m128i tmp4;
*tmp2 = _mm_shuffle_epi32(*tmp2, 0x55);
tmp4 = _mm_slli_si128(*tmp1, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
*tmp1 = _mm_xor_si128(*tmp1, *tmp2);
*tmp2 = _mm_shuffle_epi32(*tmp1, 0xff);
tmp4 = _mm_slli_si128(*tmp3, 0x4);
*tmp3 = _mm_xor_si128(*tmp3, tmp4);
*tmp3 = _mm_xor_si128(*tmp3, *tmp2);
}
void aesniExpandEncrypt192(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey) {
__m128i tmp1, tmp2, tmp3, tmp4;
__m128i bswap32 = BSWAP32_128;
__m128i *key128 = (__m128i *) key;
__m128i *encRoundKeys128 = (__m128i *) encRoundKeys;
tmp1 = _mm_loadu_si128(key128);
tmp3 = _mm_loadu_si128(key128 + 1);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encInitialKey, tmp4);
tmp4 = tmp3;
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x1);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp4, (__m128d) tmp1, 0);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128, tmp4);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp1, (__m128d) tmp3, 1);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 1, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x2);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 2, tmp4);
tmp4 = tmp3;
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x4);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp4, (__m128d) tmp1, 0);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 3, tmp4);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp1, (__m128d) tmp3, 1);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 4, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x8);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 5, tmp4);
tmp4 = tmp3;
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x10);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp4, (__m128d) tmp1, 0);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 6, tmp4);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp1, (__m128d) tmp3, 1);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 7, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x20);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 8, tmp4);
tmp4 = tmp3;
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x40);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp4, (__m128d) tmp1, 0);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 9, tmp4);
tmp4 = (__m128i) _mm_shuffle_pd((__m128d) tmp1, (__m128d) tmp3, 1);
tmp4 = _mm_shuffle_epi8(tmp4, bswap32);
_mm_storeu_si128(encRoundKeys128 + 10, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x80);
prepare_roundkey_192(&tmp1, &tmp2, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encFinalKey, tmp4);
}
void aesniExpandEncryptDecrypt192(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
aesniExpandEncrypt192(key, encInitialKey, encRoundKeys, encFinalKey);
invert_schedule(11, encInitialKey, encRoundKeys, encFinalKey, decInitialKey,
decRoundKeys, decFinalKey);
}
void aesniExpandDecrypt192(const uint8_t *key, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
uint32_t encInitialKey[4];
uint32_t encRoundKeys[4 * 11];
uint32_t encFinalKey[4];
aesniExpandEncryptDecrypt192(key, encInitialKey, encRoundKeys, encFinalKey,
decInitialKey, decRoundKeys, decFinalKey);
}
static inline void prepare_roundkey_256_1(__m128i *tmp1, __m128i *tmp2) {
__m128i tmp4;
*tmp2 = _mm_shuffle_epi32(*tmp2, 0xff);
tmp4 = _mm_slli_si128(*tmp1, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp1 = _mm_xor_si128(*tmp1, tmp4);
*tmp1 = _mm_xor_si128(*tmp1, *tmp2);
}
static inline void prepare_roundkey_256_2(__m128i *tmp1, __m128i *tmp3) {
__m128i tmp2, tmp4;
tmp4 = _mm_aeskeygenassist_si128(*tmp1, 0x0);
tmp2 = _mm_shuffle_epi32(tmp4, 0xaa);
tmp4 = _mm_slli_si128(*tmp3, 0x4);
*tmp3 = _mm_xor_si128(*tmp3, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp3 = _mm_xor_si128(*tmp3, tmp4);
tmp4 = _mm_slli_si128(tmp4, 0x4);
*tmp3 = _mm_xor_si128(*tmp3, tmp4);
*tmp3 = _mm_xor_si128(*tmp3, tmp2);
}
void aesniExpandEncrypt256(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey) {
__m128i tmp1, tmp2, tmp3, tmp4;
__m128i bswap32 = BSWAP32_128;
__m128i *key128 = (__m128i *) key;
__m128i *encRoundKeys128 = (__m128i *) encRoundKeys;
tmp1 = _mm_loadu_si128(key128);
tmp3 = _mm_loadu_si128(key128 + 1);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encInitialKey, tmp4);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128, tmp4);
tmp2 = _mm_aeskeygenassist_si128 (tmp3, 0x01);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 1, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 2, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x02);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 3, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 4, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x04);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 5, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 6, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x08);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 7, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 8, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x10);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 9, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 10, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x20);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128(encRoundKeys128 + 11, tmp4);
prepare_roundkey_256_2(&tmp1, &tmp3);
tmp4 = _mm_shuffle_epi8(tmp3, bswap32);
_mm_storeu_si128(encRoundKeys128 + 12, tmp4);
tmp2 = _mm_aeskeygenassist_si128(tmp3, 0x40);
prepare_roundkey_256_1(&tmp1, &tmp2);
tmp4 = _mm_shuffle_epi8(tmp1, bswap32);
_mm_storeu_si128((__m128i *) encFinalKey, tmp4);
}
void aesniExpandEncryptDecrypt256(const uint8_t *key, uint32_t *encInitialKey,
uint32_t *encRoundKeys, uint32_t *encFinalKey, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
aesniExpandEncrypt256(key, encInitialKey, encRoundKeys, encFinalKey);
invert_schedule(13, encInitialKey, encRoundKeys, encFinalKey, decInitialKey,
decRoundKeys, decFinalKey);
}
void aesniExpandDecrypt256(const uint8_t *key, uint32_t *decInitialKey,
uint32_t *decRoundKeys, uint32_t *decFinalKey) {
uint32_t encInitialKey[4];
uint32_t encRoundKeys[4 * 13];
uint32_t encFinalKey[4];
aesniExpandEncryptDecrypt256(key, encInitialKey, encRoundKeys, encFinalKey,
decInitialKey, decRoundKeys, decFinalKey);
}
void aesniEncryptBlock(size_t k, const uint32_t *encInitialKey,
const uint32_t *encRoundKeys, const uint32_t *encFinalKey,
const uint8_t *plaintext, uint8_t *ciphertext) {
__m128i tmp1, tmp2;
__m128i bswap32 = BSWAP32_128;
__m128i *encRoundKeys128 = (__m128i *) encRoundKeys;
tmp1 = _mm_loadu_si128((__m128i *) plaintext);
tmp2 = _mm_loadu_si128((__m128i *) encInitialKey);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_xor_si128(tmp1, tmp2);
for (size_t i = 0; i < k + 5; i++) {
tmp2 = _mm_loadu_si128(encRoundKeys128 + i);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_aesenc_si128(tmp1, tmp2);
}
tmp2 = _mm_loadu_si128((__m128i *) encFinalKey);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_aesenclast_si128(tmp1, tmp2);
_mm_storeu_si128((__m128i *) ciphertext, tmp1);
}
void aesniDecryptBlock(size_t k, const uint32_t *decInitialKey,
const uint32_t *decRoundKeys, const uint32_t *decFinalKey,
const uint8_t *ciphertext, uint8_t *plaintext) {
__m128i tmp1, tmp2;
__m128i bswap32 = BSWAP32_128;
__m128i *decRoundKeys128 = (__m128i *) decRoundKeys;
tmp1 = _mm_loadu_si128((__m128i *) ciphertext);
tmp2 = _mm_loadu_si128((__m128i *) decInitialKey);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_xor_si128(tmp1, tmp2);
for (size_t i = 0; i < k + 5; i++) {
tmp2 = _mm_loadu_si128(decRoundKeys128 + i);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_aesdec_si128(tmp1, tmp2);
}
tmp2 = _mm_loadu_si128((__m128i *) decFinalKey);
tmp2 = _mm_shuffle_epi8(tmp2, bswap32);
tmp1 = _mm_aesdeclast_si128(tmp1, tmp2);
_mm_storeu_si128((__m128i *) plaintext, tmp1);
}
#else
uint8_t checkAESNISupported() {
return 0;
}
void *aesniExpandEncrypt128 = NULL;
void *aesniExpandEncryptDecrypt128 = NULL;
void *aesniExpandDecrypt128 = NULL;
void *aesniExpandEncrypt192 = NULL;
void *aesniExpandEncryptDecrypt192 = NULL;
void *aesniExpandDecrypt192 = NULL;
void *aesniExpandEncrypt256 = NULL;
void *aesniExpandEncryptDecrypt256 = NULL;
void *aesniExpandDecrypt256 = NULL;
void *aesniEncryptBlock = NULL;
void *aesniDecryptBlock = NULL;
#endif

View File

@ -0,0 +1,194 @@
module SuiteB_FFI where
import SuiteB as SB
/***** AES ******/
/**
* Key schedule parameter setting for AES-128
*/
type AES128 = SB::AES128
/**
* Key schedule parameter setting for AES-192
*/
type AES192 = SB::AES192
/**
* Key schedule parameter setting for AES-256
*/
type AES256 = SB::AES256
/**
* Element of an AES key schedule for use in a particular round
*/
type AESRoundKey = SB::AESRoundKey
/**
* Expanded encryption key schedule for AES
*/
type AESEncryptKeySchedule k = SB::AESEncryptKeySchedule k
/**
* Expanded decryption key schedule for AES
*/
type AESDecryptKeySchedule k = SB::AESDecryptKeySchedule k
/**
* Encryption key expansion for AES-128.
* See FIPS 197, section 5.2.
*/
aes128EncryptSchedule : [128] -> AESEncryptKeySchedule AES128
aes128EncryptSchedule =
if aesniSupported
then \key -> aesniExpandEncrypt128 (split key)
else SB::aes128EncryptSchedule
/**
* Decryption key expansion for AES-128, for use in the "equivalent inverse cypher".
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes128DecryptSchedule : [128] -> AESDecryptKeySchedule AES128
aes128DecryptSchedule =
if aesniSupported
then \key -> aesniExpandDecrypt128 (split key)
else SB::aes128DecryptSchedule
/**
* Encryption and decryption key schedules for AES-128.
* If you will need both schedules, it is slightly more efficient
* to call this function than to compute the two schedules separately.
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes128Schedules : [128] -> (AESEncryptKeySchedule AES128, AESDecryptKeySchedule AES128)
aes128Schedules =
if aesniSupported
then \key -> aesniExpandEncryptDecrypt128 (split key)
else SB::aes128Schedules
/**
* Encryption key expansion for AES-192.
* See FIPS 197, section 5.2.
*/
aes192EncryptSchedule : [192] -> AESEncryptKeySchedule AES192
aes192EncryptSchedule =
if aesniSupported
then \key -> aesniExpandEncrypt192 (split key)
else SB::aes192EncryptSchedule
/**
* Decryption key expansion for AES-192, for use in the "equivalent inverse cypher".
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes192DecryptSchedule : [192] -> AESDecryptKeySchedule AES192
aes192DecryptSchedule =
if aesniSupported
then \key -> aesniExpandDecrypt192 (split key)
else SB::aes192DecryptSchedule
/**
* Encryption and decryption key schedules for AES-192.
* If you will need both schedules, it is slightly more efficient
* to call this function than to compute the two schedules separately.
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes192Schedules : [192] -> (AESEncryptKeySchedule AES192, AESDecryptKeySchedule AES192)
aes192Schedules =
if aesniSupported
then \key -> aesniExpandEncryptDecrypt192 (split key)
else SB::aes192Schedules
/**
* Encryption key expansion for AES-256.
* See FIPS 197, section 5.2
*/
aes256EncryptSchedule : [256] -> AESEncryptKeySchedule AES256
aes256EncryptSchedule =
if aesniSupported
then \key -> aesniExpandEncrypt256 (split key)
else SB::aes256EncryptSchedule
/**
* Decryption key expansion for AES-256, for use in the "equivalent inverse cypher".
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes256DecryptSchedule : [256] -> AESDecryptKeySchedule AES256
aes256DecryptSchedule =
if aesniSupported
then \key -> aesniExpandDecrypt256 (split key)
else SB::aes256DecryptSchedule
/**
* Encryption and decryption key schedules for AES-256.
* If you will need both schedules, it is slightly more efficient
* to call this function than to compute the two schedules separately.
* See FIPS 197, sections 5.2 and 5.3.5.
*/
aes256Schedules : [256] -> (AESEncryptKeySchedule AES256, AESDecryptKeySchedule AES256)
aes256Schedules =
if aesniSupported
then \key -> aesniExpandEncryptDecrypt256 (split key)
else SB::aes256Schedules
/**
* AES block encryption algorithm.
* See FIPS 197, section 5.1.
*/
aesEncryptBlock : {k} (fin k) => AESEncryptKeySchedule k -> [128] -> [128]
aesEncryptBlock =
if aesniSupported
then \schedule plaintext -> join (aesniEncryptBlock schedule (split plaintext))
else SB::aesEncryptBlock
/**
* AES block decryption algorithm, via the "equivalent inverse cypher".
* See FIPS 197, section 5.3.5.
*/
aesDecryptBlock : {k} (fin k) => AESDecryptKeySchedule k -> [128] -> [128]
aesDecryptBlock =
if aesniSupported
then \schedule ciphertext -> join (aesniDecryptBlock schedule (split ciphertext))
else SB::aesDecryptBlock
private
foreign checkAESNISupported : () -> Bit
foreign aesniExpandEncrypt128 : [16][8] -> AESEncryptKeySchedule AES128
foreign aesniExpandDecrypt128 : [16][8] -> AESDecryptKeySchedule AES128
foreign aesniExpandEncryptDecrypt128 : [16][8]
-> (AESEncryptKeySchedule AES128, AESDecryptKeySchedule AES128)
foreign aesniExpandEncrypt192 : [24][8] -> AESEncryptKeySchedule AES192
foreign aesniExpandDecrypt192 : [24][8] -> AESDecryptKeySchedule AES192
foreign aesniExpandEncryptDecrypt192 : [24][8]
-> (AESEncryptKeySchedule AES192, AESDecryptKeySchedule AES192)
foreign aesniExpandEncrypt256 : [32][8] -> AESEncryptKeySchedule AES256
foreign aesniExpandDecrypt256 : [32][8] -> AESDecryptKeySchedule AES256
foreign aesniExpandEncryptDecrypt256 : [32][8]
-> (AESEncryptKeySchedule AES256, AESDecryptKeySchedule AES256)
foreign aesniEncryptBlock : {k} (fin k) => AESEncryptKeySchedule k -> [16][8] -> [16][8]
foreign aesniDecryptBlock : {k} (fin k) => AESDecryptKeySchedule k -> [16][8] -> [16][8]
aesniSupported = checkAESNISupported ()
/***** SHA2 *****/
/**
* The SHA-224 secure hash algorithm. See FIPS 180-4, section 6.3.
*/
sha224 = SB::sha224
/**
* The SHA-256 secure hash algorithm. See FIPS 180-4, section 6.2.2.
*/
sha256 = SB::sha256
/**
* The SHA-384 secure hash algorithm. See FIPS 180-4, section 6.5.
*/
sha384 = SB::sha384
/**
* The SHA-512 secure hash algorithm. See FIPS 180-4, section 6.4.
*/
sha512 = SB::sha512

View File

@ -0,0 +1,3 @@
import SuiteB_FFI as FFI
import SuiteB as SB
import Float

View File

@ -0,0 +1,30 @@
:l perf-bench.cry
:set fpBase=10
:! echo "AES-NI AES-128 key expansion:"
FFI::aes128EncryptSchedule 0x1234567890abcdef1234567890abcdef
:time FFI::aes128EncryptSchedule 0x1234567890abcdef1234567890abcdef
let ffiTime = it.avgCpuTime
:! echo "Cryptol AES-128 key expansion:"
SB::aes128EncryptSchedule 0x1234567890abcdef1234567890abcdef
:time SB::aes128EncryptSchedule 0x1234567890abcdef1234567890abcdef
let sbTime = it.avgCpuTime
:! echo "AES-128 key expansion speedup:"
fpDiv rne sbTime ffiTime
let s = SB::aes128EncryptSchedule 0x1234567890abcdef1234567890abcdef
:! echo "AES-NI AES-128 encrypt:"
FFI::aesEncryptBlock s 0x9876543210abcdef9876543210abcdef
:time FFI::aesEncryptBlock s 0x9876543210abcdef9876543210abcdef
let ffiTime = it.avgCpuTime
:! echo "Cryptol AES-128 encrypt:"
SB::aesEncryptBlock s 0x9876543210abcdef9876543210abcdef
:time SB::aesEncryptBlock s 0x9876543210abcdef9876543210abcdef
let sbTime = it.avgCpuTime
:! echo "AES-128 encrypt speedup:"
fpDiv rne sbTime ffiTime

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,2 @@
:l aes-mct-ecb.cry
:check

View File

@ -0,0 +1,24 @@
Loading module Cryptol
Loading module Cryptol
Loading module SuiteB
Loading module SuiteB_FFI
Loading dynamic library SuiteB_FFI.so
Loading module Main
property aes128_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.

View File

@ -0,0 +1,24 @@
Loading module Cryptol
Loading module Cryptol
Loading module SuiteB
Loading module SuiteB_FFI
Loading dynamic library SuiteB_FFI.dylib
Loading module Main
property aes128_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_MCT_vectors_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_MCT_vectors_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.

File diff suppressed because it is too large Load Diff

View File

@ -0,0 +1,2 @@
:l aes-vectors.cry
:check

View File

@ -0,0 +1,78 @@
Loading module Cryptol
Loading module Cryptol
Loading module SuiteB
Loading module SuiteB_FFI
Loading dynamic library SuiteB_FFI.so
Loading module Main
property aes128_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.

View File

@ -0,0 +1,78 @@
Loading module Cryptol
Loading module Cryptol
Loading module SuiteB
Loading module SuiteB_FFI
Loading dynamic library SuiteB_FFI.dylib
Loading module Main
property aes128_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_GFSBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_GFSBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_KeySBox_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_KeySBox_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarTxt_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarTxt_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes128_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes192_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarKey_encrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.
property aes256_VarKey_decrypt_correct Using exhaustive testing.
Testing... Passed 1 tests.
Q.E.D.

View File

@ -1,5 +1,6 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
-- | Errors from dynamic loading of shared libraries for FFI.
module Cryptol.Backend.FFI.Error where

View File

@ -421,10 +421,11 @@ data EvalError
| NoPrim Name -- ^ Primitive with no implementation
| BadRoundingMode Integer -- ^ Invalid rounding mode
| BadValue String -- ^ Value outside the domain of a partial function.
| NoMatchingPropGuardCase String -- ^ No prop guard holds for the given type variables.
| FFINotSupported Name -- ^ Foreign function cannot be called
| FFITypeNumTooBig Name TParam Integer -- ^ Number passed to foreign function
-- as a type argument is too large
deriving Typeable
deriving Typeable
instance PP EvalError where
ppPrec _ e = case e of
@ -443,6 +444,7 @@ instance PP EvalError where
BadRoundingMode r -> "invalid rounding mode" <+> integer r
BadValue x -> "invalid input for" <+> backticks (text x)
NoPrim x -> text "unimplemented primitive:" <+> pp x
NoMatchingPropGuardCase msg -> text $ "No matching constraint guard; " ++ msg
FFINotSupported x -> vcat
[ text "cannot call foreign function" <+> pp x
, text "FFI calls are not supported in this context"

View File

@ -15,6 +15,7 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE NamedFieldPuns #-}
module Cryptol.Eval (
moduleEnv
@ -35,6 +36,7 @@ module Cryptol.Eval (
, Unsupported(..)
, WordTooWide(..)
, forceValue
, checkProp
) where
import Cryptol.Backend
@ -63,6 +65,7 @@ import Data.Maybe
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map.Strict as Map
import Data.Semigroup
import Control.Applicative
import Prelude ()
import Prelude.Compat
@ -215,12 +218,52 @@ evalExpr sym env expr = case expr of
env' <- evalDecls sym ds env
evalExpr sym env' e
EPropGuards guards _ -> {-# SCC "evalExpr->EPropGuards" #-} do
let checkedGuards = [ e | (ps,e) <- guards, all (checkProp . evalProp env) ps ]
case checkedGuards of
(e:_) -> eval e
[] -> raiseError sym (NoMatchingPropGuardCase $ "Among constraint guards: " ++ show (fmap pp . fst <$> guards))
where
{-# INLINE eval #-}
eval = evalExpr sym env
ppV = ppValue sym defaultPPOpts
-- | Checks whether an evaluated `Prop` holds
checkProp :: Prop -> Bool
checkProp = \case
TCon tcon ts ->
let ns = toNat' <$> ts in
case tcon of
PC PEqual | [n1, n2] <- ns -> n1 == n2
PC PNeq | [n1, n2] <- ns -> n1 /= n2
PC PGeq | [n1, n2] <- ns -> n1 >= n2
PC PFin | [n] <- ns -> n /= Inf
-- TODO: instantiate UniqueFactorization for Nat'?
-- PC PPrime | [n] <- ns -> isJust (isPrime n)
PC PTrue -> True
_ -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ TCon tcon ts ]
prop -> evalPanic "evalProp" ["cannot use this as a guarding constraint: ", show . pp $ prop ]
where
toNat' :: Type -> Nat'
toNat' = \case
TCon (TC (TCNum n)) [] -> Nat n
TCon (TC TCInf) [] -> Inf
prop -> panic "checkProp" ["Expected `" ++ pretty prop ++ "` to be an evaluated numeric type"]
-- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables according
-- to `envTypes` and expanding all type synonyms via `tNoUser`.
evalProp :: GenEvalEnv sym -> Prop -> Prop
evalProp env@EvalEnv { envTypes } = \case
TCon tc tys -> TCon tc (toType . evalType envTypes <$> tys)
TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty
prop@TUser {} -> evalProp env (tNoUser prop)
TVar tv | Nothing <- lookupTypeVar tv envTypes -> panic "evalProp" ["Could not find type variable `" ++ pretty tv ++ "` in the type evaluation environment"]
prop -> panic "evalProp" ["Cannot use the following as a type constraint: `" ++ pretty prop ++ "`"]
where
toType = either tNumTy tValTy
-- | Capure the current call stack from the evaluation monad and
-- annotate function values. When arguments are later applied
@ -409,8 +452,10 @@ evalDecl ::
GenEvalEnv sym {- ^ An evaluation environment to extend with the given declaration -} ->
Decl {- ^ The declaration to evaluate -} ->
SEval sym (GenEvalEnv sym)
evalDecl sym renv env d =
let ?range = nameLoc (dName d) in
-- evalDecl sym renv env d =
-- let ?range = nameLoc (dName d) in
evalDecl sym renv env d = do
let ?range = nameLoc (dName d)
case dDefinition d of
DPrim ->
case ?evalPrim =<< asPrim (dName d) of

View File

@ -76,8 +76,8 @@ findForeignDecls = mapMaybe getForeign . mDecls
evalForeignDecls :: ForeignSrc -> [(Name, FFIFunType)] -> EvalEnv ->
Eval (Either [FFILoadError] EvalEnv)
evalForeignDecls fsrc decls env = io do
ePrims <- for decls \(name, ffiType) ->
fmap ((name,) . foreignPrimPoly name ffiType) <$>
ePrims <- for decls \(name, ffiFunType) ->
fmap ((name,) . foreignPrimPoly name ffiFunType) <$>
loadForeignImpl fsrc (unpackIdent $ nameIdent name)
pure case partitionEithers ePrims of
([], prims) -> Right $ foldr (uncurry bindVarDirect) env prims

View File

@ -0,0 +1,166 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeApplications #-}
-- | Generate C header files from foreign declarations.
module Cryptol.Eval.FFI.GenHeader
( generateForeignHeader
) where
import Control.Monad.Writer.Strict
import Data.Functor
import Data.Char(isAlphaNum)
import Data.List
import Data.Set (Set)
import qualified Data.Set as Set
import Language.C99.Pretty as C
import qualified Language.C99.Simple as C
import qualified Text.PrettyPrint as Pretty
import Cryptol.ModuleSystem.Name
import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.TypeCheck.Type
import Cryptol.Utils.Ident
import Cryptol.Utils.RecordMap
-- | @Include foo@ represents an include statement @#include <foo>@
newtype Include = Include String deriving (Eq, Ord)
-- | The monad for generating headers. We keep track of which headers we need to
-- include and add them to the output at the end.
type GenHeaderM = Writer (Set Include)
-- | Generate a C header file from the given foreign declarations.
generateForeignHeader :: [(Name, FFIFunType)] -> String
generateForeignHeader decls =
unlines (map renderInclude $ Set.toAscList incs)
++ Pretty.render (C.pretty $ C.translate (C.TransUnit cdecls []))
where (cdecls, incs) = runWriter $ traverse convertFun decls
renderInclude :: Include -> String
renderInclude (Include inc) = "#include <" ++ inc ++ ">"
-- | The "direction" of a parameter (input or output).
data ParamDir = In | Out
-- | The result of converting a Cryptol type into its C representation.
data ConvertResult
= Direct C.Type -- ^ A type that can be directly returned if it is a return
-- type and passed as a single parameter if it is a Cryptol
-- parameter type.
| Params [C.Param] -- ^ A type that is turned into a number of parameters,
-- for both Cryptol parameter and return type cases.
-- | Convert a Cryptol foreign declaration into a C function declaration.
convertFun :: (Name, FFIFunType) -> GenHeaderM C.Decln
convertFun (fName, FFIFunType {..}) = do
let tpIdent = fmap nameIdent . tpName
typeParams <- traverse convertTypeParam (pickNames (map tpIdent ffiTParams))
-- Name the input args in0, in1, etc
let inPrefixes =
case ffiArgTypes of
[_] -> ["in"]
_ -> ["in" ++ show @Integer i | i <- [0..]]
inParams <- convertMultiType In $ zip inPrefixes ffiArgTypes
(retType, outParams) <- convertType Out ffiRetType
<&> \case
Direct u -> (u, [])
-- Name the output arg out
Params ps -> (C.TypeSpec C.Void, map (prefixParam "out") ps)
-- Avoid possible name collisions
let params = snd $ mapAccumL renameParam Set.empty $
typeParams ++ inParams ++ outParams
renameParam names (C.Param u name) =
(Set.insert name' names, C.Param u name')
where name' = until (`Set.notMember` names) (++ "_") name
pure $ C.FunDecln Nothing retType (unpackIdent $ nameIdent fName) params
-- | Convert a Cryptol type parameter to a C value parameter.
convertTypeParam :: String -> GenHeaderM C.Param
convertTypeParam name = (`C.Param` name) <$> sizeT
-- | Convert a Cryptol parameter or return type to C.
convertType :: ParamDir -> FFIType -> GenHeaderM ConvertResult
convertType _ FFIBool = Direct <$> uint8T
convertType _ (FFIBasic t) = Direct <$> convertBasicType t
convertType _ (FFIArray _ t) = do
u <- convertBasicType t
pure $ Params [C.Param (C.Ptr u) ""]
convertType dir (FFITuple ts) = Params <$> convertMultiType dir
-- We name the tuple components using their indices
(zip (map (componentSuffix . show @Integer) [0..]) ts)
convertType dir (FFIRecord tMap) =
Params <$> convertMultiType dir (zip names ts)
where
(fs,ts) = unzip (displayFields tMap)
names = map componentSuffix (pickNames (map Just fs))
-- | Convert many Cryptol types, each associated with a prefix, to C parameters
-- named with their prefixes.
convertMultiType :: ParamDir -> [(C.Ident, FFIType)] -> GenHeaderM [C.Param]
convertMultiType dir = fmap concat . traverse \(prefix, t) ->
convertType dir t
<&> \case
Direct u -> [C.Param u' prefix]
where u' = case dir of
In -> u
-- Turn direct return types into pointer out parameters
Out -> C.Ptr u
Params ps -> map (prefixParam prefix) ps
-- | Convert a basic Cryptol FFI type to a C type.
convertBasicType :: FFIBasicType -> GenHeaderM C.Type
convertBasicType (FFIWord _ s) =
case s of
FFIWord8 -> uint8T
FFIWord16 -> uint16T
FFIWord32 -> uint32T
FFIWord64 -> uint64T
convertBasicType (FFIFloat _ _ s) =
case s of
FFIFloat32 -> pure $ C.TypeSpec C.Float
FFIFloat64 -> pure $ C.TypeSpec C.Double
prefixParam :: C.Ident -> C.Param -> C.Param
prefixParam pre (C.Param u name) = C.Param u (pre ++ name)
-- | Create a suffix corresponding to some component name of some larger type.
componentSuffix :: String -> C.Ident
componentSuffix = ('_' :)
sizeT, uint8T, uint16T, uint32T, uint64T :: GenHeaderM C.Type
sizeT = typedefFromInclude stddefH "size_t"
uint8T = typedefFromInclude stdintH "uint8_t"
uint16T = typedefFromInclude stdintH "uint16_t"
uint32T = typedefFromInclude stdintH "uint32_t"
uint64T = typedefFromInclude stdintH "uint64_t"
stddefH, stdintH :: Include
stddefH = Include "stddef.h"
stdintH = Include "stdint.h"
-- | Return a type with the given name, included from some header file.
typedefFromInclude :: Include -> C.Ident -> GenHeaderM C.Type
typedefFromInclude inc u = do
tell $ Set.singleton inc
pure $ C.TypeSpec $ C.TypedefName u
-- | Given some Cryptol identifiers (normal ones, not operators)
-- pick suitable unique C names for them
pickNames :: [Maybe Ident] -> [String]
pickNames xs = snd (mapAccumL add Set.empty xs)
where
add known x =
let y = simplify x
ys = y : [ y ++ show i | i <- [ 0 :: Int .. ] ]
y' : _ = dropWhile (`Set.member` known) ys
in (Set.insert y' known, y')
simplify x = case x of
Just i | let y = filter ok (unpackIdent i), not (null y) -> y
_ -> "zz"
ok x = x == '_' || isAlphaNum x

View File

@ -1452,12 +1452,12 @@ fromToV sym =
PNumPoly \first ->
PNumPoly \lst ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty in
case (first, lst) of
(Nat first', Nat lst') ->
let len = 1 + (lst' - first')
in VSeq len $ indexSeqMap $ \i -> f (first' + i)
in mkSeq sym (Nat len) ty $ indexSeqMap $ \i -> f (first' + i)
_ -> evalPanic "fromToV" ["invalid arguments"]
{-# INLINE fromThenToV #-}
@ -1469,12 +1469,12 @@ fromThenToV sym =
PNumPoly \lst ->
PTyPoly \ty ->
PNumPoly \len ->
PVal
PPrim
let !f = mkLit sym ty in
case (first, next, lst, len) of
(Nat first', Nat next', Nat _lst', Nat len') ->
let diff = next' - first'
in VSeq len' $ indexSeqMap $ \i -> f (first' + i*diff)
in mkSeq sym (Nat len') ty $ indexSeqMap $ \i -> f (first' + i*diff)
_ -> evalPanic "fromThenToV" ["invalid arguments"]
{-# INLINE fromToLessThanV #-}
@ -1484,12 +1484,12 @@ fromToLessThanV sym =
PFinPoly \first ->
PNumPoly \bound ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty
ss = indexSeqMap $ \i -> f (first + i)
in case bound of
Inf -> VStream ss
Nat bound' -> VSeq (bound' - first) ss
Inf -> return $ VStream ss
Nat bound' -> mkSeq sym (Nat (bound' - first)) ty ss
{-# INLINE fromToByV #-}
-- @[ 0 .. 10 by 2 ]@
@ -1499,10 +1499,10 @@ fromToByV sym =
PFinPoly \lst ->
PFinPoly \stride ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty
ss = indexSeqMap $ \i -> f (first + i*stride)
in VSeq (1 + ((lst - first) `div` stride)) ss
in mkSeq sym (Nat (1 + ((lst - first) `div` stride))) ty ss
{-# INLINE fromToByLessThanV #-}
-- @[ 0 .. <10 by 2 ]@
@ -1512,12 +1512,12 @@ fromToByLessThanV sym =
PNumPoly \bound ->
PFinPoly \stride ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty
ss = indexSeqMap $ \i -> f (first + i*stride)
in case bound of
Inf -> VStream ss
Nat bound' -> VSeq ((bound' - first + stride - 1) `div` stride) ss
Inf -> return $ VStream ss
Nat bound' -> mkSeq sym (Nat ((bound' - first + stride - 1) `div` stride)) ty ss
{-# INLINE fromToDownByV #-}
@ -1528,10 +1528,10 @@ fromToDownByV sym =
PFinPoly \lst ->
PFinPoly \stride ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty
ss = indexSeqMap $ \i -> f (first - i*stride)
in VSeq (1 + ((first - lst) `div` stride)) ss
in mkSeq sym (Nat (1 + ((first - lst) `div` stride))) ty ss
{-# INLINE fromToDownByGreaterThanV #-}
-- @[ 10 .. >0 down by 2 ]@
@ -1541,10 +1541,10 @@ fromToDownByGreaterThanV sym =
PFinPoly \bound ->
PFinPoly \stride ->
PTyPoly \ty ->
PVal
PPrim
let !f = mkLit sym ty
ss = indexSeqMap $ \i -> f (first - i*stride)
in VSeq ((first - bound + stride - 1) `div` stride) ss
in mkSeq sym (Nat ((first - bound + stride - 1) `div` stride)) ty ss
{-# INLINE infFromV #-}
infFromV :: Backend sym => sym -> Prim sym

View File

@ -10,6 +10,8 @@
> {-# LANGUAGE BlockArguments #-}
> {-# LANGUAGE PatternGuards #-}
> {-# LANGUAGE LambdaCase #-}
> {-# LANGUAGE NamedFieldPuns #-}
> {-# LANGUAGE ViewPatterns #-}
>
> module Cryptol.Eval.Reference
> ( Value(..)
@ -32,6 +34,7 @@
> import LibBF (BigFloat)
> import qualified LibBF as FP
> import qualified GHC.Num.Compat as Integer
> import qualified Data.List as List
>
> import Cryptol.ModuleSystem.Name (asPrim)
> import Cryptol.TypeCheck.Solver.InfNat (Nat'(..), nAdd, nMin, nMul)
@ -46,6 +49,8 @@
> import Cryptol.Utils.Panic (panic)
> import Cryptol.Utils.PP
> import Cryptol.Utils.RecordMap
> import Cryptol.Eval (checkProp)
> import Cryptol.Eval.Type (evalType, lookupTypeVar, tNumTy, tValTy)
>
> import qualified Cryptol.ModuleSystem as M
> import qualified Cryptol.ModuleSystem.Env as M (loadedModules,loadedNewtypes)
@ -332,11 +337,27 @@ assigns values to those variables.
> EProofAbs _ e -> evalExpr env e
> EProofApp e -> evalExpr env e
> EWhere e dgs -> evalExpr (foldl evalDeclGroup env dgs) e
>
> EPropGuards guards _ty ->
> case List.find (all (checkProp . evalProp env) . fst) guards of
> Just (_, e) -> evalExpr env e
> Nothing -> evalPanic "fromVBit" ["No guard constraint was satisfied"]
> appFun :: E Value -> E Value -> E Value
> appFun f v = f >>= \f' -> fromVFun f' v
> -- | Evaluates a `Prop` in an `EvalEnv` by substituting all variables
> -- according to `envTypes` and expanding all type synonyms via `tNoUser`.
> evalProp :: Env -> Prop -> Prop
> evalProp env@Env { envTypes } = \case
> TCon tc tys -> TCon tc (toType . evalType envTypes <$> tys)
> TVar tv | Just (toType -> ty) <- lookupTypeVar tv envTypes -> ty
> prop@TUser {} -> evalProp env (tNoUser prop)
> TVar tv | Nothing <- lookupTypeVar tv envTypes -> panic "evalProp" ["Could not find type variable `" ++ pretty tv ++ "` in the type evaluation environment"]
> prop -> panic "evalProp" ["Cannot use the following as a type constraint: `" ++ pretty prop ++ "`"]
> where
> toType = either tNumTy tValTy
Selectors
---------

View File

@ -28,7 +28,7 @@ import Control.DeepSeq
-- | An evaluated type of kind *.
-- These types do not contain type variables, type synonyms, or type functions.
data TValue
= TVBit -- ^ @ Bit @
= TVBit -- ^ @ Bit @
| TVInteger -- ^ @ Integer @
| TVFloat Integer Integer -- ^ @ Float e p @
| TVIntMod Integer -- ^ @ Z n @
@ -105,6 +105,7 @@ finNat' n' =
newtype TypeEnv =
TypeEnv
{ envTypeMap :: IntMap.IntMap (Either Nat' TValue) }
deriving (Show)
instance Monoid TypeEnv where
mempty = TypeEnv mempty

View File

@ -117,6 +117,7 @@ instance FreeVars Expr where
EProofAbs p e -> freeVars p <> freeVars e
EProofApp e -> freeVars e
EWhere e ds -> foldFree ds <> rmVals (defs ds) (freeVars e)
EPropGuards guards _ -> mconcat [ freeVars e | (_, e) <- guards ]
where
foldFree :: (FreeVars a, Defs a) => [a] -> Deps
foldFree = foldr updateFree mempty

View File

@ -18,6 +18,7 @@ module Cryptol.ModuleSystem (
, findModule
, loadModuleByPath
, loadModuleByName
, checkModuleByPath
, checkExpr
, evalExpr
, benchmarkExpr
@ -70,9 +71,9 @@ loadModuleByPath path minp = do
moduleEnv' <- resetModuleEnv $ minpModuleEnv minp
runModuleM minp{ minpModuleEnv = moduleEnv' } $ do
unloadModule ((InFile path ==) . lmFilePath)
m <- Base.loadModuleByPath path
(mPath, m) <- Base.loadModuleByPath True path
setFocusedModule (T.mName m)
return (InFile path,m)
return (mPath,m)
-- | Load the given parsed module.
loadModuleByName :: P.ModName -> ModuleCmd (ModulePath,T.Module)
@ -84,6 +85,13 @@ loadModuleByName n minp = do
setFocusedModule (T.mName m')
return (path,m')
-- | Parse and typecheck a module, but don't evaluate or change the environment.
checkModuleByPath :: FilePath -> ModuleCmd (ModulePath, T.Module)
checkModuleByPath path minp = do
(res, warns) <- runModuleM minp $ Base.loadModuleByPath False path
-- restore the old environment
pure (fmap (minpModuleEnv minp <$) res, warns)
-- Extended Environments -------------------------------------------------------
-- These functions are particularly useful for interactive modes, as

View File

@ -61,6 +61,8 @@ import qualified Cryptol.Parser as P
import qualified Cryptol.Parser.Unlit as P
import Cryptol.Parser.AST as P
import Cryptol.Parser.NoPat (RemovePatterns(removePatterns))
import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards
( expandPropGuards, runExpandPropGuardsM )
import Cryptol.Parser.NoInclude (removeIncludesModule)
import Cryptol.Parser.Position (HasLoc(..), Range, emptyRange)
import qualified Cryptol.TypeCheck as T
@ -118,6 +120,14 @@ noPat a = do
unless (null errs) (noPatErrors errs)
return a'
-- ExpandPropGuards ------------------------------------------------------------
-- | Run the expandPropGuards pass.
expandPropGuards :: Module PName -> ModuleM (Module PName)
expandPropGuards a =
case ExpandPropGuards.runExpandPropGuardsM $ ExpandPropGuards.expandPropGuards a of
Left err -> expandPropGuardsError err
Right a' -> pure a'
-- Parsing ---------------------------------------------------------------------
@ -180,8 +190,9 @@ parseModule path = do
-- Modules ---------------------------------------------------------------------
-- | Load a module by its path.
loadModuleByPath :: FilePath -> ModuleM T.Module
loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
loadModuleByPath :: Bool {- ^ evaluate declarations in the module -} ->
FilePath -> ModuleM (ModulePath, T.Module)
loadModuleByPath eval path = withPrependedSearchPath [ takeDirectory path ] $ do
let fileName = takeFileName path
foundPath <- findFile fileName
(fp, pm) <- parseModule (InFile foundPath)
@ -195,9 +206,11 @@ loadModuleByPath path = withPrependedSearchPath [ takeDirectory path ] $ do
case lookupModule n env of
-- loadModule will calculate the canonical path again
Nothing -> doLoadModule False (FromModule n) (InFile foundPath) fp pm
Nothing -> do
m <- doLoadModule eval False (FromModule n) (InFile foundPath) fp pm
pure (InFile foundPath, m)
Just lm
| path' == loaded -> return (lmModule lm)
| path' == loaded -> return (lmFilePath lm, lmModule lm)
| otherwise -> duplicateModuleName n path' loaded
where loaded = lmModuleId lm
@ -213,18 +226,19 @@ loadModuleFrom quiet isrc =
do path <- findModule n
errorInFile path $
do (fp, pm) <- parseModule path
m <- doLoadModule quiet isrc path fp pm
m <- doLoadModule True quiet isrc path fp pm
return (path,m)
-- | Load dependencies, typecheck, and add to the eval environment.
doLoadModule ::
Bool {- ^ evaluate declarations in the module -} ->
Bool {- ^ quiet mode: true suppresses the "loading module" message -} ->
ImportSource ->
ModulePath ->
Fingerprint ->
P.Module PName ->
ModuleM T.Module
doLoadModule quiet isrc path fp pm0 =
doLoadModule eval quiet isrc path fp pm0 =
loading isrc $
do let pm = addPrelude pm0
loadDeps pm
@ -241,10 +255,9 @@ doLoadModule quiet isrc path fp pm0 =
let ?evalPrim = \i -> Right <$> Map.lookup i tbl
callStacks <- getCallStacks
let ?callStacks = callStacks
foreignSrc <- if T.isParametrizedModule tcm
then pure Nothing
else evalForeign tcm
unless (T.isParametrizedModule tcm) $
let shouldEval = eval && not (T.isParametrizedModule tcm)
foreignSrc <- if shouldEval then evalForeign tcm else pure Nothing
when shouldEval $
modifyEvalEnv (E.moduleEnv Concrete tcm)
loadedModule path fp nameEnv foreignSrc tcm
@ -468,8 +481,11 @@ checkSingleModule how isrc m = do
-- remove pattern bindings
npm <- noPat m
-- run expandPropGuards
epgm <- expandPropGuards npm
-- rename everything
renMod <- renameModule npm
renMod <- renameModule epgm
-- when generating the prim map for the typechecker, if we're checking the
-- prelude, we have to generate the map from the renaming environment, as we

View File

@ -1,4 +1,5 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
module Cryptol.ModuleSystem.Exports where
import Data.Set(Set)

View File

@ -217,6 +217,10 @@ instance Inst Expr where
EProofApp e -> EProofApp (go e)
EWhere e ds -> EWhere (go e) (inst env ds)
-- TODO: this doesn't exist in the new module system, so it will have to
-- be implemented differently there anyway
EPropGuards _guards _ty -> panic "inst" ["This is not implemented for EPropGuards yet."]
instance Inst DeclGroup where
inst env dg =

View File

@ -11,6 +11,7 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE Safe #-}
module Cryptol.ModuleSystem.Interface (
Iface
, IfaceG(..)

View File

@ -29,6 +29,7 @@ import qualified Cryptol.Parser.AST as P
import Cryptol.Parser.Position (Located)
import Cryptol.Utils.Panic (panic)
import qualified Cryptol.Parser.NoPat as NoPat
import qualified Cryptol.Parser.ExpandPropGuards as ExpandPropGuards
import qualified Cryptol.Parser.NoInclude as NoInc
import qualified Cryptol.TypeCheck as T
import qualified Cryptol.TypeCheck.AST as T
@ -102,6 +103,8 @@ data ModuleError
-- ^ Problems during the renaming phase
| NoPatErrors ImportSource [NoPat.Error]
-- ^ Problems during the NoPat phase
| ExpandPropGuardsError ImportSource ExpandPropGuards.Error
-- ^ Problems during the ExpandPropGuards phase
| NoIncludeErrors ImportSource [NoInc.IncludeError]
-- ^ Problems during the NoInclude phase
| TypeCheckingFailed ImportSource T.NameMap [(Range,T.Error)]
@ -137,6 +140,7 @@ instance NFData ModuleError where
RecursiveModules mods -> mods `deepseq` ()
RenamerErrors src errs -> src `deepseq` errs `deepseq` ()
NoPatErrors src errs -> src `deepseq` errs `deepseq` ()
ExpandPropGuardsError src err -> src `deepseq` err `deepseq` ()
NoIncludeErrors src errs -> src `deepseq` errs `deepseq` ()
TypeCheckingFailed nm src errs -> nm `deepseq` src `deepseq` errs `deepseq` ()
ModuleNameMismatch expected found ->
@ -185,6 +189,8 @@ instance PP ModuleError where
NoPatErrors _src errs -> vcat (map pp errs)
ExpandPropGuardsError _src err -> pp err
NoIncludeErrors _src errs -> vcat (map NoInc.ppIncludeError errs)
TypeCheckingFailed _src nm errs -> vcat (map (T.ppNamedError nm) errs)
@ -250,6 +256,11 @@ noPatErrors errs = do
src <- getImportSource
ModuleT (raise (NoPatErrors src errs))
expandPropGuardsError :: ExpandPropGuards.Error -> ModuleM a
expandPropGuardsError err = do
src <- getImportSource
ModuleT (raise (ExpandPropGuardsError src err))
noIncludeErrors :: [NoInc.IncludeError] -> ModuleM a
noIncludeErrors errs = do
src <- getImportSource

View File

@ -685,6 +685,11 @@ instance Rename BindDef where
rename DPrim = return DPrim
rename DForeign = return DForeign
rename (DExpr e) = DExpr <$> rename e
rename (DPropGuards cases) = DPropGuards <$> traverse rename cases
instance Rename PropGuardCase where
rename g = PropGuardCase <$> traverse (rnLocated rename) (pgcProps g)
<*> rename (pgcExpr g)
-- NOTE: this only renames types within the pattern.
instance Rename Pattern where

View File

@ -276,7 +276,7 @@ prim_bind :: { [TopDecl PName] }
| mbDoc 'primitive' 'type' schema ':' kind {% mkPrimTypeDecl $1 $4 $6 }
foreign_bind :: { [TopDecl PName] }
: mbDoc 'foreign' name ':' schema { mkForeignDecl $1 $3 $5 }
: mbDoc 'foreign' name ':' schema {% mkForeignDecl $1 $3 $5 }
parameter_decls :: { [TopDecl PName] }
: 'parameter' 'v{' par_decls 'v}' { reverse $3 }
@ -302,11 +302,14 @@ mbDoc :: { Maybe (Located Text) }
: doc { Just $1 }
| {- empty -} { Nothing }
decl :: { Decl PName }
: vars_comma ':' schema { at (head $1,$3) $ DSignature (reverse $1) $3 }
| ipat '=' expr { at ($1,$3) $ DPatBind $1 $3 }
| '(' op ')' '=' expr { at ($1,$5) $ DPatBind (PVar $2) $5 }
| var apats_indices propguards_cases
{% mkPropGuardsDecl $1 $2 $3 }
| var propguards_cases
{% mkConstantPropGuardsDecl $1 $2 }
| var apats_indices '=' expr
{ at ($1,$4) $ mkIndexedDecl $1 $2 $4 }
@ -385,6 +388,19 @@ let_decl :: { Decl PName }
| 'infix' NUM ops {% mkFixity NonAssoc $2 (reverse $3) }
propguards_cases :: { [PropGuardCase PName] }
: propguards_cases propguards_case { $2 : $1 }
| propguards_case { [$1] }
propguards_case :: { PropGuardCase PName }
: '|' propguards_quals '=>' expr { PropGuardCase $2 $4 }
propguards_quals :: { [Located (Prop PName)] }
: type {% mkPropGuards $1 }
newtype :: { Newtype PName }
: 'newtype' qname '=' newtype_body
{ Newtype $2 [] (thing $4) }

View File

@ -16,6 +16,7 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE FlexibleInstances #-}
module Cryptol.Parser.AST
( -- * Names
Ident, mkIdent, mkInfix, isInfixIdent, nullIdent, identText
@ -59,6 +60,7 @@ module Cryptol.Parser.AST
, ParameterType(..)
, ParameterFun(..)
, NestedModule(..)
, PropGuardCase(..)
-- * Interactive
, ReplInput(..)
@ -76,6 +78,7 @@ module Cryptol.Parser.AST
, emptyFunDesc
, PrefixOp(..)
, prefixFixity
, asEApps
-- * Positions
, Located(..)
@ -280,8 +283,15 @@ type LBindDef = Located (BindDef PName)
data BindDef name = DPrim
| DForeign
| DExpr (Expr name)
| DPropGuards [PropGuardCase name]
deriving (Eq, Show, Generic, NFData, Functor)
data PropGuardCase name = PropGuardCase
{ pgcProps :: [Located (Prop name)]
, pgcExpr :: Expr name
}
deriving (Eq,Generic,NFData,Functor,Show)
data Pragma = PragmaNote String
| PragmaProperty
deriving (Eq, Show, Generic, NFData)
@ -728,6 +738,7 @@ instance (Show name, PPName name) => PP (BindDef name) where
ppPrec _ DPrim = text "<primitive>"
ppPrec _ DForeign = text "<foreign>"
ppPrec p (DExpr e) = ppPrec p e
ppPrec _p (DPropGuards _guards) = text "propguards"
instance PPName name => PP (TySyn name) where
@ -991,6 +1002,8 @@ instance PPName name => PP (Type name) where
instance PPName name => PP (Prop name) where
ppPrec n (CType t) = ppPrec n t
instance PPName name => PP [Prop name] where
ppPrec n props = parens . commaSep . fmap (ppPrec n) $ props
--------------------------------------------------------------------------------
-- Drop all position information, so equality reflects program structure

View File

@ -0,0 +1,130 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
-- |
-- Module : Cryptol.Parser.PropGuards
-- Copyright : (c) 2022 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
--
-- Expands PropGuards into a top-level definition for each case, and rewrites
-- the body of each case to be an appropriate call to the respectively generated
-- function.
module Cryptol.Parser.ExpandPropGuards where
import Control.DeepSeq
import Cryptol.Parser.AST
import Cryptol.Utils.PP
import Cryptol.Utils.Panic (panic)
import Data.Text (pack)
import GHC.Generics (Generic)
-- | Monad
type ExpandPropGuardsM a = Either Error a
runExpandPropGuardsM :: ExpandPropGuardsM a -> Either Error a
runExpandPropGuardsM m = m
-- | Error
data Error = NoSignature (Located PName)
deriving (Show, Generic, NFData)
instance PP Error where
ppPrec _ err = case err of
NoSignature x ->
text "At" <+> pp (srcRange x) <.> colon
<+> text "Declarations using constraint guards require an explicit type signature."
expandPropGuards :: ModuleG m PName -> ExpandPropGuardsM (ModuleG m PName)
expandPropGuards m =
do mDecls' <- mapM expandTopDecl (mDecls m)
pure m {mDecls = concat mDecls' }
expandTopDecl :: TopDecl PName -> ExpandPropGuardsM [TopDecl PName]
expandTopDecl topDecl =
case topDecl of
Decl topLevelDecl ->
do ds <- expandDecl (tlValue topLevelDecl)
pure [ Decl topLevelDecl { tlValue = d } | d <- ds ]
DModule tl | NestedModule m <- tlValue tl ->
do m1 <- expandPropGuards m
pure [DModule tl { tlValue = NestedModule m1 }]
_ -> pure [topDecl]
expandDecl :: Decl PName -> ExpandPropGuardsM [Decl PName]
expandDecl decl =
case decl of
DBind bind -> do bs <- expandBind bind
pure (map DBind bs)
_ -> pure [decl]
expandBind :: Bind PName -> ExpandPropGuardsM [Bind PName]
expandBind bind =
case thing (bDef bind) of
DPropGuards guards -> do
Forall params props t rng <-
case bSignature bind of
Just schema -> pure schema
Nothing -> Left . NoSignature $ bName bind
let goGuard ::
PropGuardCase PName ->
ExpandPropGuardsM (PropGuardCase PName, Bind PName)
goGuard (PropGuardCase props' e) = do
bName' <- newName (bName bind) (thing <$> props')
-- call to generated function
tParams <- case bSignature bind of
Just (Forall tps _ _ _) -> pure tps
Nothing -> Left $ NoSignature (bName bind)
typeInsts <-
(\(TParam n _ _) -> Right . PosInst $ TUser n [])
`traverse` tParams
let e' = foldl EApp (EAppT (EVar $ thing bName') typeInsts) (patternToExpr <$> bParams bind)
pure
( PropGuardCase props' e',
bind
{ bName = bName',
-- include guarded props in signature
bSignature = Just (Forall params
(props <> map thing props')
t rng),
-- keeps same location at original bind
-- i.e. "on top of" original bind
bDef = (bDef bind) {thing = DExpr e}
}
)
(guards', binds') <- unzip <$> mapM goGuard guards
pure $
bind {bDef = DPropGuards guards' <$ bDef bind} :
binds'
_ -> pure [bind]
patternToExpr :: Pattern PName -> Expr PName
patternToExpr (PVar locName) = EVar (thing locName)
patternToExpr _ =
panic "patternToExpr"
["Unimplemented: patternToExpr of anything other than PVar"]
newName :: Located PName -> [Prop PName] -> ExpandPropGuardsM (Located PName)
newName locName props =
pure case thing locName of
Qual modName ident ->
let txt = identText ident
txt' = pack $ show $ pp props
in Qual modName (mkIdent $ txt <> txt') <$ locName
UnQual ident ->
let txt = identText ident
txt' = pack $ show $ pp props
in UnQual (mkIdent $ txt <> txt') <$ locName
NewName _ _ ->
panic "mkName"
[ "During expanding prop guards"
, "tried to make new name from NewName case of PName"
]

View File

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
module Cryptol.Parser.Name where
@ -33,6 +34,7 @@ data PName = UnQual !Ident
-- | Passes that can generate fresh names.
data Pass = NoPat
| MonoValues
| ExpandPropGuards String
deriving (Eq,Ord,Show,Generic)
instance NFData PName
@ -54,8 +56,9 @@ getIdent (Qual _ n) = n
getIdent (NewName p i) = packIdent ("__" ++ pass ++ show i)
where
pass = case p of
NoPat -> "p"
MonoValues -> "mv"
NoPat -> "p"
MonoValues -> "mv"
ExpandPropGuards _ -> "epg"
isGeneratedName :: PName -> Bool
isGeneratedName x =

View File

@ -9,6 +9,8 @@
-- This module defines the scoping rules for value- and type-level
-- names in Cryptol.
{-# LANGUAGE Safe #-}
module Cryptol.Parser.Names
( tnamesNT
, tnamesT
@ -65,6 +67,7 @@ namesDef :: Ord name => BindDef name -> Set name
namesDef DPrim = Set.empty
namesDef DForeign = Set.empty
namesDef (DExpr e) = namesE e
namesDef (DPropGuards guards) = Set.unions (map (namesE . pgcExpr) guards)
-- | The names used by an expression.
@ -186,6 +189,11 @@ tnamesDef :: Ord name => BindDef name -> Set name
tnamesDef DPrim = Set.empty
tnamesDef DForeign = Set.empty
tnamesDef (DExpr e) = tnamesE e
tnamesDef (DPropGuards guards) = Set.unions (map tnamesPropGuardCase guards)
tnamesPropGuardCase :: Ord name => PropGuardCase name -> Set name
tnamesPropGuardCase c =
Set.unions (tnamesE (pgcExpr c) : map (tnamesC . thing) (pgcProps c))
-- | The type names used by an expression.
tnamesE :: Ord name => Expr name -> Set name

View File

@ -228,6 +228,20 @@ noMatchB b =
do e' <- noPatFun (Just (thing (bName b))) 0 (bParams b) e
return b { bParams = [], bDef = DExpr e' <$ bDef b }
DPropGuards guards ->
do let nm = thing (bName b)
ps = bParams b
gs <- mapM (noPatPropGuardCase nm ps) guards
pure b { bParams = [], bDef = DPropGuards gs <$ bDef b }
noPatPropGuardCase ::
PName ->
[Pattern PName] ->
PropGuardCase PName -> NoPatM (PropGuardCase PName)
noPatPropGuardCase f xs pc =
do e <- noPatFun (Just f) 0 xs (pgcExpr pc)
pure pc { pgcExpr = e }
noMatchD :: Decl PName -> NoPatM [Decl PName]
noMatchD decl =
case decl of

View File

@ -17,6 +17,7 @@
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.Parser.ParserUtils where
import Data.Char(isAlphaNum)
import Data.Maybe(fromMaybe)
import Data.Bits(testBit,setBit)
import Data.List.NonEmpty ( NonEmpty(..) )
@ -40,7 +41,7 @@ import Cryptol.Parser.Lexer
import Cryptol.Parser.Token(SelectorType(..))
import Cryptol.Parser.Position
import Cryptol.Parser.Utils (translateExprToNumT,widthIdent)
import Cryptol.Utils.Ident(packModName,packIdent,modNameChunks)
import Cryptol.Utils.Ident(packModName,packIdent,modNameChunks,unpackIdent)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic
import Cryptol.Utils.RecordMap
@ -609,6 +610,35 @@ mkIndexedDecl f (ps, ixs) e =
rhs :: Expr PName
rhs = mkGenerate (reverse ixs) e
-- NOTE: The lists of patterns are reversed!
mkPropGuardsDecl ::
LPName ->
([Pattern PName], [Pattern PName]) ->
[PropGuardCase PName] ->
ParseM (Decl PName)
mkPropGuardsDecl f (ps, ixs) guards =
do unless (null ixs) $
errorMessage (srcRange f)
["Indexed sequence definitions may not use constraint guards"]
let gs = reverse guards
pure $
DBind Bind { bName = f
, bParams = reverse ps
, bDef = Located (srcRange f) (DPropGuards gs)
, bSignature = Nothing
, bPragmas = []
, bMono = False
, bInfix = False
, bFixity = Nothing
, bDoc = Nothing
, bExport = Public
}
mkConstantPropGuardsDecl ::
LPName -> [PropGuardCase PName] -> ParseM (Decl PName)
mkConstantPropGuardsDecl f guards =
mkPropGuardsDecl f ([],[]) guards
-- NOTE: The lists of patterns are reversed!
mkIndexedExpr :: ([Pattern PName], [Pattern PName]) -> Expr PName -> Expr PName
mkIndexedExpr (ps, ixs) body
@ -627,8 +657,18 @@ mkIf ifThens theElse = foldr addIfThen theElse ifThens
mkPrimDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
mkPrimDecl = mkNoImplDecl DPrim
mkForeignDecl :: Maybe (Located Text) -> LPName -> Schema PName -> [TopDecl PName]
mkForeignDecl = mkNoImplDecl DForeign
mkForeignDecl ::
Maybe (Located Text) -> LPName -> Schema PName -> ParseM [TopDecl PName]
mkForeignDecl mbDoc nm ty =
do let txt = unpackIdent (getIdent (thing nm))
unless (all isOk txt)
(errorMessage (srcRange nm)
[ "`" ++ txt ++ "` is not a valid foreign name."
, "The name should contain only alpha-numeric characters or '_'."
])
pure (mkNoImplDecl DForeign mbDoc nm ty)
where
isOk c = c == '_' || isAlphaNum c
-- | Generate a signature and a binding for value declarations with no
-- implementation (i.e. primitive or foreign declarations). The reason for
@ -768,6 +808,10 @@ distrLoc :: Located [a] -> [Located a]
distrLoc x = [ Located { srcRange = r, thing = a } | a <- thing x ]
where r = srcRange x
mkPropGuards :: Type PName -> ParseM [Located (Prop PName)]
mkPropGuards ty =
do lp <- mkProp ty
pure [ lp { thing = p } | p <- thing lp ]
mkProp :: Type PName -> ParseM (Located [Prop PName])
mkProp ty =

View File

@ -1,5 +1,6 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
module Cryptol.Parser.Token where
import Data.Text(Text)

View File

@ -10,6 +10,7 @@
-- from previous Cryptol versions.
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
module Cryptol.Parser.Utils
( translateExprToNumT

View File

@ -74,6 +74,8 @@ import qualified Cryptol.Backend.SeqMap as E
import Cryptol.Eval.Concrete( Concrete(..) )
import qualified Cryptol.Eval.Concrete as Concrete
import qualified Cryptol.Eval.Env as E
import Cryptol.Eval.FFI
import Cryptol.Eval.FFI.GenHeader
import qualified Cryptol.Eval.Type as E
import qualified Cryptol.Eval.Value as E
import qualified Cryptol.Eval.Reference as R
@ -119,7 +121,7 @@ import System.Environment (lookupEnv)
import System.Exit (ExitCode(ExitSuccess))
import System.Process (shell,createProcess,waitForProcess)
import qualified System.Process as Process(runCommand)
import System.FilePath((</>), isPathSeparator)
import System.FilePath((</>), (-<.>), isPathSeparator)
import System.Directory(getHomeDirectory,setCurrentDirectory,doesDirectoryExist
,getTemporaryDirectory,setPermissions,removeFile
,emptyPermissions,setOwnerReadable)
@ -309,6 +311,12 @@ commandList =
, "number of tests is determined by the \"tests\" option."
])
""
, CommandDescr [ ":generate-foreign-header" ] ["FILE"] (FilenameArg genHeaderCmd)
"Generate a C header file from foreign declarations in a Cryptol file."
(unlines
[ "Converts all foreign declarations in the given Cryptol file into C"
, "function declarations, and writes them to a file with the same name"
, "but with a .h extension." ])
]
genHelp :: [CommandDescr] -> [String]
@ -1222,6 +1230,23 @@ loadHelper how =
M.InMem {} -> clearEditPath
setDynEnv mempty
genHeaderCmd :: FilePath -> REPL ()
genHeaderCmd path
| null path = pure ()
| otherwise = do
(mPath, m) <- liftModuleCmd $ M.checkModuleByPath path
let decls = findForeignDecls m
if null decls
then rPutStrLn $ "No foreign declarations in " ++ pretty mPath
else do
let header = generateForeignHeader decls
case mPath of
M.InFile p -> do
let hPath = p -<.> "h"
rPutStrLn $ "Writing header to " ++ hPath
replWriteFileString hPath header (rPutStrLn . show)
M.InMem _ _ -> rPutStrLn header
versionCmd :: REPL ()
versionCmd = displayVersion rPutStrLn
@ -1536,23 +1561,16 @@ liftModuleCmd cmd =
}
moduleCmdResult =<< io (cmd minp)
-- TODO: add filter for my exhaustie prop guards warning here
moduleCmdResult :: M.ModuleRes a -> REPL a
moduleCmdResult (res,ws0) = do
warnDefaulting <- getKnownUser "warnDefaulting"
warnShadowing <- getKnownUser "warnShadowing"
warnPrefixAssoc <- getKnownUser "warnPrefixAssoc"
warnNonExhConGrds <- getKnownUser "warnNonExhaustiveConstraintGuards"
-- XXX: let's generalize this pattern
let isDefaultWarn (T.DefaultingTo _ _) = True
isDefaultWarn _ = False
filterDefaults w | warnDefaulting = Just w
filterDefaults (M.TypeCheckWarnings nameMap xs) =
case filter (not . isDefaultWarn . snd) xs of
[] -> Nothing
ys -> Just (M.TypeCheckWarnings nameMap ys)
filterDefaults w = Just w
isShadowWarn (M.SymbolShadowed {}) = True
let isShadowWarn (M.SymbolShadowed {}) = True
isShadowWarn _ = False
isPrefixAssocWarn (M.PrefixAssocChanged {}) = True
@ -1565,9 +1583,23 @@ moduleCmdResult (res,ws0) = do
ys -> Just (M.RenamerWarnings ys)
filterRenamer _ _ w = Just w
let ws = mapMaybe filterDefaults
. mapMaybe (filterRenamer warnShadowing isShadowWarn)
-- ignore certain warnings during typechecking
filterTypecheck :: M.ModuleWarning -> Maybe M.ModuleWarning
filterTypecheck (M.TypeCheckWarnings nameMap xs) =
case filter (allow . snd) xs of
[] -> Nothing
ys -> Just (M.TypeCheckWarnings nameMap ys)
where
allow :: T.Warning -> Bool
allow = \case
T.DefaultingTo _ _ | not warnDefaulting -> False
T.NonExhaustivePropGuards _ | not warnNonExhConGrds -> False
_ -> True
filterTypecheck w = Just w
let ws = mapMaybe (filterRenamer warnShadowing isShadowWarn)
. mapMaybe (filterRenamer warnPrefixAssoc isPrefixAssocWarn)
. mapMaybe filterTypecheck
$ ws0
names <- M.mctxNameDisp <$> getFocusedEnv
mapM_ (rPrint . runDoc names . pp) ws
@ -1669,8 +1701,15 @@ itIdent :: M.Ident
itIdent = M.packIdent "it"
replWriteFile :: FilePath -> BS.ByteString -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFile fp bytes handler =
do x <- io $ X.catch (BS.writeFile fp bytes >> return Nothing) (return . Just)
replWriteFile = replWriteFileWith BS.writeFile
replWriteFileString :: FilePath -> String -> (X.SomeException -> REPL ()) -> REPL ()
replWriteFileString = replWriteFileWith writeFile
replWriteFileWith :: (FilePath -> a -> IO ()) -> FilePath -> a ->
(X.SomeException -> REPL ()) -> REPL ()
replWriteFileWith write fp contents handler =
do x <- io $ X.catch (write fp contents >> return Nothing) (return . Just)
maybe (return ()) handler x
replReadFile :: FilePath -> (X.SomeException -> REPL (Maybe BS.ByteString)) -> REPL (Maybe BS.ByteString)

View File

@ -902,6 +902,8 @@ userOptions = mkOptionMap
"Choose whether to display warnings when expression association has changed due to new prefix operator fixities."
, simpleOpt "warnUninterp" ["warn-uninterp"] (EnvBool True) noCheck
"Choose whether to issue a warning when uninterpreted functions are used to implement primitives in the symbolic simulator."
, simpleOpt "warnNonExhaustiveConstraintGuards" ["warn-nonexhaustive-constraintguards"] (EnvBool True) noCheck
"Choose whether to issue a warning when a use of constraint guards is not determined to be exhaustive."
, simpleOpt "smtFile" ["smt-file"] (EnvString "-") noCheck
"The file to use for SMT-Lib scripts (for debugging or offline proving).\nUse \"-\" for stdout."
, OptionDescr "path" [] (EnvString "") noCheck

View File

@ -17,6 +17,7 @@ import Cryptol.ModuleSystem.Name(toParamInstName,asParamName,nameIdent
,paramModRecParam)
import Cryptol.Utils.Ident(paramInstModName)
import Cryptol.Utils.RecordMap(recordFromFields)
import Data.Bifunctor (Bifunctor(second))
{-
Note that we have to be careful when doing this transformation on
@ -258,6 +259,7 @@ instance Inst Expr where
_ -> EProofApp (inst ps e1)
EWhere e dgs -> EWhere (inst ps e) (inst ps dgs)
EPropGuards guards ty -> EPropGuards (second (inst ps) <$> guards) ty
instance Inst Match where

View File

@ -201,6 +201,8 @@ rewE rews = go
EWhere e dgs -> EWhere <$> go e <*> inLocal
(mapM (rewDeclGroup rews) dgs)
EPropGuards guards ty -> EPropGuards <$> (\(props, e) -> (,) <$> pure props <*> go e) `traverse` guards <*> pure ty
rewM :: RewMap -> Match -> M Match
rewM rews ma =

View File

@ -19,12 +19,16 @@ import qualified Cryptol.ModuleSystem as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.ModuleSystem.Monad as M
import Cryptol.ModuleSystem.Name
import Cryptol.Eval (checkProp)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (catMaybes)
import qualified Data.List as List
import MonadLib hiding (mapM)
import Cryptol.ModuleSystem.Base (getPrimMap)
-- Specializer Monad -----------------------------------------------------------
@ -102,6 +106,16 @@ specializeExpr expr =
EProofAbs p e -> EProofAbs p <$> specializeExpr e
EProofApp {} -> specializeConst expr
EWhere e dgs -> specializeEWhere e dgs
-- The type should be monomorphic, and the guarded expressions should
-- already be normalized, so we just need to choose the first expression
-- that's true.
EPropGuards guards ty ->
case List.find (all checkProp . fst) guards of
Just (_, e) -> specializeExpr e
Nothing -> do
pm <- liftSpecT getPrimMap
pure $ eError pm ty "no constraint guard was satisfied"
specializeMatch :: Match -> SpecM Match
specializeMatch (From qn l t e) = From qn l t <$> specializeExpr e

View File

@ -150,6 +150,8 @@ data Expr = EList [Expr] Type -- ^ List value (with type of elements)
| EWhere Expr [DeclGroup]
| EPropGuards [([Prop], Expr)] Type
deriving (Show, Generic, NFData)
@ -268,6 +270,12 @@ instance PP (WithNames Expr) where
, hang "where" 2 (vcat (map ppW ds))
]
EPropGuards guards _ ->
parens (text "propguards" <+> vsep (ppGuard <$> guards))
where ppGuard (props, e) = indent 1
$ pipe <+> commaSep (ppW <$> props)
<+> text "=>" <+> ppW e
where
ppW x = ppWithNames nm x
ppWP x = ppWithNamesPrec nm x

View File

@ -1,3 +1,5 @@
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Default where
import qualified Data.Set as Set

View File

@ -68,6 +68,7 @@ subsumes _ _ = False
data Warning = DefaultingKind (P.TParam Name) P.Kind
| DefaultingWildType P.Kind
| DefaultingTo !TVarInfo Type
| NonExhaustivePropGuards Name
deriving (Show, Generic, NFData)
-- | Various errors that might happen during type checking/inference
@ -151,6 +152,16 @@ data Error = KindMismatch (Maybe TypeSource) Kind Kind
| UnsupportedFFIType TypeSource FFITypeError
-- ^ Type is not supported for FFI
| NestedConstraintGuard Ident
-- ^ Constraint guards may only apper at the top-level
| DeclarationRequiresSignatureCtrGrd Ident
-- ^ All declarataions in a recursive group involving
-- constraint guards should have signatures
| InvalidConstraintGuard Prop
-- ^ The given constraint may not be used as a constraint guard
| TemporaryError Doc
-- ^ This is for errors that don't fit other cateogories.
-- We should not use it much, and is generally to be used
@ -211,6 +222,10 @@ errorImportance err =
UnsupportedFFIType {} -> 7
-- less than UnexpectedTypeWildCard
NestedConstraintGuard {} -> 10
DeclarationRequiresSignatureCtrGrd {} -> 9
InvalidConstraintGuard {} -> 5
instance TVars Warning where
apSubst su warn =
@ -218,6 +233,7 @@ instance TVars Warning where
DefaultingKind {} -> warn
DefaultingWildType {} -> warn
DefaultingTo d ty -> DefaultingTo d $! (apSubst su ty)
NonExhaustivePropGuards {} -> warn
instance FVS Warning where
fvs warn =
@ -225,6 +241,7 @@ instance FVS Warning where
DefaultingKind {} -> Set.empty
DefaultingWildType {} -> Set.empty
DefaultingTo _ ty -> fvs ty
NonExhaustivePropGuards {} -> Set.empty
instance TVars Error where
apSubst su err =
@ -262,6 +279,10 @@ instance TVars Error where
UnsupportedFFIKind {} -> err
UnsupportedFFIType src e -> UnsupportedFFIType src !$ apSubst su e
NestedConstraintGuard {} -> err
DeclarationRequiresSignatureCtrGrd {} -> err
InvalidConstraintGuard p -> InvalidConstraintGuard $! apSubst su p
TemporaryError {} -> err
@ -300,6 +321,10 @@ instance FVS Error where
UnsupportedFFIKind {} -> Set.empty
UnsupportedFFIType _ t -> fvs t
NestedConstraintGuard {} -> Set.empty
DeclarationRequiresSignatureCtrGrd {} -> Set.empty
InvalidConstraintGuard p -> fvs p
TemporaryError {} -> Set.empty
instance PP Warning where
@ -323,6 +348,10 @@ instance PP (WithNames Warning) where
text "Defaulting" <+> pp (tvarDesc d) <+> text "to"
<+> ppWithNames names ty
NonExhaustivePropGuards n ->
text "Could not prove that the constraint guards used in defining" <+>
pp n <+> text "were exhaustive."
instance PP (WithNames Error) where
ppPrec _ (WithNames err names) =
case err of
@ -337,8 +366,13 @@ instance PP (WithNames Error) where
UnexpectedTypeWildCard ->
addTVarsDescsAfter names err $
nested "Wild card types are not allowed in this context"
"(e.g., they cannot be used in type synonyms or FFI declarations)."
nested "Wild card types are not allowed in this context" $
vcat [ "They cannot be used in:"
, bullets [ "type synonyms"
, "FFI declarations"
, "declarations with constraint guards"
]
]
KindMismatch mbsrc k1 k2 ->
addTVarsDescsAfter names err $
@ -484,6 +518,27 @@ instance PP (WithNames Error) where
[ ppWithNames names t
, "When checking" <+> pp src ]
NestedConstraintGuard d ->
vcat [ "Local declaration" <+> backticks (pp d)
<+> "may not use constraint guards."
, "Constraint guards may only appear at the top-level of a module."
]
DeclarationRequiresSignatureCtrGrd d ->
vcat [ "The declaration of" <+> backticks (pp d) <+>
"requires a full type signature,"
, "because it is part of a recursive group with constraint guards."
]
InvalidConstraintGuard p ->
let d = case tNoUser p of
TCon tc _ -> pp tc
_ -> ppWithNames names p
in
vcat [ backticks d <+> "may not be used in a constraint guard."
, "Constraint guards support only numeric comparisons and `fin`."
]
TemporaryError doc -> doc
where
bullets xs = vcat [ "" <+> d | d <- xs ]

View File

@ -1,6 +1,7 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE Safe #-}
-- | Checking and conversion of 'Type's to 'FFIType's.
module Cryptol.TypeCheck.FFI

View File

@ -2,6 +2,7 @@
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE Safe #-}
-- | Errors from typechecking foreign functions.
module Cryptol.TypeCheck.FFI.Error where

View File

@ -1,5 +1,6 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE Safe #-}
-- | This module defines a nicer intermediate representation of Cryptol types
-- allowed for the FFI, which the typechecker generates then stores in the AST.

View File

@ -15,8 +15,13 @@
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE Safe #-}
-- {-# LANGUAGE Trustworthy #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
{-# LANGUAGE LambdaCase #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant <$>" #-}
{-# HLINT ignore "Redundant <&>" #-}
module Cryptol.TypeCheck.Infer
( checkE
, checkSigB
@ -30,7 +35,7 @@ import Data.Text(Text)
import qualified Data.Text as Text
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc)
import Cryptol.ModuleSystem.Name (lookupPrimDecl,nameLoc, nameIdent)
import Cryptol.Parser.Position
import qualified Cryptol.Parser.AST as P
import qualified Cryptol.ModuleSystem.Exports as P
@ -43,7 +48,8 @@ import Cryptol.TypeCheck.Kind(checkType,checkSchema,checkTySyn,
checkPropSyn,checkNewtype,
checkParameterType,
checkPrimType,
checkParameterConstraints)
checkParameterConstraints,
checkPropGuards)
import Cryptol.TypeCheck.Instantiate
import Cryptol.TypeCheck.Subst (listSubst,apSubst,(@@),isEmptySubst)
import Cryptol.TypeCheck.Unify(rootPath)
@ -52,20 +58,22 @@ import Cryptol.TypeCheck.FFI.FFIType
import Cryptol.Utils.Ident
import Cryptol.Utils.Panic(panic)
import Cryptol.Utils.RecordMap
import Cryptol.Utils.PP (pp)
import qualified Data.Map as Map
import Data.Map (Map)
import qualified Data.Set as Set
import Data.List(foldl',sortBy,groupBy)
import Data.List(foldl', sortBy, groupBy, partition)
import Data.Either(partitionEithers)
import Data.Maybe(isJust, fromMaybe, mapMaybe)
import Data.List(partition)
import Data.Ratio(numerator,denominator)
import Data.Traversable(forM)
import Data.Function(on)
import Control.Monad(zipWithM,unless,foldM,forM_,mplus,when)
import Control.Monad(zipWithM, unless, foldM, forM_, mplus, zipWithM,
unless, foldM, forM_, mplus, when)
-- import Debug.Trace
-- import Cryptol.TypeCheck.PP
inferModule :: P.Module Name -> InferM Module
inferModule m =
@ -733,15 +741,18 @@ inferCArm armNum (m : ms) =
newGoals CtComprehension [ pFin n' ]
return (m1 : ms', Map.insertWith (\_ old -> old) x t ds, tMul n n')
-- | @inferBinds isTopLevel isRec binds@ performs inference for a
-- strongly-connected component of 'P.Bind's.
-- If any of the members of the recursive group are already marked
-- as monomorphic, then we don't do generalization.
-- If @isTopLevel@ is true,
-- any bindings without type signatures will be generalized. If it is
-- false, and the mono-binds flag is enabled, no bindings without type
-- signatures will be generalized, but bindings with signatures will
-- be unaffected.
{- | @inferBinds isTopLevel isRec binds@ performs inference for a
strongly-connected component of 'P.Bind's.
If any of the members of the recursive group are already marked
as monomorphic, then we don't do generalization.
If @isTopLevel@ is true,
any bindings without type signatures will be generalized. If it is
false, and the mono-binds flag is enabled, no bindings without type
signatures will be generalized, but bindings with signatures will
be unaffected.
-}
inferBinds :: Bool -> Bool -> [P.Bind Name] -> InferM [Decl]
inferBinds isTopLevel isRec binds =
do -- when mono-binds is enabled, and we're not checking top-level
@ -789,6 +800,8 @@ inferBinds isTopLevel isRec binds =
genCs <- generalize bs1 cs
return (done,genCs)
checkNumericConstraintGuardsOK isTopLevel sigs noSigs
rec
let exprMap = Map.fromList (map monoUse genBs)
(doneBs, genBs) <- check exprMap
@ -816,6 +829,37 @@ inferBinds isTopLevel isRec binds =
withQs = foldl' appP withTys qs
{-
Here we also check that:
* Numeric constraint guards appear only at the top level
* All definitions in a recursive groups with numberic constraint guards
have signatures
The reason is to avoid interference between local constraints coming
from the guards and type inference. It might be possible to
relex these requirements, but this requires some more careful thought on
the interaction between the two, and the effects on pricniple types.
-}
checkNumericConstraintGuardsOK ::
Bool -> [P.Bind Name] -> [P.Bind Name] -> InferM ()
checkNumericConstraintGuardsOK isTopLevel haveSig noSig =
do unless isTopLevel
(mapM_ (mkErr NestedConstraintGuard) withGuards)
unless (null withGuards)
(mapM_ (mkErr DeclarationRequiresSignatureCtrGrd) noSig)
where
mkErr f b =
do let nm = P.bName b
inRange (srcRange nm) (recordError (f (nameIdent (thing nm))))
withGuards = filter hasConstraintGuards haveSig
-- When desugaring constraint guards we check that they have signatures,
-- so no need to look at noSig
hasConstraintGuards b =
case thing (P.bDef b) of
P.DPropGuards {} -> True
_ -> False
@ -836,9 +880,10 @@ guessType exprMap b@(P.Bind { .. }) =
Just s ->
do let wildOk = case thing bDef of
P.DForeign {} -> NoWildCards
P.DPrim -> NoWildCards
P.DExpr {} -> AllowWildCards
P.DForeign {} -> NoWildCards
P.DPrim -> NoWildCards
P.DExpr {} -> AllowWildCards
P.DPropGuards {} -> NoWildCards
s1 <- checkSchema wildOk s
return ((name, ExtVar (fst s1)), Left (checkSigB b s1))
@ -973,25 +1018,33 @@ checkMonoB b t =
, dDoc = P.bDoc b
}
P.DPropGuards _ ->
tcPanic "checkMonoB"
[ "Used constraint guards without a signature at "
, show . pp $ P.bName b ]
-- XXX: Do we really need to do the defaulting business in two different places?
checkSigB :: P.Bind Name -> (Schema,[Goal]) -> InferM Decl
checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
checkSigB b (Forall as asmps0 t0, validSchema) =
let name = thing (P.bName b) in
case thing (P.bDef b) of
-- XXX what should we do with validSchema in this case?
P.DPrim ->
do return Decl { dName = thing (P.bName b)
, dSignature = Forall as asmps0 t0
, dDefinition = DPrim
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
-- XXX what should we do with validSchema in this case?
P.DPrim ->
return Decl
{ dName = name
, dSignature = Forall as asmps0 t0
, dDefinition = DPrim
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
P.DForeign ->
do let loc = getLoc b
name = thing $ P.bName b
src = DefinitionOf name
P.DForeign -> do
let loc = getLoc b
name' = thing $ P.bName b
src = DefinitionOf name'
inRangeMb loc do
-- Ensure all type params are of kind #
forM_ as \a ->
@ -1001,8 +1054,8 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
ffiFunType <-
case toFFIFunType (Forall as asmps0 t0) of
Right (props, ffiFunType) -> ffiFunType <$ do
ffiGoals <- traverse (newGoal (CtFFI name)) props
proveImplication True (Just name) as asmps0 $
ffiGoals <- traverse (newGoal (CtFFI name')) props
proveImplication True (Just name') as asmps0 $
validSchema ++ ffiGoals
Left err -> do
recordErrorLoc loc $ UnsupportedFFIType src err
@ -1019,54 +1072,198 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
, dDoc = P.bDoc b
}
P.DExpr e0 ->
inRangeMb (getLoc b) $
withTParams as $
do (e1,cs0) <- collectGoals $
do let nm = thing (P.bName b)
tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
addGoals validSchema
() <- simplifyAllConstraints -- XXX: using `asmps` also?
return e1
P.DExpr e0 ->
inRangeMb (getLoc b) $
withTParams as $ do
(t, asmps, e2) <- checkBindDefExpr [] asmps0 e0
asmps1 <- applySubstPreds asmps0
cs <- applySubstGoals cs0
return Decl
{ dName = name
, dSignature = Forall as asmps t
, dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
let findKeep vs keep todo =
let stays (_,cvs) = not $ Set.null $ Set.intersection vs cvs
(yes,perhaps) = partition stays todo
(stayPs,newVars) = unzip yes
in case stayPs of
[] -> (keep,map fst todo)
_ -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
P.DPropGuards cases0 ->
inRangeMb (getLoc b) $
withTParams as $ do
asmps1 <- applySubstPreds asmps0
t1 <- applySubst t0
cases1 <- mapM checkPropGuardCase cases0
let -- if a goal mentions any of these variables, we'll commit to
-- solving it now.
stickyVars = Set.fromList (map tpVar as) `Set.union` fvs asmps1
(stay,leave) = findKeep stickyVars []
[ (c, fvs c) | c <- cs ]
exh <- checkExhaustive (P.bName b) as asmps1 (map fst cases1)
unless exh $
-- didn't prove exhaustive i.e. none of the guarding props
-- necessarily hold
recordWarning (NonExhaustivePropGuards name)
addGoals leave
let schema = Forall as asmps1 t1
return Decl
{ dName = name
, dSignature = schema
, dDefinition = DExpr
(foldr ETAbs
(foldr EProofAbs
(EPropGuards cases1 t1)
asmps1)
as)
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
su <- proveImplication False (Just (thing (P.bName b))) as asmps1 stay
extendSubst su
where
let asmps = concatMap pSplitAnd (apSubst su asmps1)
t <- applySubst t0
e2 <- applySubst e1
checkBindDefExpr ::
[Prop] -> [Prop] -> P.Expr Name -> InferM (Type, [Prop], Expr)
checkBindDefExpr asmpsSign asmps1 e0 = do
return Decl
{ dName = thing (P.bName b)
, dSignature = Forall as asmps t
, dDefinition = DExpr (foldr ETAbs (foldr EProofAbs e2 asmps) as)
, dPragmas = P.bPragmas b
, dInfix = P.bInfix b
, dFixity = P.bFixity b
, dDoc = P.bDoc b
}
(e1,cs0) <- collectGoals $ do
let nm = thing (P.bName b)
tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
addGoals validSchema
() <- simplifyAllConstraints -- XXX: using `asmps` also?
return e1
asmps2 <- applySubstPreds asmps1
cs <- applySubstGoals cs0
let findKeep vs keep todo =
let stays (_,cvs) = not $ Set.null $ Set.intersection vs cvs
(yes,perhaps) = partition stays todo
(stayPs,newVars) = unzip yes
in case stayPs of
[] -> (keep,map fst todo)
_ -> findKeep (Set.unions (vs:newVars)) (stayPs ++ keep) perhaps
let -- if a goal mentions any of these variables, we'll commit to
-- solving it now.
stickyVars = Set.fromList (map tpVar as) `Set.union` fvs asmps2
(stay,leave) = findKeep stickyVars []
[ (c, fvs c) | c <- cs ]
addGoals leave
-- includes asmpsSign for the sake of implication, but doesn't actually
-- include them in the resulting asmps
su <- proveImplication True (Just (thing (P.bName b))) as (asmpsSign <> asmps2) stay
extendSubst su
let asmps = concatMap pSplitAnd (apSubst su asmps2)
t <- applySubst t0
e2 <- applySubst e1
pure (t, asmps, e2)
{- |
Given a DPropGuards of the form
@
f : {...} A
f | (B1, B2) => ...
| (C1, C2, C2) => ...
@
we check that it is exhaustive by trying to prove the following
implications:
@
A /\ ~B1 => C1 /\ C2 /\ C3
A /\ ~B2 => C1 /\ C2 /\ C3
@
The implications were derive by the following general algorithm:
- Find that @(C1, C2, C3)@ is the guard that has the most conjuncts, so we
will keep it on the RHS of the generated implications in order to minimize
the number of implications we need to check.
- Negate @(B1, B2)@ which yields @(~B1) \/ (~B2)@. This is a disjunction, so
we need to consider a branch for each disjunct --- one branch gets the
assumption @~B1@ and another branch gets the assumption @~B2@. Each
branch's implications need to be proven independently.
-}
checkExhaustive :: Located Name -> [TParam] -> [Prop] -> [[Prop]] -> InferM Bool
checkExhaustive name as asmps guards =
case sortBy cmpByLonger guards of
[] -> pure False -- XXX: we should check the asmps are unsatisfiable
longest : rest -> doGoals (theAlts rest) (map toGoal longest)
where
cmpByLonger props1 props2 = compare (length props2) (length props1)
-- reversed, so that longets is first
theAlts :: [[Prop]] -> [[Prop]]
theAlts = map concat . sequence . map chooseNeg
-- Choose one of the things to negate
chooseNeg ps =
case ps of
[] -> []
p : qs -> (pNegNumeric p ++ qs) : [ p : alts | alts <- chooseNeg qs ]
-- Try to validate all cases
doGoals todo gs =
case todo of
[] -> pure True
alt : more ->
do ok <- canProve (asmps ++ alt) gs
if ok then doGoals more gs
else pure False
toGoal :: Prop -> Goal
toGoal prop =
Goal
{ goalSource = CtPropGuardsExhaustive (thing name)
, goalRange = srcRange name
, goal = prop
}
canProve :: [Prop] -> [Goal] -> InferM Bool
canProve asmps' goals =
tryProveImplication (Just (thing name)) as asmps' goals
{- | This function does not validate anything---it just translates into
the type-checkd syntax. The actual validation of the guard will happen
when the (automatically generated) function corresponding to the guard is
checked, assuming 'ExpandpropGuards' did its job correctly.
-}
checkPropGuardCase :: P.PropGuardCase Name -> InferM ([Prop],Expr)
checkPropGuardCase (P.PropGuardCase guards e0) =
do ps <- checkPropGuards guards
tys <- mapM (`checkType` Nothing) ts
let rhsTs = foldl ETApp (getV eV) tys
rhsPs = foldl (\e _p -> EProofApp e) rhsTs ps
rhs = foldl EApp rhsPs (map getV es)
pure (ps,rhs)
where
(e1,es) = P.asEApps e0
(eV,ts) = case e1 of
P.EAppT ex1 tis -> (ex1, map getT tis)
_ -> (e1, [])
getV ex =
case ex of
P.EVar x -> EVar x
_ -> bad "Expression is not a variable."
getT ti =
case ti of
P.PosInst t -> t
P.NamedInst {} -> bad "Unexpeceted NamedInst"
bad msg = panic "checkPropGuardCase" [msg]
--------------------------------------------------------------------------------
--------------------------------------------------------------------------------

View File

@ -220,6 +220,7 @@ data ConstraintSource
| CtImprovement
| CtPattern TypeSource -- ^ Constraints arising from type-checking patterns
| CtModuleInstance ModName -- ^ Instantiating a parametrized module
| CtPropGuardsExhaustive Name -- ^ Checking that a use of prop guards is exhastive
| CtFFI Name -- ^ Constraints on a foreign declaration required
-- by the FFI (e.g. sequences must be finite)
deriving (Show, Generic, NFData)
@ -249,6 +250,7 @@ instance TVars ConstraintSource where
CtImprovement -> src
CtPattern _ -> src
CtModuleInstance _ -> src
CtPropGuardsExhaustive _ -> src
CtFFI _ -> src
@ -356,6 +358,7 @@ instance PP ConstraintSource where
CtImprovement -> "examination of collected goals"
CtPattern ad -> "checking a pattern:" <+> pp ad
CtModuleInstance n -> "module instantiation" <+> pp n
CtPropGuardsExhaustive n -> "exhaustion check for prop guards used in defining" <+> pp n
CtFFI f -> "declaration of foreign function" <+> pp f
ppUse :: Expr -> Doc

View File

@ -6,6 +6,7 @@
-- Stability : provisional
-- Portability : portable
{-# Language OverloadedStrings #-}
{-# Language Safe #-}
module Cryptol.TypeCheck.Instantiate
( instantiateWith
, TypeArg(..)

View File

@ -1,3 +1,5 @@
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Interface where
import qualified Data.Map as Map

View File

@ -7,6 +7,7 @@
-- Portability : portable
{-# LANGUAGE RecursiveDo #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE Safe #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
@ -19,6 +20,7 @@ module Cryptol.TypeCheck.Kind
, checkPropSyn
, checkParameterType
, checkParameterConstraints
, checkPropGuards
) where
import qualified Cryptol.Parser.AST as P
@ -40,8 +42,6 @@ import Data.Function(on)
import Data.Text (Text)
import Control.Monad(unless,when)
-- | Check a type signature. Returns validated schema, and any implicit
-- constraints that we inferred.
checkSchema :: AllowWildCards -> P.Schema Name -> InferM (Schema, [Goal])
@ -66,6 +66,30 @@ checkSchema withWild (P.Forall xs ps t mb) =
Nothing -> id
Just r -> inRange r
{- | Validate parsed propositions that appear in the guard of a PropGuard.
* Note that we don't validate the well-formedness constraints here---instead,
they'd be validated when the signature for the auto generated
function corresponding guard is checked.
* We also check that there are no wild-cards in the constraints.
-}
checkPropGuards :: [Located (P.Prop Name)] -> InferM [Prop]
checkPropGuards props =
do (newPs,_gs) <- collectGoals (mapM check props)
pure newPs
where
check lp =
inRange (srcRange lp)
do let p = thing lp
(_,ps) <- withTParams NoWildCards schemaParam [] (checkProp p)
case tNoUser ps of
TCon (PC x) _ | x `elem` [PEqual,PNeq,PGeq,PFin,PTrue] -> pure ()
_ -> recordError (InvalidConstraintGuard ps)
pure ps
-- | Check a module parameter declarations. Nothing much to check,
-- we just translate from one syntax to another.
checkParameterType :: P.ParameterType Name -> Maybe Text -> InferM ModTParam
@ -398,7 +422,7 @@ doCheckType ty k =
-- | Validate a parsed proposition.
checkProp :: P.Prop Name -- ^ Proposition that need to be checked
-> KindM Type -- ^ Checked representation
-> KindM Prop -- ^ Checked representation
checkProp (P.CType t) = doCheckType t (Just KProp)
@ -411,5 +435,3 @@ checkKind _ (Just k1) k2
| k1 /= k2 = do kRecordError (KindMismatch Nothing k1 k2)
kNewType TypeErrorPlaceHolder k1
checkKind t _ _ = return t

View File

@ -63,6 +63,8 @@ instance ShowParseable Expr where
--NOTE: erase all "proofs" for now (change the following two lines to change that)
showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")"
showParseable (EPropGuards guards _) = parens (text "EPropGuards" $$ showParseable guards)
instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
showParseable (x,y) = parens (showParseable x <> comma <> showParseable y)

View File

@ -270,6 +270,9 @@ exprSchema expr =
in go dgs
EPropGuards _guards typ ->
pure Forall {sVars = [], sProps = [], sType = typ}
checkHas :: Type -> Selector -> TcM Type
checkHas t sel =
case sel of

View File

@ -1,4 +1,5 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE Safe #-}
-- See Note [-Wincomplete-uni-patterns and irrefutable patterns] in Cryptol.TypeCheck.TypePat
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
module Cryptol.TypeCheck.SimpType where

View File

@ -11,6 +11,7 @@
module Cryptol.TypeCheck.Solve
( simplifyAllConstraints
, proveImplication
, tryProveImplication
, proveModuleTopLevel
, defaultAndSimplify
, defaultReplExpr
@ -287,6 +288,25 @@ proveImplication dedupErrs lnam as ps gs =
Left errs -> mapM_ recordError errs
return su
-- | Tries to prove an implication. If proved, then returns `Right (m_su ::
-- InferM Subst)` where `m_su` is an `InferM` computation that results in the
-- solution substitution, and records any warning invoked during proving. If not
-- proved, then returns `Left (m_err :: InferM ())`, which records all errors
-- invoked during proving.
tryProveImplication ::
Maybe Name -> [TParam] -> [Prop] -> [Goal] -> InferM Bool
tryProveImplication lnam as ps gs =
do evars <- varsWithAsmps
solver <- getSolver
extraAs <- (map mtpParam . Map.elems) <$> getParamTypes
extra <- map thing <$> getParamConstraints
(mbErr,_su) <- io (proveImplicationIO solver False lnam evars
(extraAs ++ as) (extra ++ ps) gs)
case mbErr of
Left {} -> pure False
Right {} -> pure True
proveImplicationIO :: Solver
-> Bool -- ^ Whether to remove duplicate goals in errors

View File

@ -1,3 +1,5 @@
{-# LANGUAGE Safe #-}
-- | Look for opportunity to solve goals by instantiating variables.
module Cryptol.TypeCheck.Solver.Improve where

View File

@ -10,6 +10,7 @@
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE Safe #-}
module Cryptol.TypeCheck.Solver.Numeric.Interval where

Some files were not shown because too many files have changed in this diff Show More