Skip to content

Commit b4470bd

Browse files
desaperadosdesaperados
committed
Populating contracts pages
1 parent b521088 commit b4470bd

File tree

9 files changed

+341
-13
lines changed

9 files changed

+341
-13
lines changed

‎conf.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@
4747

4848
# General information about the project.
4949
project = u'RChain Architecture'
50-
copyright = u'2016, Ede Eykholt, Lucius Gregory Meredith, Joseph Denman'
50+
copyright = u'2016, RChain Co-op'
5151
author = u'Ede Eykholt, Lucius Gregory Meredith, Joseph Denman'
5252

5353
# The version info for the project you're documenting, acts as replacement for

‎contracts/applied-pi-calculus.rst‎

Lines changed: 85 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,85 @@
1+
.. _applied-pi-calculus:
2+
3+
################################################################################
4+
The Applied 𝛑-Calculus
5+
################################################################################
6+
7+
There are relatively few programming paradigms and languages that handle concurrent
8+
processes in their core model. Instead, they bolt on some kind of threading-based
9+
concurrency model to address being able to scale by doing more than one thing at a time.
10+
Mobile process calculi are the former. They provide one set of models, which we’ve chosen,
11+
that address concurrent processes in their core model. They provide a fundamentally
12+
different notion of what computing is. In these models, computing arises primarily
13+
from the interaction of processes.
14+
15+
The family of mobile process calculi provides an optimal foundation for a system of
16+
interacting processes. Among these models of computation, the π-calculus stands out.
17+
It models processes that send queries over channels. This approach maps very well onto
18+
today's Internet and has been used as the tool of choice for reasoning about a wide
19+
variety of concerns that are essential for distributed protocols.
20+
21+
==================
22+
Syntax
23+
==================
24+
25+
The π-calculus denotes names and processes where a name is either a channel of communication
26+
or a variable, and a process is a protocol of arbitrary size. The calculus gives a formal
27+
system to describe concurrent, communicating processes - a tool by which we can reason
28+
about concurrent systems before their implementation.
29+
30+
Given some notion of channel, the calculus builds a handful of basic forms of process, where
31+
P and Q are processes::
32+
33+
P,Q :: = 0
34+
| for (ptrn <- x). P
35+
| x!(m)
36+
| P|Q
37+
| (new x). P
38+
| (def X(ptrn) = P)[m]
39+
| X(m)
40+
41+
The first three terms are about I/O, describing the actions of message passing:
42+
43+
* :code:`0` is the form of the inert or stopped process that is the ground of the model
44+
45+
* :code:`for ( ptrn <- x ). P` is the form of an input-guarded process, :code:`P`, waiting
46+
for a message on channel :code:`x` that matches a pattern, ptrn. On receiving such a
47+
message, :code:`P` will execute in an environment where any variables in the pattern are
48+
bound to the values in the message
49+
50+
* :code:`x!( m )` is the form of sending a message, :code:`m`, on a channel, :code:`x`
51+
52+
The second three terms are about the concurrent nature of processes, the creation of channels,
53+
and recursion:
54+
55+
* :code:`(new x)P` is the form of a process that executes a subprocess, :code:`P`, in a context
56+
in which :code:`x` is bound to a fresh channel, distinct from all other channels in use
57+
58+
* :code:`(def X( ptrn ) = P)[ m ]` and :code:`X( m )`, these are the process forms for recursive
59+
definition and invocation
60+
61+
Note that *for* - comprehension is syntactic sugar for treating access to a channel monadically,
62+
by use of the *continuation* monad. The result is that channels are pattern-input guarded. The
63+
for-comprehension-based input can now be smoothly extended to input from multiple sources, each/all
64+
of which must pass a pattern filter, before the continuation is invoked. This extension as known
65+
as the *Applied π-calculus.*
66+
67+
Using a for-comprehension allows the input guarded semantics to be parametric in the monad used for
68+
channels, and hence the particular join semantics can be supplied polymorphically.
69+
70+
The for-comprehension also provides the proper setting in which to interpret Kiselyov’s LogicT monad
71+
transformer - searching down each input source until a tuple of inputs that satisfies the conditions
72+
is found. A means to programmatically describe interleaving policy is critical for reliable and
73+
performant services. This is the actual importance of LogicT. **Finally, now we have a syntactic
74+
form for nested transactions. Specifically, a process can only run in a context in which all of
75+
the state changes associated with the input sources and conditions are met**. Thus a programmer, or
76+
a program analyzer, can detect transaction boundaries syntactically. This is vital for contracts
77+
involving financial and other mission-critical transactions.
78+
79+
Getting concurrency right is hard, and support from this kind of typing discipline will be extremely
80+
valuable to ensure end-to-end correctness of a large system of communicating processes.
81+
82+
For more information, see The `Polyadic Pi-Calculus - A Tutorial`_ and `Higher Category Models of the Pi-Calculus`_.
83+
84+
.. _Polyadic Pi-Calculus - A Tutorial: http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/
85+
.. _Higher Category Models of the Pi-Calculus: https://arxiv.org/abs/1504.04311

‎contracts/index.rst‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,11 +2,10 @@
22
Contracts
33
################################################################################
44

5-
.. note::
6-
7-
Work in progress
8-
95
.. toctree::
106
:maxdepth: 2
117

128
contract-design.rst
9+
applied-pi-calculus.rst
10+
rho-calculus.rst
11+
rholang.rst

‎contracts/rho-calculus.rst‎

Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
.. _rho-calculus:
2+
3+
################################################################################
4+
The Rho-Calculus
5+
################################################################################
6+
7+
Even a model based on the applied π-calculus and equipped with a behavioral typing
8+
discipline is still not quite the best fit for a programming language for the
9+
decentralized Internet, let alone a contracting language for the blockchain.
10+
There’s another key ingredient: The rho-calculus.
11+
12+
Rho-calculus, a variant of the π-calculus, was introduced in 2004 and provided the
13+
first model of concurrent computation with reflection. 'Rho' stands for reflective,
14+
higher-order. Reflection is now widely recognized as a key feature of practical
15+
programming languages.
16+
17+
==================
18+
Syntax
19+
==================
20+
21+
Reflection is a disciplined way to turn programs into data that programs can operate
22+
on and then turn the modified data back into new programs.
23+
24+
To formalize this feature, the rho-calculus denotes names and processes where a name
25+
**may be a channel of communication, a variable, or a 'quoted' process of arbitrary
26+
size**::
27+
28+
P,Q :: = 0
29+
| for (ptrn <- x). P
30+
| x ⦉ P ⦊
31+
| ⌝ x ⌜
32+
| P|Q
33+
| (new x). P
34+
| (def X(ptrn) = P)[m]
35+
| X(m)
36+
37+
x, ptrn :: = ⌜P⌝
38+
39+
It provides two additional terms to enable reflection:
40+
41+
* :code:`⌜P⌝`, the 'Reflect' term, introduces the notion of a 'quoted process', which is a
42+
process that has been packaged up as a name, :code:`x`, or pattern :code:`ptrn`
43+
44+
* :code:`⌝ x ⌜`, the 'Reify' term, allows a quoted process to transform back into its
45+
original format
46+
47+
* The, :code:`x ⦉ P ⦊`, operator packages quoted processes and makes them available on
48+
channel, :code:`x`. It may interpreted as :code:`x!( ⌜P⌝ )`.
49+
50+
By this syntax, we may reason about concurrent systems where processes are passed around as
51+
first-class citizens. This syntax also gives the basic term language which will comprise
52+
the Rholang type system primitives. Note that channels have sophisticated internal structure
53+
and may, not exclusively, be used as data stores.
54+
55+
This model has been peer reviewed multiple times over the last ten years. Prototypes
56+
demonstrating its soundness have been available for nearly a decade. This extended syntax
57+
increases the set of contract building primitives to a grand total of nine primitives,
58+
far fewer than found in Solidity, Ethereum’s smart contracting language, yet the model is
59+
far more expressive than Solidity. In particular, Solidity-based smart contracts do not
60+
enjoy internal concurrency.
61+
62+
Java, C#, and Scala eventually adopted reflection as a core feature, and even OCaml and Haskell
63+
have ultimately developed reflective versions. The reason is simple: at industrial scale,
64+
programmers use programs to write programs. Without the computational leverage, it would
65+
take too long to write advanced industrial scale programs. Lisp programmers have known for
66+
decades how powerful this feature is. It simply took modern languages some time to catch up
67+
to that understanding.
68+
69+
The rho-calculus is the first computational model to combine all of these core requirements:
70+
behaviorally typed, fundamentally concurrent, message-passing model, with reflection. For
71+
details, see `A Reflective Higher-Order Calculus`_ and `Namespace Logic - A Logic for a Reflective Higher-Order Calculus`_.
72+
73+
.. _A Reflective Higher-Order Calculus: http://www.sciencedirect.com/science/article/pii/S1571066105051893
74+
.. _Namespace Logic - A Logic for a Reflective Higher-Order Calculus: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.95.9601

‎contracts/rholang.rst‎

Lines changed: 119 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,119 @@
1+
.. _rholang:
2+
3+
################################################################################
4+
Rholang - A Concurrent Smart Contracting Language
5+
################################################################################
6+
7+
Rholang is a fully featured, general purpose, Turing complete programming language
8+
built from the rho-calculus. It is a behaviorally typed, reflective, higher-order
9+
process language, and the official smart contracting language of RChain - its purpose
10+
is to concretize language-level concurrency.
11+
12+
Necessarily, the language is concurrency-oriented, with a focus on message-passing
13+
through input-guarded channels. Channels are statically typed and can be used as
14+
single message-pipes, streams, or data stores. Similar to typed functional languages,
15+
Rholang will support immutable data structures.
16+
17+
To get a taste of Rholang, here’s a contract named :code:`{Cell}` that holds a value
18+
and allows clients to get and set it:
19+
20+
.. code-block:: scala
21+
22+
contract Cell( get, set, state ) = {
23+
select {
24+
case rtn <- get; v <- state => {
25+
rtn!( *v ) | state!( *v ) | Cell( get, set, state )
26+
}
27+
case newValue <- set; v <- state => {
28+
state!( newValue ) | Cell( get, set, state )
29+
}
30+
}
31+
}
32+
33+
This contract takes a channel for {get} requests, a channel for {set} requests, and a
34+
{state} channel where we will hold a the data resource. It waits on the {get} and {set}
35+
channels for client requests. Client requests are pattern matched via {case} class.
36+
37+
Upon receiving a request, the contract joins {;} an incoming client with a request against
38+
the {state} channel. This join does two things. Firstly, it removes the internal {state}
39+
from access while this, in turn, serializes {get} and {set} actions, so that they are
40+
always operating against a single consistent copy of the resource - simultaneously providing
41+
a data resource synchronization mechanism and a memory of accesses and updates against the {state}.
42+
43+
In the {case} of {get}, a request comes in with a {rtn} channel where the value, {v}, in i
44+
{state} will be sent. Since {v} has been taken from the {state} channel, it is put back, and
45+
the {Cell} behavior is recursively invoked.
46+
47+
In the {case} of {set}, a request comes in with a {newValue}, which is published to the
48+
{state} channel (the old value having been stolen by the join). Meanwhile, the {Cell} behavior
49+
is recursively invoked.
50+
51+
Confirmed by {select}, only one of the threads in {Cell} can respond to the client request.
52+
It’s a race, and the losing thread, be it getter or setter, is killed. This way, when the
53+
recursive invocation of {Cell} is called, the losing thread is not hanging around, yet the new
54+
{Cell} process is still able to respond to either type of client request.
55+
56+
For an historical narrative leading up to Rholang, see `Mobile Process Calculi for Programming the Blockchain`_.
57+
58+
59+
.. _Mobile Process Calculi for Programming the Blockchain: https://docs.google.com/document/d/1lAbB_ssUvUkJ1D6_16WEp4FzsH0poEqZYCi-FBKanuY/edit
60+
61+
=================
62+
Behavioural Types
63+
=================
64+
65+
The task of creating a tractable and fault-tolerant execution environment for a
66+
system of communicating processes is non-trivial without a built-in mechanism to
67+
standardize the notion of 'safe' interaction among those processes.
68+
69+
Our intention from the beginning was to create a rho-bust language capable of
70+
expressing smart contracts with confidence. Our approach is correct-by-construction,
71+
'programs from theorems' language development. But to have true utility, Rholang
72+
had to be expressive and easy to reason about, which means that it had to boast
73+
a full-bodied typing discipline and include an automated formal spec. verification
74+
feature for mission-critical contracts. When we commit to the mobile process calculi,
75+
we are afforded those mechanisms in the form of 'Behavioral Types'.
76+
77+
Behavioral types represent a novel typing discipline that constrains not only the
78+
shape of input and output, but the permitted order of inputs and outputs among
79+
communicating and (possibly) concurrent processes. They exist to specify 'safe'
80+
interaction between objects in a composite system; we can think of an object
81+
(i.e. a process, channel, or variable), with an assigned behavioral type, as
82+
an object that is necessarily bound to operate in an authorized set of predictable
83+
and discrete interaction patterns.
84+
85+
.. note::
86+
87+
TODO: Example
88+
89+
Thereby, we can compose sub-processes while preserving their individual typings,
90+
which means that, whether the number of processes that execute (concurrently or not),
91+
between the time a transaction is initiated and the time it is verified, is one process,
92+
or 1,000,000 processes, correctness of data is always preserved. And that whether
93+
data is sent across the network to 1 location, or to 1,000,000 locations, correctness
94+
is preserved.
95+
96+
There are a number of additional benefits that we get for free with behavioral types:
97+
98+
System informatics analysis and optimization criterion for:
99+
100+
* Data/Information Flow
101+
* Control Flow
102+
* Resource Access Patterns
103+
* Capability based addressing
104+
105+
In their seminal paper, `Logic as a Distributive Law`_, Mike Stay & Gregory Meredith,
106+
develop an algorithm to iteratively generate a spatial-behavioral logic from any monadic
107+
data structure. The result is equivalent to a full-bodied type system decorated with
108+
modal logical operators, which can, not exclusively, be leveraged to generate a
109+
mathematically precise specification for polymorphic structure and behavior of processes.
110+
111+
The behavioral type systems Rholang will support make it possible to evaluate collections
112+
of contracts against how their code is shaped and how it behaves. As such, Rholang contracts
113+
elevate semantics to a type-level vantage point, where we are able to scope how entire
114+
protocols can safely interface.
115+
116+
For more information, see `Rholang Specification - Contracts, Composition, and Scaling`_.
117+
118+
.. _Logic as a Distributive Law: https://arxiv.org/pdf/1610.02247v3.pdf
119+
.. _Rholang Specification - Contracts, Composition, and Scaling: https://docs.google.com/document/d/1gnBCGe6KLjYnahktmPSm_-8V4jX53Zk10J-KFQl7mf8/edit#heading=h.k4bk2akncduu

‎glossary.rst‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,7 @@ Glossary
1616
concurrency
1717
The composition of independently operating processes
1818

19-
contract : contract
20-
smart contract : contract
19+
smart contract
2120
Loosely referred to as *contract*, a smart contract is a process, with a discrete
2221
state value, that resides at an address (i.e., a specific name) on RChain.
2322
Important to remember is that the term *contract* may refer to an atomic operation,

‎index.rst‎

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -19,9 +19,6 @@ community.
1919
developers who want to help see this vision realized, and for others who want to
2020
support these efforts.
2121

22-
Contents
23-
========
24-
2522
.. toctree::
2623
:maxdepth: 2
2724
:caption: Contents:

‎storage-and-query/index.rst‎

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,11 @@
22
Storage and Query
33
################################################################################
44

5-
.. note::
6-
7-
Work in progress
5+
The goal of this layer is to look like a local database with leased storage,
6+
asynchronously accessed, and to implement behind the scenes the aspects of
7+
decentralization and consensus.
88

99
.. toctree::
1010
:maxdepth: 2
11+
12+
special-k.rst

0 commit comments

Comments
 (0)