cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Merge pull request #10132 from ethereum/smt_docs_types

Browse Source 
Update SMT types docs
This commit is contained in:
Đorđe Mijović 2020-10-28 16:30:58 +01:00 committed by GitHub
commit cfc1eb0029
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 15 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
docs/security-considerations.rst
View File

@ -448,19 +448,21 @@ The SMT encoding tries to be as precise as possible, mapping Solidity types
and expressions to their closest `SMT-LIB <http://smtlib.cs.uiowa.edu/>`_
representation, as shown in the table below.
+-----------------------+--------------+-----------------------------+
|Solidity type |SMT sort |Theories (quantifier-free) |
+=======================+==============+=============================+
|Boolean |Bool |Bool |
+-----------------------+--------------+-----------------------------+
|intN, uintN, address, |Integer |LIA, NIA |
|bytesN, enum | | |
+-----------------------+--------------+-----------------------------+
|array, mapping, bytes, |Array |Arrays |
|string | | |
+-----------------------+--------------+-----------------------------+
|other types |Integer |LIA |
+-----------------------+--------------+-----------------------------+
+-----------------------+--------------------------------+-----------------------------+
|Solidity type |SMT sort |Theories (quantifier-free) |
+=======================+================================+=============================+
|Boolean |Bool |Bool |
+-----------------------+--------------------------------+-----------------------------+
|intN, uintN, address, |Integer |LIA, NIA |
|bytesN, enum | | |
+-----------------------+--------------------------------+-----------------------------+
|array, mapping, bytes, |Tuple |Datatypes, Arrays, LIA |
|string |(Array elements, Integer length)| |
+-----------------------+--------------------------------+-----------------------------+
|struct |Tuple |Datatypes |
+-----------------------+--------------------------------+-----------------------------+
|other types |Integer |LIA |
+-----------------------+--------------------------------+-----------------------------+
Types that are not yet supported are abstracted by a single 256-bit unsigned
integer, where their unsupported operations are ignored.