From 16ee58b77d9945803a03a7ab6d83376d15132582 Mon Sep 17 00:00:00 2001 From: Chris Phifer Date: Tue, 24 Nov 2020 11:51:01 -0600 Subject: [PATCH] Pull Argo docs in build --- cryptol-remote-api/docs/Cryptol.rst | 336 ++++++++++++++++++++++++++++ cryptol-remote-api/docs/Errors.rst | 161 +++++++++++++ cryptol-remote-api/docs/Makefile | 8 + cryptol-remote-api/docs/index.rst | 9 +- 4 files changed, 511 insertions(+), 3 deletions(-) create mode 100644 cryptol-remote-api/docs/Cryptol.rst create mode 100644 cryptol-remote-api/docs/Errors.rst diff --git a/cryptol-remote-api/docs/Cryptol.rst b/cryptol-remote-api/docs/Cryptol.rst new file mode 100644 index 00000000..df3052ca --- /dev/null +++ b/cryptol-remote-api/docs/Cryptol.rst @@ -0,0 +1,336 @@ +================== +Cryptol Evaluation +================== + +All methods in this section additionally propagate server state in the +manner described in the prior section. + +These methods may return :ref:`a variety of Cryptol errors +`, with codes in the range of ``20000``-``29999``. + +Module Management +================= + +Changing Directories +-------------------- + +:Method name: + ``change directory`` +:Parameters: + - ``directory``: The new working directory, represented as a string. + +Loading Modules +--------------- + +:Method name: + ``load module`` +:Parameters: + - ``module name``: The name of the Cryptol module to be loaded. + +Loading Files +------------- + +:Method name: + ``load file`` +:Parameters: + - ``file``: The name of the Cryptol source file to be loaded. + +Module Context +-------------- + +:Method name: + ``focused module`` +:Parameters: none +:Return fields: + - ``module``: The name of the focused module, which would be shown in the + prompt in the Cryptol REPL, or ``null`` if there is no such focused module. + - ``parameterized``: A Boolean value indicating whether the focused module is + parameterized. This field is only present when the module name is not + ``null``. + +Evaluation and Typechecking +=========================== + +Evaluating Expressions +---------------------- + +This method evaluates a Cryptol expression. The type of the expression +needs to be fully-determined and finite - that is, functions and +infinite streams are not supported, and neither is polymorphism. + +:Method name: + ``evaluate expression`` +:Parameters: + - ``expression``: The :ref:`JSON Cryptol expression ` to be evaluated +:Return fields: + - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value + - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type + - ``type string``: A human-readable representation of the result type + +Calling Functions +----------------- + +Note: this method may be removed in the future, because its abilities +have been subsumed by ``evaluate expression``. + +This method applies a Cryptol function to some arguments. The type of +the resulting expression needs to be fully-determined and finite - +that is, functions and infinite streams are not supported, and neither +is polymorphism. + +:Method name: + ``call`` +:Parameters: + - ``function``: The name of a Cryptol function that is currently in scope + - ``arguments``: A list of arguments to the function, encoded as JSON + Cryptol expressions +:Return fields: + - ``value``: A :ref:`JSON Cryptol expression ` that denotes the value + - ``type``: A :ref:`JSON Cryptol type ` that denotes the result type + - ``type string``: A human-readable representation of the result type + +Visible Names +------------- + +Return information about all names in scope. + +:Method name: + ``visible names`` +:Parameters: none +:Return value: + A list of name information objects. Each name information object has the following + fields: + + - ``name``: A human-readable representation of the name + - ``type string``: A human-readable representation of the name's type schema + - ``type``: A :ref:`JSON Cryptol type ` + + Some will additionally have the following field: + + - ``documentation``: The documentation string for the name, if it is documented + +Checking Types +-------------- + +Check the type of an expression. + +:Method name: + ``check type`` +:Parameters: + - ``expression``: A :ref:`JSON Cryptol expression ` for which a type is desired. +:Return fields: + - ``type schema``: A :ref:`JSON Cryptol type ` + +SAT +--- + +This method is not yet ready for public consumption. + +Terms and Types +=============== + +.. _cryptol-json-expression: + +JSON Cryptol Expressions +------------------------ + +In the API, Cryptol expressions can be represented by the following: + +JSON Booleans + Represent the corresponding Cryptol Booleans + +JSON Integers + Cryptol integer literals, that can be used at a variety of types + +JSON Strings + Cryptol concrete syntax + +JSON Objects + Objects can represent a variety of Cryptol expressions. The field + ``expression`` contains a tag that can be used to determine the + remaining fields. + +The tag values in objects can be: + +``bits`` + The expression is a bitvector. Further fields are: + + + ``encoding``: Either the string ``base64`` or ``hex``, for base-64 or hexadecimal + representations of the bitvector + + ``data``: A string containing the actual data + + ``width``: An integer: the bit-width of the represented bit vector + +``record`` + The expression is a record. The field ``data`` is a JSON + object that maps record field names to :ref:`JSON Cryptol expressions `. + +``sequence`` + The expression is a sequence. The field ``data`` contains a + JSON array of the elements of the sequence; each is a JSON Cryptol + expression. + +``tuple`` + The expression is a tuple. The field ``data`` contains a JSON + array of the elements of the tuple; each is a JSON Cryptol + expression. + +``unit`` + The expression is the unit constructor, and there are no further fields. + +``let`` + The expression is a ``where`` binding. The fields are: + + ``binders`` + A list of binders. Each binder is an object with two fields: + + - ``name``: A string that is the name to be bound, and + - ``definition``: A :ref:`JSON Cryptol expression `. + + ``body`` + A :ref:`JSON Cryptol expression ` in which the bound names may be used. + +``call`` + The expression is a function application. Further fields are: + + - ``function``: A :ref:`JSON Cryptol expressions `. + - ``arguments``: A JSON array of :ref:`JSON Cryptol expressions `. + +``instantiate`` + The expression is a type application. Further fields are: + + - ``generic``: The polymorphic expression to be instantiated + - ``arguments``: A JSON object in which keys are the names of type parameters and values are :ref:`JSON Cryptol types `. + +``integer modulo`` + The expression is an integer with a modulus (the Cryptol ``Z`` type). Further fields are: + + - ``integer``: A JSON number, representing the integer + - ``modulus``: A JSON number, representing the modulus + +.. _cryptol-json-type: + +JSON Cryptol Types +------------------ + +JSON representations of types are type schemas. A type schema has +three fields: + +``forall`` + + Contains an array of objects. Each object has two fields: ``name`` + is the name of a type variable, and ``kind`` is its kind. There + are four kind formers: the string ``Type`` represents ordinary + datatypes, the string ``Num`` is the kind of numbers, and + ``Prop`` is the kind of propositions. Arrow kinds are represented + by objects in which the field ``kind`` is the string ``arrow``, + and the fields ``from`` and ``to`` are the kinds on the left and + right side of the arrow, respectively. + +``propositions`` + A JSON array of the constraints in the type. + +``type`` + The type in which the variables from ``forall`` are in scope and + the constraints in ``propositions`` are in effect. + +Concrete Types +~~~~~~~~~~~~~~ + +Types are represented as JSON objects. The ``type`` field contains one of the following tags (represented as JSON strings): + +``variable`` + The type is a type variable. The remaining fields are ``name``, + which contains the variable's name, and ``kind``, which contains + its kind (represented as in the ``forall`` section). When providing + types to Cryptol, the ``kind`` field should be elided, and type synonyms + may be provided with arguments through an optional ``arguments`` field. + +``record`` + The type is a record type. The remaining field is ``fields``, + which contains a JSON object whose keys are the names of fields and + whose values are the fields' types. + +``number`` + The type is a number. The field ``value`` contains the number + itself. + +``inf`` + The type is the infinite number. There are no further fields. + +``Bit`` + The type is the bit type. There are no further fields. + +``Integer`` + The type is the integer type. There are no further fields. + +``Rational`` + The type is the rational number type. There are no further fields. + +``Z`` + The type is integers modulo another value. The field ``modulus`` + contains the modulus, which is a type. + +``bitvector`` + The type is a bitvector. The field ``width`` contains the number + of bits, which is a type. + +``sequence`` + The type is a sequence. The field ``length`` contains the length + of the sequence (a type), and the field ``contents`` contains the + type of entries in the sequence. + +``function`` + The type is a function type. The fields ``domain`` and ``range`` + contain the domain and range types. + +``unit`` + The type is the unit type. There are no further fields. + +``tuple`` + The type is a tuple. The field ``contents`` is a JSON array + containing the types of the projections from the tuple. + +One of ``+``, ``-``, ``*``, ``/``, ``%``, ``^^``, ``width``, ``min``, ``max``, ``/^``, ``%^``, ``lengthFromThenTo`` + The type is an application of the indicated type function. The + arguments are contained in the ``arguments`` field, as a JSON + array. + +Propositions +~~~~~~~~~~~~ + +Propositions/constraints have the key ``prop``, mapped to one of the +following tags: + +``==`` + Equality. The equated terms are in the ``left`` and ``right`` + fields. + +``!=`` + Inequality. The disequated terms are in the ``left`` and + ``right`` fields. + +``>=`` + Greater than. The greater type is in the ``greater`` field and the + lesser type is in the ``lesser`` field. + +``fin`` + Finitude. The finite type is in the ``subject`` field. + +``has`` + The selector is in the ``selector`` field, the type that has this + selector is in the ``type`` field, and the type expected for the + projection is in the ``is`` field. + +``Arith``, ``Cmp``, ``SignedCmp``, ``Zero``, ``Logic`` + The type that has these operations defined is in the ``subject`` + field. + +``Literal`` + The size is in the ``size`` field, and the type is in the + ``subject`` field. + +``True`` + There are no further fields. + +``And`` + The conjuncts are in the ``left`` and ``right`` fields. diff --git a/cryptol-remote-api/docs/Errors.rst b/cryptol-remote-api/docs/Errors.rst new file mode 100644 index 00000000..3a5b9c71 --- /dev/null +++ b/cryptol-remote-api/docs/Errors.rst @@ -0,0 +1,161 @@ +Errors returned by the JSON-RPC API +=================================== + +The JSON-RPC spec reserves the following error codes: + ++ ``-32602``: “Invalid params” (for this particular known method) ++ ``-32700``: “Parse error” (i.e. invalid JSON) ++ ``-32601``: “Method not found” ++ ``-32600``: “Invalid request” ++ ``-32603``: “Internal error” + +In the case where an error is returned and a ``data`` object is attached, it +MUST be a JSON object. It MAY contain a ``path`` field which, if present, MUST +be a string referencing a specific file to which the error pertains. It MAY also +contain a ``warnings`` field which, if present, MUST be a JSON list of warnings +which occurred alongside this error. + +Specific errors are free to define all other fields of the ``data`` object to +hold data of their choice specific to the error at hand. In the lists of errors +below, informal JSON schemata will be used to describe the format of these +additional fields, omitting the mention of the ``path`` and ``warnings`` fields. +A client SHOULD expect that these fields may be present or absent from the +error response to any given request to the API. + +Errors in the Argo Protocol Layer (``1``–``9999``) +-------------------------------------------------- + +If the client is correctly following the JSON-RPC spec but failing to conform to +the protocol of the state-caching Argo service, some errors may be thrown +specific to that. + +State field (``1``–``99``) +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``10``: “Missing state field” +- ``20``: “Invalid state field” ``{ state: , error: String }`` + +.. _saw-server-errors: + +SAW Server Errors (``10000``–``19999``) +--------------------------------------- + +.. + The SAW server uses the same errors as the Cryptol server for Cryptol errors + (that is, when a Cryptol error occurs it should be directly returned as such, + which will have a code outside this range). + +An error in this range should be considered a bug in a client: a client +correctly interacting with the Argo API should never see these errors, and they +are indicative that the client is doing something wrong. + +Server value errors (``10000``–``10099``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``10000``: “No server value with name \____\_” ``{ name: String }`` +- ``10010``: “The server value with name \____\_ is not a Cryptol environment” + ``{ name: String }`` +- ``10020``: “The server value with name \____\_ is not an LLVM module” + ``{name: String }`` +- ``10030``: “The server value with name \____\_ is not an LLVM setup script” + ``{ name: String }`` +- ``10040``: “The server value with name \____\_ is not an LLVM setup value” + ``{ name: String }`` +- ``10050``: “The server value with name \____\_ is not an LLVM method + specification” + ``{ name: String }`` +- ``10080``: “The server value with name \____\_ is not a JVM class” + ``{ name: String }`` +- ``10090``: “The server value with name \____\_ is not a JVM method + specification” + ``{ name: String }`` + +Setup errors (``10100``–``10199``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``10100``: “Not currently setting up Cryptol” +- ``10110``: “Not currently setting up Crucible/LLVM” +- ``10120``: “Not at top level” ``{ tasks: [String] }`` + +Loading and filesystem errors (``10200``–``10299``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``10200``: “Can’t load LLVM module” ``{ error: String }`` + +Verification errors (``10300``–``19999``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``10300``: Verification exception ``{ error: String }``. This error will be + likely split into several specific separate errors in the future and possibly + deprecated. + +Cryptol errors (``11000``, to be deprecated) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``11000``: Cryptol exception ``{ error: String }``. This error will be + deprecated in a future release and Cryptol errors will instead be reported + identically to the manner described below for the Cryptol-only server. + +.. _cryptol-server-errors: + +Cryptol Server Errors (``20000``–``29999``) +------------------------------------------- + +Parse, print, and load errors (``20000``–``20199``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``20000``: “There was a Cryptol parse error” + ``{ error: String, input: String }`` (the input is rendered as + literal string) +- ``20010``: “Bad UTF-8” ``{ path: String, error: String }`` +- ``20020``: “Invalid Base64” ``{ input: String }`` +- ``20030``: “Not a hex digit” ``{ input: String }`` +- ``20040``: “Can’t convert Cryptol data from this type to JSON” + ``{ type: , "type string": String }`` where the JSON object for ``type`` + is a :ref:`JSON Cryptol type `. +- ``20050``: “Can’t find file” ``{ path: String }`` +- ``20051``: “Can’t find directory ``{ path: String }`` (this is for + the ``ChangeDir`` method) +- ``20060``: “Other IO error” ``{ path: String, error: String }`` + +Evaluation errors (``20200``–``20499``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``20200``: “Can’t evaluate at polymorphic type” + ``{ type: , "type string": String }`` where the JSON object for ``type`` + is a :ref:`JSON Cryptol type `. +- ``20210``: “Execution would have required these defaults” + ``{ defaults: [ { parameter: String, type: "type string": String } ] }`` + where the JSON object for ``type`` is a + :ref:`JSON Cryptol type `. +- ``20220``: “Can’t evaluate Cryptol in a parameterized module” + ``{ modules: [String] }`` +- ``20230``: “Prover error” ``{ error: String }`` + +Module errors (``20500``–``20699``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``20500``: “Module not found” ``{ source: String, path: String }`` +- ``20540``: “Module parse error” ``{ source: String, error: String }`` +- ``20550``: “Recursive modules” ``{ modules: [String] }`` +- ``20600``: “Module name mismatch” + ``{ expected: String, found: String }`` +- ``20610``: “Duplicate module name” + ``{ name: String, paths: [String, String] (2-element list) }`` +- ``20630``: “Imported parameterized module” ``{ module: String }`` +- ``20640``: “Failed to parameterize module defs” + ``{ module: String, parameters: [String] }`` +- ``20650``: “Not a parameterized module” ``{ module: String }`` + +Type errors (``20700``–``29999``) +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +- ``20700``: “Renamer error(s)” + ``{ source: String, errors: [String] }`` +- ``20710``: “No pat errors” ``{ source: String, errors: [String] }`` +- ``20720``: “No include errors” + ``{ source: String, errors: [String] }`` +- ``20730``: “Typechecking failed” + ``{ source: String, errors: [String] }`` (could be split in future + into many separate errors) +- ``29999``: “Other failure” ``{ error: String }`` diff --git a/cryptol-remote-api/docs/Makefile b/cryptol-remote-api/docs/Makefile index d4bb2cbb..9e4b56c0 100644 --- a/cryptol-remote-api/docs/Makefile +++ b/cryptol-remote-api/docs/Makefile @@ -8,6 +8,12 @@ SPHINXBUILD ?= sphinx-build SOURCEDIR = . BUILDDIR = _build +# Documentation taken from Argo +# Edit ARGODOCS if the dependency path changes; add reST files to ARGODEPS +# that live in Argo but are needed here +ARGODOCS = ../../deps/argo/docs +ARGODEPS = Protocol.rst + # Put it first so that "make" without argument is like "make help". help: @$(SPHINXBUILD) -M help "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) @@ -17,4 +23,6 @@ help: # Catch-all target: route all unknown targets to Sphinx using the new # "make mode" option. $(O) is meant as a shortcut for $(SPHINXOPTS). %: Makefile + cp $(foreach d,$(ARGODEPS),$(ARGODOCS)/$(d)) . @$(SPHINXBUILD) -M $@ "$(SOURCEDIR)" "$(BUILDDIR)" $(SPHINXOPTS) $(O) + rm $(ARGODEPS) diff --git a/cryptol-remote-api/docs/index.rst b/cryptol-remote-api/docs/index.rst index 71fa7bc1..db60a119 100644 --- a/cryptol-remote-api/docs/index.rst +++ b/cryptol-remote-api/docs/index.rst @@ -3,13 +3,16 @@ You can adapt this file completely to your liking, but it should at least contain the root `toctree` directive. -Welcome to Cryptol Remote API's documentation! -============================================== +Cryptol Remote API +================== .. toctree:: - :maxdepth: 2 + :maxdepth: 3 :caption: Contents: + Protocol Overview + Cryptol Evaluation + Errors Indices and tables