Skip to content

Commit

Permalink
Ported tutorial to readthedocs format.
Browse files Browse the repository at this point in the history
  • Loading branch information
mcoblenz committed Aug 27, 2019
1 parent bf3972e commit 26a28d9
Show file tree
Hide file tree
Showing 12 changed files with 498 additions and 11 deletions.
10 changes: 5 additions & 5 deletions user_guide/source/conf.py
Original file line number Diff line number Diff line change
Expand Up @@ -18,14 +18,14 @@

import sphinx_rtd_theme

# def setup(sphinx):
# from pygments_lexer_solidity import SolidityLexer
# sphinx.add_lexer('Solidity', SolidityLexer())
def setup(sphinx):
from pygments_lexer_obsidian import ObsidianLexer
sphinx.add_lexer('Obsidian', ObsidianLexer())

# -- Project information -----------------------------------------------------

project = u'Obsidian'
copyright = u'2019, Michael Coblenz'
copyright = u'2019, Michael Coblenz and Obsidian Project Contributors'
author = u'Michael Coblenz'

# The short X.Y version
Expand Down Expand Up @@ -77,7 +77,7 @@
# The name of the Pygments (syntax highlighting) style to use.
pygments_style = 'sphinx'

highlight_language = 'Solidity'
highlight_language = 'Obsidian'

# -- Options for HTML output -------------------------------------------------

Expand Down
9 changes: 3 additions & 6 deletions user_guide/source/index.rst
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@
.. toctree::
:maxdepth: 2
:maxdepth: 1
:hidden:

Getting Started <getting_started>
Expand All @@ -14,9 +14,6 @@



Indices and tables
==================
Obsidian is an object-oriented, strongly-typed language for smart contracts. Obsidian provides strong safety guarantees by using *typestate* and *linear types*.

* :ref:`genindex`
* :ref:`modindex`
* :ref:`search`
Even if you are highly experienced with OOP, you will find that Obsidian is very different from other languages you have used. Obsidian enables the compiler to reason about what states objects are in; by leveraging the power of the compiler, you can ensure that you only manipulate objects in ways that are appropriate for their current state. We recommend that you read the sections of the manual on *ownership* and *states* before you write your first Obsidian program.
30 changes: 30 additions & 0 deletions user_guide/source/tutorial/assets.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
Assets
======
Some owning references are to things that should not be accidentally lost. To prevent accidental loss, we can declare contracts
with the keyword ``asset``. Let's do this for ``Money``:

::

asset contract Money {
}

Now, if we accidentally lose track of an owning reference to a ``Money`` object (by letting it go out of scope without transferring ownership to somewhere else, such as a field), the compiler will give an error:

::

transaction test() {
Money m = ...; [m@Owned]; // OK, m is Owned here
// ERROR: cannot drop reference to owned asset m
}


We can fix this by (for example) returning m, assigning it to an owning field, or passing it as an argument to an appropriate transaction. For example:

::

transaction test() returns Money@Owned {
Money m = ...; [m@Owned]; // OK, m is Owned here
return m; // gives ownership of m to the caller of test()
}

NOTE: non-owning references to ``Money`` are not restricted; the compiler gives no errors when they go out of scope.
Binary file added user_guide/source/tutorial/ownership-diagram.png
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
61 changes: 61 additions & 0 deletions user_guide/source/tutorial/ownership1.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,61 @@
Ownership -- Introduction
=============================================================


.. highlight:: Obsidian



Our new programming language is object-oriented. It includes *contracts*, which are like classes, and can have *fields*
and *transactions*, analogous to member variables and functions respectively. As in other object-oriented languages,
there must be exactly one ``main contract``.
In addition, of the many variables or fields that reference objects, exactly *one* of them
can own the object, as seen in diagram *(a)* below. An object can have any number of Unowned references, and, if the object is not Owned,
it can have any number of Shared references (shown in *(b)* below). An object with Shared references can also have Unowned references,
but not Owned ones.

.. image:: ownership-diagram.png
:alt: Ownership
:width: 1000

In other words, the concept of ownership is having different types of references to an object. There are three different
types these references: ``Owned``, ``Unowned``, and ``Shared``.
Let's use money as an example. If you have $10, that money belongs to you -- you own it. This is the idea of an ``Owned`` reference.
You can show this money to anyone else; they can see the money, and talk about it, but they can't do anything with it --
they can't spend it, or save it, or add to it because it's not theirs. This is the idea of an ``Unowned`` reference; it's a reference to an object,
but doesn't have as much manipulative power over the object because it doesn't own the object. Now imagine the $10 is in a public pot that anyone can take from.
In this case, everyone shares ownership of the money; i.e., you all have ``Shared`` references to it. ``Shared`` references
are similar to normal references in other programming languages, and are the default ownership type if no permission is specified.


*Note that ownership ONLY applies to objects; primitive types (like ints, strings, booleans, etc.) do NOT have permissions.*


Continuing with money, here is an example of a contract (a ``Wallet``) with an object, a ``Money`` contract,
that has one ``Owned`` reference:

::

contract Money {
}

main contract Wallet {
Money @ Owned m; // @Owned indicates that the reference m owns the object it refers to
transaction spendMoney() {
...
}
}

Note that with this code alone, ``m`` is an ``Owned`` reference that doesn't actually point to any object. If we wanted to create a new object,
we would do it in a similar way to other object-oriented languages: ``m = new Money()``. Now, ``m`` is an Owned reference pointing to a
``Money`` object.


The compiler tracks ownership of each variable every time the variable is used. This information is part of the *type* of the variable. For example, the type of ``m`` is ``Money@Owned``. Information about ownership is NOT available at runtime; it is only available during compilation.


- If a reference is the only one that holds ownership, then it is ``Owned``.
- If all references to the object are the same (there is no owner), then each reference is ``Shared``.
- If a reference is NOT the owning one, but there might be another owning reference, then the reference is ``Unowned``.

70 changes: 70 additions & 0 deletions user_guide/source/tutorial/ownership2.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
Ownership -- Transactions
=============================================================


Transaction return types
------------------------

When transactions return objects, the type of the returned object must be annotated in the transaction declaration. For example:

::

transaction withdraw() returns Money@Owned {
// body not shown
return m; //where m is of type Money@Owned
}


If we did not return ``m`` within the transaction, or if ``m`` was not of type ``Money@Owned``, we would get an error.



Transaction parameters
------------------------
When a reference is passed to a transaction as an argument, the transaction's declaration specifies initial and final ownership with ``>>``.
If ``>>`` is not specified for a certain parameter, then the ownership of that parameter *doesn't change*. For example:

::

transaction spend(Money@Owned >> Unowned m) { // m is Owned initially but must be Unowned at the end.
// implementation not shown
};

transaction testSpend(Money@Owned >> Unowned m) {
spend(m);
// m is now of type Money@Unowned due to specification on spend() declaration.
}

transaction foo(Money@Owned m) { //this is the equivalent to Money@Owned >> Owned m
// body not shown
}

If a transaction expects an argument that is ``Unowned``, this means that the transaction cannot take ownership.
As a result, it is safe to pass an ``Owned`` reference as an argument to a transaction that expects an ``Unowned`` argument.
After the transaction returns, the caller still holds ownership.


For example, ``transaction bar(Money@Unowned m)`` can accept a
``Money`` reference with any ownership and the caller maintains whatever ownership it had initially when it called that transaction.


Transaction receivers (``this``)
---------------------------------
Sometimes the ownership of ``this`` (the ownership of this contract) needs to change in a transaction.
That can be specified by adding ``this`` as the first argument in the transaction declaration. Note that ``this`` is implicit,
and is not an actual parameter. For example:

::

contract Money {
transaction discard(Money@Owned >> Unowned this) {
disown this;
}
}

contract Wallet {
transaction throwAwayMoney(Money@Owned >> Unowned money) {
money.discard(); // 'this' argument is implicit; do not include it in transaction call.
}
}
70 changes: 70 additions & 0 deletions user_guide/source/tutorial/ownership3.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
Ownership -- Variables
=======================

Assignment
----------
Assignment (``=``) transfers ownership. That is, the variable on the left becomes the *new* owner, and the variable on the right loses ownership. For example:

::

Money m = ...; // m is Owned
Money newMoney = m; // m is Unowned, and newMoney is Owned
// Now m is of type Money@Unowned, not Money@Owned.


Fields
-------
*Field declarations* MUST include ownership specifications.

This means that at the END of each transaction, the permission (ownership status) of the object the field references MUST match the annotation on the field when it was *declared*. For example:

::

contract Wallet {
Money@Owned money; // Note that this annotation is on a field declaration!

// exchange removes (and returns) the current contents of the Wallet, replacing it with the input Money.
transaction exchange(Money@Owned >> Unowned otherMoney) returns Money@Owned {
Money temporaryMoney = money;
money = otherMoney;
return temporaryMoney;
}
}

NOTE: in the above example, ``money`` becomes ``Unowned`` in the ``exchange`` transaction when the ownership
is transferred to ``temporaryMoney``. However, by the end of the transaction, ``money`` gets ownership of ``otherMoney``,
so its permission at the end of the transaction still matches its permission where it was declared (as a field).


Local variables
----------------
Local variables (variables declared within transactions) are declared *WITHOUT* any ownership specified;
instead, you can optionally write compiler ownership checks ``[]`` to specify their ownership.
The compiler will output an error if the ownership does not match the check. For example:
::

transaction withdraw() returns Money@Owned {
// body not shown
}

transaction test() {
Money m = withdraw(); [m@Owned];
spend(m); [m@Unowned];
[m@Owned]; // COMPILE ERROR: m is Unowned here

Constructors
-------------
Constructors are specified just like in other object-oriented languages, but can include a permission.

Fields of a contract must be initialized in the constructor. For example:

::

contract Wallet {
Money@Owned money; // Note that this annotation is on a field declaration!

//Constructor, takes in a Money parameter
Wallet@Owned(Money@Owned >> Unowned initialMoney) {
money = initialMoney;
}
}
71 changes: 71 additions & 0 deletions user_guide/source/tutorial/ownership4.rst
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
Ownership -- Miscellaneous
============================

Ownership checks
-----------------
Ownership can be documented and checked by writing the ownership in brackets. For example, ``[m@Owned]`` indicates
that ``m`` is an owning reference at that particular point in the code. The compiler will generate an error if this
might not be the case. For example:


::

transaction spend(Money@Owned >> Unowned m) { // m is Owned initially but must be Unowned at the end.
// implementation not shown
}

transaction testSpend(Money@Owned >> Unowned m) {
spend(m); [m@Unowned]; // OK
[m@Owned]; // COMPILE ERROR: m is Unowned here
}

Ownership checks in ``[]`` *never* change ownership; they only document and check what is known.


Getting rid of ownership
--------------------------
If ownership is no longer desired, ``disown`` can be used to relinquish ownership. For example:
::

contract Money {
int amount;

transaction merge(Money@Owned >> Unowned mergeFrom) {
amount = amount + mergeFrom.amount;
disown mergeFrom; // We absorbed the value of mergeFrom, so the owner doesn't own it anymore.
}
}


Invoking transactions
----------------------
The compiler checks each invocation to make sure it is permitted according to the ownership of the transaction arguments. For example:

::

transaction spend(Money@Owned >> Unowned m) {
// implementation not shown
};
transaction print(Money@Unowned m) {
// implementation not shown
}

transaction test() {
Money m = ... // assume m is now owned.
print(m); // m is still Owned
spend(m); // m is now Unowned
spend(m); // COMPILE ERROR: spend() requires Owned input, but m is Unowned here
}


Handling Errors
-----------------
Errors can be flagged with ``revert``. A description of the error can be provided as well. An example of usage is given below.
::

transaction checkAmount(Money@Unowned m) {
if (m.getAmount() < 0) {
revert("Money must have an amount greater than 0");
}
}

0 comments on commit 26a28d9

Please sign in to comment.