Merge pull request #17 from formal-land/guillaume-claret@add-install-…

…instructions

doc: add getting started

coq/docs/src/SUMMARY.md

@@ -2,6 +2,6 @@
 
 [Introduction](./introduction.md)
 
-<!-- # User Guide
+# User Guide
 
-- [Installation](guide/installation.md) -->
+- [Getting Started](guide/getting_started.md)

coq/docs/src/guide/getting_started.md

@@ -0,0 +1,66 @@
+# Getting Started
+
+Here we give you the instructions to get started to translate Solidity smart contracts to Coq.
+
+## Translate Solidity to Coq
+
+If you have a smart contract named `contract.sol`, generate the JSON of its unoptimized Yul code with the following command:
+
+```
+solc --ir-ast-json contract.sol \
+  | tail -1 \
+  > contract.yul.json
+```
+
+assuming you have installed the Solidity compiler `solc`.
+
+Then clone the repository of [coq-of-solidity](https://github.com/formal-land/coq-of-solidity):
+
+```
+git clone --recursive https://github.com/formal-land/coq-of-solidity.git
+cd coq-of-solidity
+```
+
+Then translate it to Coq with the following command:
+
+```
+python coq/scripts/shallow_embed.py path/to/contract.yul.json \
+  > shallow.v
+```
+
+The resulting file `shallow.v` contains the Coq code of the smart contract. Generally the first part is the deployment code (constructor), and then comes the code for the entrypoints of the smart contract.
+
+## Compile the generated Coq code
+
+Assuming you have a working installation of the [opam]() package manager that we use for Coq, from the root of the `coq-of-solidity` repository, run the following command to install the `CoqOfSolidity` library:
+
+```
+opam install --deps-only coq/CoqOfSolidity/coq-of-solidity.opam
+```
+
+Then go to the directory with the Coq code:
+
+```
+cd coq
+```
+
+Install the `coq-evm` dependency including the definition of cryptographic primitives such as Keccak256:
+
+```
+third-party/coq-evm
+./configure
+make
+make install
+cd ../..
+```
+
+Compile and install the `CoqOfSolidity` library:
+
+```
+cd CoqOfSolidity
+make
+make install
+cd ..
+```
+
+You can now compile your generated `shallow.v` file, for example opening it in VSCode with the Coq extension installed.