From 732092b9523a072fc4f519fd592f0d3e5004cc62 Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Tue, 4 Jun 2019 03:13:24 -0700 Subject: [PATCH 1/8] Add first sketch of invariant draft. --- _drafts/2019-06-03-invariant-intro.md | 174 ++++++++++++++++++++++++++ 1 file changed, 174 insertions(+) create mode 100644 _drafts/2019-06-03-invariant-intro.md diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md new file mode 100644 index 0000000000..c79194b7e6 --- /dev/null +++ b/_drafts/2019-06-03-invariant-intro.md @@ -0,0 +1,174 @@ +--- +layout: post +title: Add your invariant to datopia +author: Christian Weilbach +summary: TODO +tags: blockchain clojure code datalog +date: 2019-06-03 12:00:00 +--- + + +# Motivation + +
+TODO +
+ +## Problem + +- databases often need invariants +- invariants are typically encoded in logic languages and verified with these + systems, e.g. type systems or formal verification (some references) +- databases already have a logic language +- but not used to encode logical constraints e.g. PostgresSQL triggers +- turing complete non-logic language, fully trusted in sandbox (might not + terminate), ugly (show how ugly?) +- deployment of invariants often require highly privileged access to the + database for this reason +- overall heavy to use and get right +- blockchains are all about invariants, addressing invariants for databases in + general provides us with a good solution for datopia + + +## Warmup example + + +- To explain: What is an invariant? + +- TODO sketch by drawing figures, then describe + +- have simple self-explaining datalog example + +- i like the idea of establishing some trivial graph theoretic property that + could be discussed in the context of a social network or dbpedia-style + ontology, because these are easy to visualize + +- e.g. detecting cycles in category hierarchies, or even something more trivial + like enforcing account-blocking rules for a social network - maybe that's too + trivial, but you get the idea. + + + +# Requirements + +- restrict write operations so that invariant is never violated, i.e. violating + transactions are rejected +- use logic language datalog itself to verify transaction data +- deterministic +- guaranteed to terminate +- automatically sandboxed through restricted query language environment +- exploit that naturally composable with datalog database query engine +- permissionless, invariants can be deployed by users/app developers: open schema, lightweight + + +# Accounting example + +- [accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of bookkeeping +- bitcoin as an invariant for attribute `:account/balance` +- asset transfer invariants + 1. Zero-Sum + 2. Positivity of Accounts + 3. Sender is spending + + +- TODO destructure +- explain subquery +- explain 4 types of databases passed + +~~~clojure +[:find ?matches . + :in $before $after $empty+txs $txs + :where + ;; run the sub-query + [(subquery [:find (sum ?balance-before) (sum ?balance-after) (sum ?balance-change) + :with ?affected-entity + :in $before $after $empty+txs $txs + :where + ;; Unify data from databases and transactions with affected-entity + [$after ?affected-entity :account/balance ?balance-after] + [$empty+txs ?affected-entity :account/balance ?balance-change] + [(get-else $before ?affected-entity :account/balance 0) ?balance-before] + + ;; 1. Zero-Sum + [(+ ?balance-change ?balance-before) ?computed-balance-after] + [(= ?balance-after ?computed-balance-after)] + + ;; 2. Positivity + [(>= ?balance-after 0)] + + ;; 3. Sender spending + #_[$txn _ :transaction/signed-by ?sender] + #_[(datopia.attribute-invariants/balance-check + ?sender ?affected-entity ?balance-before ?balance-after)]] + $before $after $empty+txs $txs) + [[?sum-before ?sum-after ?sum-change]]] + [(= ?sum-before ?sum-after)] + [(= ?sum-change sum-change-expected) ?matches]] +~~~ + + + +# Cost model for datopia + +- index accesses cost gas + + +# Extension + +- double accounting with transferring between different accounts under debit/credit + +# Try it out + +- datomic walk through (?) + +# Conclusion + + +# Maybe Related Work + +- Bitcoin +- Ethereum +- https://github.com/juxt/juxt-accounting + + +- Moe Prior Art: + - Postgres functionality (CREATE CONSTRAINT TRIGGER), for execution of arbitrary (unbounded) verification procedures per row or tx to determine fitness (in addition to first class pkey/fkey/uniqueness constraints, obv.). Triggers are obviously widespread, w/ some creative interpretations of the standard, though the ability to validate an entire transaction pre-commit (per postgres) is closer to Datopia & more interesting than column-level constraints for the types of invariants we're interested in enforcing + - RDF "Query shape maps" in Shacl - A lot of this stuff is buried under RDF-specific terminology and unlikely to be of much explanatory use when talking to a general audience, though it's conceptually pretty close, and looks like a less interesting/powerful graph validation scheme - e.g. "The query shape map extends the fixed shape map to enable simple pattern matching to select focus nodes from the data graph. This is done by permitting the node selectors to be either an RDF node as in a fixed map or a triple pattern. A triple pattern can have a focus keyword to represent the nodes that will be validated and a node or wildcard (represented by the underscore character _)." Some of the high level principles, like homoiconicity (you can validate everything, defining validation rules as triples) are cute http://book.validatingrdf.com/bookHtml010.html +- Other RDF-centric graph validation techniques using OWL dialects w/ varying + complexity/decidability guarantees. RDF is obviously not a technology widely + deployed in transaction processing systems, but there's some congruent + thinking + https://www.w3.org/TR/owl2-profiles/#Reasoning_in_OWL_2_RL_and_RDF_Graphs_using_Rules + + +# TODO incorporate prior discussions + +## UseCases + +- taken from https://github.com/datopia/planning/wiki/UseCases + +- MOE: Useful data should be put on chain to allow informed execution of bureaucracy. In general on chain data should be cheap and be provided easily. + +- Justin: Mineral rights are generally handled through small county clerk offices. Large oil companies need to go in and figure out who owns what. They employ a lot of folks called land men. + + +## Etherpad + +- Moe on flesh out code examples + +>>> It makes sense to me to use Datomic only in the samples, and note its applicability to Datahike, for publicity reasons. We can focus on its generality in title / intro, but should prob. pick a backend and stick with it for the code. + + +- Judith: invariants in other DBs + - some specific invariants are implemented in most schema-on-write DBs: not null, unique, foreign key, data type + - DBs using SQL often allow more extensive invariants being formulated: column and table constraints (CHECK and CONSTRAINT clauses), e.g. Postgres, MariaDB (give example of SQL statement?) + - MongoDB since schemaless/schema-on-read doesn't support invariant checks + + +- Moe on accounting + >>> I think accounting is much more appealing than travel expenses - happy to go with that. Unless we can think of an interesting invariant in which the triples represent something people naturally think of in terms of graphs - that might be easier to visualize. But nothing's really jumping out at me. Might be interesting to think of something impressively complex along those lines for a follow-up. + +- Moe on column only constraints +>>> We can work up to it, but the idea of transaction constraints (per the postgres point below) may be worth working up to incrementally - esp. b/c plsql stored procedures and whatever else you can evaluate in-db are potentially undecidable and unsandboxed (& perrhaps imperative/immune to advanced optimizations &c). conceptually trivial invariants like zero sum value transfer would require tx-level constraint triggers (i.e. multi-row) to enforce atomically in a relational database. once we introduce the requirement of hard determinism, general purpose validation languages are out, and once we introduce open schemas, SQL starts looking insanely verbose. I think a general, intuitive progression which terminates at a commonsense appeal to the necessity for deterministic, declarative, inferential transaction level constraints - before getting into any Datopia/Datalog specifics would be easy enough to follow. + + From b73526edb322eb5dd2f59bdabfdaf7a50142a4e1 Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Tue, 3 Sep 2019 01:52:13 -0700 Subject: [PATCH 2/8] Invariant post draft 1. --- _drafts/2019-06-03-invariant-intro.md | 309 ++++++++++++++++++++------ 1 file changed, 247 insertions(+), 62 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index c79194b7e6..ae03aba86b 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -1,6 +1,6 @@ --- layout: post -title: Add your invariant to datopia +title: Invariants as the essence of smart contracts author: Christian Weilbach summary: TODO tags: blockchain clojure code datalog @@ -8,32 +8,117 @@ date: 2019-06-03 12:00:00 --- -# Motivation +# Invariants -
-TODO +
"The principle of least action is the basic +variational principle of particle and continuum systems. In Hamilton's +formulation, a true dynamical trajectory of a system between an initial and +final configuration in a specified time is found by imagining all possible +trajectories that the system could conceivably take, computing the action (a +functional of the trajectory) for each of these trajectories, and selecting one +that makes the action locally stationary (traditionally called "least"). True +trajectories are those that have least action." +[Principle of Least Action, Scholarpedia](http://www.scholarpedia.org/article/Principle_of_least_action)
-## Problem - -- databases often need invariants -- invariants are typically encoded in logic languages and verified with these - systems, e.g. type systems or formal verification (some references) -- databases already have a logic language -- but not used to encode logical constraints e.g. PostgresSQL triggers -- turing complete non-logic language, fully trusted in sandbox (might not - terminate), ugly (show how ugly?) -- deployment of invariants often require highly privileged access to the - database for this reason -- overall heavy to use and get right -- blockchains are all about invariants, addressing invariants for databases in - general provides us with a good solution for datopia +Every complicated modern application uses one or multiple databases to manage +its internal state. These databases often carry powerful relational logic +engines like SQL or datalog for the user. Usually these query languages do much +of the hard work to extract information about a request from the large body of +accumulated knowledge efficiently, while the rest is glue code to expose the +information from the database to the surroundings. For this reason we will +provide light-client facility to selectively load index segments from the p2p +cloud directly into the client-side query engine. A current datahike prototype +is working with the help of the dat project, but we think other variants on IPFS +or [BitTorrent](http://www.bittorrent.org/) are also possible. TODO It is even +conceivable with technologies like [3df](https://github.com/sixthnormal/clj-3df) +that soon most user interfaces can be directly filled through an incrementally +updating materialized view on a client of the database. We are having a +collaboration working on support for 3df in datahike. Datopia will therefore +provide a straightforward extended datalog dialect to extract information on the +client without any additional server functionality. -## Warmup example - +# The change we need + +But what about adding new facts to datopia and changing the database? To supply +an interface to the user with similar ease as the query interface, we would have +to constrain it in a similar way. What if... we would use datalog also as a +language to just attach an invariant to each attribute to hold after the change? +On each transaction we can then check (in parallel) that the invariant for each +attribute hold after it. Since datalog is guaranteed to halt, compact to express +against a database of structured fact triples and in general considered powerful +enough to do most application logic, we can expose our `invariant` library +through the datomic or datahike transactor to the internet and let users deploy +invariants to the database that way similarly to smart contract systems like +Ethereum. To be sensible we of course also need to add a public-private key +based identification system and a cost model for the submission of transaction +data, which we will address briefly below. + +Why is this not possible with off-the-shelf PostgresSQL, CouchDB, MongoDB +datomic/datahike transactor functions or your favorite database? These databases +provide more powerful languages to express transaction operations because they +trust the code of the database is secured by manual selection of the +administrator. Besides being somewhat odd to use programming languages these +mechanisms are therefore all Turing-complete, which we consider unnecessary and +harmful for the suggested application to smart contract systems. A lot of effort +is spent to restrict functional languages to allow good smart contract +abstractions, yet we think simpler but almost equally expressive means have +barely been explored so far in a smart contract setting. + +Footnote: What if you could use SQL to check transactions into the same SQL +database? You should be able to build a similar library to `invariant` then. But +do you really not want to use a logic language with variables that allow a +compact implicit joins instead of throwing in another bunch of where clauses to +join over multiple "tables"? Datalog is so much more concise and easy to extend +by user-defined rules... + + +## Desiderata + +Ok, so after we have seen how we approach our database management setup, we +should summarize at least the following requirements that our `invariant` system +needs to satisfy: + +1. Our query results must be deterministic and verifiable by other peers later. +2. Each query must terminate. +3. The query might not interact with anything but the database. +4. We need to restrict write operations to a sandbox so that all invariants for + attributes changed by the transaction are maintained. +5. We use the concise logic language datalog to verify transaction data, because + it is composable with the database and has everything available. It is a + natural fit for the first 4 points. +6. Access to the system must be permissionless, i.e. everybody can create + identities, deploy invariants and add transactions. This can be arbitrarily + restricted more, e.g. by initially deploying invariants for identity related + transactions that need to be signed by some known entity or by replacing it + with a conventional identity management system like LDAP. +7. The schema for the database is extendable by each user for themselves through + public-private key cryptography. + + +We address the details of 6. in the following and 7. will be added for our +test-net implementation. + +## Invariant + +But can we really express all the smart contract examples out there into +datalog? What exactly is an an invariant? Invariants in general describe things +that stay the same. While we think that invariants are the most important +building blocks in describing interesting systems, e.g. for accounting, our +system is not limited to invariants, but can also verify properties that change +over time, maybe we should change the project name at some point (?). + +We have quite a bit of experience with datalog and we think that writing +reliable code with datalog is conceptually much more secure and better +understandable than in other smart contract environments. We note that almost +all interesting laws can be expressed as invariants, e.g. energy conservation in +physics. We are also able to extend datalog with custom extensions to provide +complicated logic efficiently without providing the full lambda calculus. TODO +link datafun + +# Warmup example -- To explain: What is an invariant? - TODO sketch by drawing figures, then describe @@ -48,80 +133,180 @@ TODO trivial, but you get the idea. +- explain 4 types of databases passed + + -# Requirements +# Accounting example -- restrict write operations so that invariant is never violated, i.e. violating - transactions are rejected -- use logic language datalog itself to verify transaction data -- deterministic -- guaranteed to terminate -- automatically sandboxed through restricted query language environment -- exploit that naturally composable with datalog database query engine -- permissionless, invariants can be deployed by users/app developers: open schema, lightweight +Let's move on to the more practical example of accounting. +[Accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of +bookkeeping that has been around since humans have tracked their possessions. +For simplicity we will model an asset we call `datacoin`. To deploy our contract +we use again our public key prefix `0x74703/datacoin`. +In the spirit of logic programming we again do not describe how to do an asset +transfer, we only need to describe what properties need to be fulfilled for it +to be valid. Assuming asset transfer transactions have authenticated senders, +e.g. by public-private key cryptography that is provided by the system, we need +at least the following three invariants to have a contract in place that I would +risk putting money in: -# Accounting example +1. Zero-Sum +2. Positivity of Accounts +3. Sender is spending -- [accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of bookkeeping -- bitcoin as an invariant for attribute `:account/balance` -- asset transfer invariants - 1. Zero-Sum - 2. Positivity of Accounts - 3. Sender is spending +Zero-Sum means that after each transaction the total sum of assets in the system +should not change. Positivity of accounts means that you cannot overdraft your +account into a negative balance. Finally only a signing sender can spend money +in a transaction. + +The full invariant for `0x74703/datacoin` then looks like: - -- TODO destructure -- explain subquery -- explain 4 types of databases passed - ~~~clojure [:find ?matches . :in $before $after $empty+txs $txs :where ;; run the sub-query - [(subquery [:find (sum ?balance-before) (sum ?balance-after) (sum ?balance-change) - :with ?affected-entity + [(subquery [:find (sum ?balance-before) + (sum ?balance-after) + (sum ?balance-change) + :with ?affected-account :in $before $after $empty+txs $txs :where - ;; Unify data from databases and transactions with affected-entity - [$after ?affected-entity :account/balance ?balance-after] - [$empty+txs ?affected-entity :account/balance ?balance-change] - [(get-else $before ?affected-entity :account/balance 0) ?balance-before] - - ;; 1. Zero-Sum - [(+ ?balance-change ?balance-before) ?computed-balance-after] - [(= ?balance-after ?computed-balance-after)] + ;; Unify data from databases and transactions with affected-account + [$after ?affected-account :0x74703.account/balance ?balance-after] + [$empty+txs ?affected-account :0x74703.account/balance ?balance-change] + [(get-else $before ?affected-account :0x74703.account/balance 0) ?balance-before] ;; 2. Positivity [(>= ?balance-after 0)] ;; 3. Sender spending - #_[$txn _ :transaction/signed-by ?sender] - #_[(datopia.attribute-invariants/balance-check - ?sender ?affected-entity ?balance-before ?balance-after)]] + [$txs _ _ :transaction/signed-by ?sender] + [(= ?sender ?affected-account) ?is-sender] + [(>= ?balance-change 0) ?pos-change] + [(or ?is-sender ?pos-change)]] $before $after $empty+txs $txs) [[?sum-before ?sum-after ?sum-change]]] + ;; 1. Zero-Sum aggregated [(= ?sum-before ?sum-after)] [(= ?sum-change sum-change-expected) ?matches]] ~~~ +Let's break it down. First we note that we support a `subquery` functionality by +our invariant library for both Datomic and datahike. The subquery here unifies +the database against each `?affected-account`. It first binds the respective +balances from the supplied databases. This is effectively an extension of +datalog with aggregation. Additionally it provides a form of lambda abstraction +that can be reused and adjusted to custom arguments and return types. + +Note that these attributes are easy to describe on a systematic level, but we +have for instance never defined between how many participants these transactions +happen and how they should be supplied to the system or which other transactions +they are transacted with. By splitting up the constraints by attribute we can +achieve compositionality between constraints of different attributes, because +they can also reason about each other. + +Finally the 4 different representations, $before, $after, $empty+txs and $txs, +allow to optimize the calculation of each invariant by different representations +of the change applied to the database. $before and $after work well for +selective queries, but might be prohibitively expensive to aggregate. For this +reason $empty+txs allows to reason about an empty database populated only with +this transaction data and finally about the list of transactions themselves. We +think this setup is sufficient to express many common invariants conveniently +and efficiently. + +## Extension + +It is equally easy to do double accounting in the same system by booking things +under respective debit and credit attributes. That way a similar zero-sum +predicate can be used to ensure that all accounts stay consistent. This is left +as an exercise to the reader :). + + +# Design aspects + +## Cost model for datopia + +Reading from datopia will not cost anything as the database is replicated over a +p2p network freely. Writing to the database costs the execution of invariant +queries for each modified attribute though. We have not defined a full cost +model for aggregation yet, but we know already that generally index accesses +will cost most gas. This is in contrast to low-level gas models like Ethereum, +because we optimize for resources that are used after compiling a very efficient +executable of the contract in form of a query plan. The CPU time that is +required to operate the query engine is negligible compared to the cost to +access the underlying storage. By decoupling of the resource cost model we can +improve the runtime. Suppliers of transactions will automatically reap the +benefits without any changes to the deployed invariants. We assume that that way +many invariants stay attractive for long periods of time. This is in contrast to +Ethereum, which specifies a cost model on instruction level, which means that +the overlaying code needs to be recompiled to use less resources when new +optimizations are added to the library or compiler. + +## Deployment of invariants + +How do we deploy invariants into the system then in the first place? We need to +make sure that the deployed code does not harm the system when it is executed +and that the code artifact does not affect the queries of other users. To make +sure that the deployed code does not harm the system we parse it and check that +it only uses our supported set of datalog clauses and aggregates. Since these +are not able to affect the environment and are guaranteed to halt every provider +of the system should feel fine to accept them if a (profitable) fee is provided. +We will even add a good, established datalog query planning framework to ensure +that each query will complete by upperbounding the costs of the query plan +upfront. This is incredibly hard to do for Turing-complete programming +languages, even if they have a strong type system. + +Since adding an invariant is just another form of transaction and its addition +happens under the namespace of a public-key id of the sender, we need not +constrain users from supplying invariants. We can just ask to pay a minimum fee +for the IO operations that it costs to add one or a bunch of such contracts. It +will not pollute other index fragments, potentially causing additional costs to +other people's data or queries. And while in most blockchain systems users need +to fetch all data transacted to read arbitrarily from the blockchain, in datopia +it is enough to follow the Merkle proof to the leafs of each index tree. + +Footnote: +Technically we also need a way to verify the root of the tree, we can conceive +one way to do so by using a closed consensus system like Cosmos/Tendermint so +clients will be able to tell easily whether a block is valid by following the +global sequence and checking the majority validation of the root. + + +## Optimal interface + +We speculate that with most meaningful contracts and apps, the partition in +index fragments will be almost information theoretically optimal for clients, +because the query plan will be minimized by detailed statistics of the +distribution of each attribute and these should cluster as well as they do for +conventional applications. In other words each client will only download the +data it needs from the giant database (plus an approximately constant size +overhead). Additionally we will gain the same expressivity as for the original +query language and at benefit from all optimizations to the query planner. + + +We want this interface to be wildly available. In fact it is a middleware for +both datomic and datahike right now and can be combined with different +transactor implementations based on Cosmos/Tendermint, a proof-of-work based +transactor or a managed, privileged set of servers. In other words datopia can +run in any combination with a transaction mechanism. It is demonstrating one way +to expose the query language to the transactor to achieve our objectives. -# Cost model for datopia -- index accesses cost gas +# Try it out +Link to repo with datomic walk through (?) -# Extension +# Conclusion + +... -- double accounting with transferring between different accounts under debit/credit -# Try it out -- datomic walk through (?) -# Conclusion # Maybe Related Work From c640b6fef5cb0947011e3f9806e4c42cc219e215 Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Tue, 3 Sep 2019 02:04:12 -0700 Subject: [PATCH 3/8] Small fixes and smoothing. --- _drafts/2019-06-03-invariant-intro.md | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index ae03aba86b..3e8b8d91fe 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -2,13 +2,12 @@ layout: post title: Invariants as the essence of smart contracts author: Christian Weilbach -summary: TODO +summary: Expressing invariants with datalog provides a powerful smart contract system. tags: blockchain clojure code datalog -date: 2019-06-03 12:00:00 +date: 2019-09-01 12:00:00 --- -# Invariants
"The principle of least action is the basic variational principle of particle and continuum systems. In Hamilton's @@ -18,7 +17,7 @@ trajectories that the system could conceivably take, computing the action (a functional of the trajectory) for each of these trajectories, and selecting one that makes the action locally stationary (traditionally called "least"). True trajectories are those that have least action." -[Principle of Least Action, Scholarpedia](http://www.scholarpedia.org/article/Principle_of_least_action) +Principle of Least Action, Scholarpedia
Every complicated modern application uses one or multiple databases to manage @@ -44,16 +43,15 @@ client without any additional server functionality. But what about adding new facts to datopia and changing the database? To supply an interface to the user with similar ease as the query interface, we would have to constrain it in a similar way. What if... we would use datalog also as a -language to just attach an invariant to each attribute to hold after the change? -On each transaction we can then check (in parallel) that the invariant for each -attribute hold after it. Since datalog is guaranteed to halt, compact to express -against a database of structured fact triples and in general considered powerful -enough to do most application logic, we can expose our `invariant` library -through the datomic or datahike transactor to the internet and let users deploy -invariants to the database that way similarly to smart contract systems like -Ethereum. To be sensible we of course also need to add a public-private key -based identification system and a cost model for the submission of transaction -data, which we will address briefly below. +language to just attach an invariant to each relation to hold after the change? +Since datalog is guaranteed to halt, compact to express against a database of +structured fact triples and in general considered powerful enough to do most +application logic, we can expose our `invariant` library through the datomic or +datahike transactor to the internet and let users deploy invariants to the +database that way similarly to smart contract systems like Ethereum. To be +sensible we of course also need to add a public-private key based identification +system and a cost model for the submission of transaction data, which we will +address briefly below. Why is this not possible with off-the-shelf PostgresSQL, CouchDB, MongoDB datomic/datahike transactor functions or your favorite database? These databases From a23f7058e0aad1dbaae28bb1e0db4789162932fb Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Tue, 3 Sep 2019 11:05:35 -0700 Subject: [PATCH 4/8] Improve introduction. --- _drafts/2019-06-03-invariant-intro.md | 34 ++++++++++++++++++--------- 1 file changed, 23 insertions(+), 11 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index 3e8b8d91fe..e9d3903ba9 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -7,8 +7,6 @@ tags: blockchain clojure code datalog date: 2019-09-01 12:00:00 --- - -
"The principle of least action is the basic variational principle of particle and continuum systems. In Hamilton's formulation, a true dynamical trajectory of a system between an initial and @@ -17,25 +15,39 @@ trajectories that the system could conceivably take, computing the action (a functional of the trajectory) for each of these trajectories, and selecting one that makes the action locally stationary (traditionally called "least"). True trajectories are those that have least action." -Principle of Least Action, Scholarpedia +Principle of Least Action describing invariants in physics, Scholarpedia
+We have described in a [prior +blogpost](/2018/11/03/blockchain-information-system/) the appeal of a datalog +based database in a typical blockchain setting with the addition of access to a +versioned history of it. In this blog post we will talk about how datopia can be +managed by a novel, yet simple, datalog based transaction system that is, in our +opinion, much more fit for smart contract purposes than all other approaches +known to us. + Every complicated modern application uses one or multiple databases to manage its internal state. These databases often carry powerful relational logic engines like SQL or datalog for the user. Usually these query languages do much of the hard work to extract information about a request from the large body of accumulated knowledge efficiently, while the rest is glue code to expose the -information from the database to the surroundings. For this reason we will -provide light-client facility to selectively load index segments from the p2p -cloud directly into the client-side query engine. A current datahike prototype -is working with the help of the dat project, but we think other variants on IPFS -or [BitTorrent](http://www.bittorrent.org/) are also possible. TODO It is even +information from the database to the surroundings. Since our database technology +stores immutable facts, datopia instead provides support to selectively load +index segments from the P2P cloud directly into the client-side query engine. +Datopia will therefore automatically provide a straightforward extended datalog +dialect to extract information on the client without the need for any +intermediary server or client functionality. The programming model to read from +the database is elegantly established that way. + + +Footnote: A datahike client replication prototype is working with the help of +the [dat project](https://dat.foundation/) because of its publish and subscribe +system, but we think other variants on [IPFS](https://ipfs.io/) or +[BitTorrent](http://www.bittorrent.org/) are also possible. It is even conceivable with technologies like [3df](https://github.com/sixthnormal/clj-3df) that soon most user interfaces can be directly filled through an incrementally updating materialized view on a client of the database. We are having a -collaboration working on support for 3df in datahike. Datopia will therefore -provide a straightforward extended datalog dialect to extract information on the -client without any additional server functionality. +collaboration working on support for 3df in datahike. # The change we need From 640265c6cb167fa8d894f469a20d5904d53cfa5b Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Tue, 3 Sep 2019 21:31:40 -0700 Subject: [PATCH 5/8] s/wildly/widely/ --- _drafts/2019-06-03-invariant-intro.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index e9d3903ba9..bd222ffbfd 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -294,10 +294,10 @@ distribution of each attribute and these should cluster as well as they do for conventional applications. In other words each client will only download the data it needs from the giant database (plus an approximately constant size overhead). Additionally we will gain the same expressivity as for the original -query language and at benefit from all optimizations to the query planner. +query language with the benefit from all optimizations to the query planner. -We want this interface to be wildly available. In fact it is a middleware for +We want this interface to be widely available. In fact it is a middleware for both datomic and datahike right now and can be combined with different transactor implementations based on Cosmos/Tendermint, a proof-of-work based transactor or a managed, privileged set of servers. In other words datopia can From 0c341832353de8a178cfd817017b066a3a305ae2 Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Thu, 19 Sep 2019 04:23:55 -0700 Subject: [PATCH 6/8] Update draft. --- _drafts/2019-06-03-invariant-intro.md | 321 +++++++++++++++----------- 1 file changed, 185 insertions(+), 136 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index bd222ffbfd..1f07810979 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -1,12 +1,18 @@ --- layout: post -title: Invariants as the essence of smart contracts +title: Invariants - Smart Contracts distilled author: Christian Weilbach -summary: Expressing invariants with datalog provides a powerful smart contract system. -tags: blockchain clojure code datalog +summary: Expressing invariants with Datalog provides a powerful smart contract system. +tags: blockchain clojure code Datalog date: 2019-09-01 12:00:00 --- + +
"The principle of least action is the basic variational principle of particle and continuum systems. In Hamilton's formulation, a true dynamical trajectory of a system between an initial and @@ -15,124 +21,168 @@ trajectories that the system could conceivably take, computing the action (a functional of the trajectory) for each of these trajectories, and selecting one that makes the action locally stationary (traditionally called "least"). True trajectories are those that have least action." -Principle of Least Action describing invariants in physics, Scholarpedia +Principle of Least Action describing invariants in Physics, Scholarpedia
-We have described in a [prior -blogpost](/2018/11/03/blockchain-information-system/) the appeal of a datalog -based database in a typical blockchain setting with the addition of access to a -versioned history of it. In this blog post we will talk about how datopia can be -managed by a novel, yet simple, datalog based transaction system that is, in our -opinion, much more fit for smart contract purposes than all other approaches -known to us. - -Every complicated modern application uses one or multiple databases to manage -its internal state. These databases often carry powerful relational logic -engines like SQL or datalog for the user. Usually these query languages do much -of the hard work to extract information about a request from the large body of -accumulated knowledge efficiently, while the rest is glue code to expose the -information from the database to the surroundings. Since our database technology -stores immutable facts, datopia instead provides support to selectively load -index segments from the P2P cloud directly into the client-side query engine. -Datopia will therefore automatically provide a straightforward extended datalog -dialect to extract information on the client without the need for any -intermediary server or client functionality. The programming model to read from -the database is elegantly established that way. - - -Footnote: A datahike client replication prototype is working with the help of -the [dat project](https://dat.foundation/) because of its publish and subscribe -system, but we think other variants on [IPFS](https://ipfs.io/) or -[BitTorrent](http://www.bittorrent.org/) are also possible. It is even -conceivable with technologies like [3df](https://github.com/sixthnormal/clj-3df) -that soon most user interfaces can be directly filled through an incrementally -updating materialized view on a client of the database. We are having a -collaboration working on support for 3df in datahike. +We have [previously established](/2018/11/03/blockchain-information-system/) the +appeal of a [Datalog based database](https://en.wikipedia.org/wiki/Datalog) in a +blockchain setting. In summary, simplicity must be a [core design +principle](https://www.infoq.com/presentations/Simple-Made-Easy) to manage +complexity in (distributed) information systems. In the following we will lay +out how datopia can be managed by a novel, yet very simple transaction system. +We will first give a motivation for our work and how it relates to other +technologies, then describe its implementation with a simple example and a +real-world accounting contract and finally look at design aspects like cost +models and finally we conclude. Since our concept is useful both in datomic and +datahike, we provide it as a light-weight library that is used by Datopia +instances. + + +# Motivation + + + +Almost every contemporary, partially automated social process uses one or more +databases to manage its internal state. These databases often provide powerful +relational logic languages like [SQL](http://www.mysql.com) or +[Datalog](http://datomic.com) to the user. Usually these query languages do most +of the hard work to extract information for a query, efficiently scanning the +large body of accumulated knowledge. The rest of the application is often glue +code to expose the information from the database to the surroundings in form of +user interfaces or APIs and manage access to it. The fact that each database is +contained in a silo that way requires endless, slow and error-prone integration +between different systems. + +Datopia instead provides support to selectively load index segments from a swarm +of peers directly into the client-side query engine. Our Datalog query engine +does not distinguish between the data hosted in datopia or locally hosted +private databases in [datahike](https://github.com/replikativ/datahike), in +other words an arbitrary number of databases can be joint at query time at the +reader. The system composes by datalog semantics and the efficiency of its query +planning. [We conceptualize](https://www.youtube.com/watch?v=A2CZwOHOb6U) +Datalog as a universal language for distributed systems. Datopia will therefore +automatically provide a straightforward extended Datalog dialect to extract +information on the client without the need for any intermediary server or client +functionality. Since indices are managed by [immutable data +structures](https://blog.datopia.io/2018/11/03/hitchhiker-tree/) this reading +pattern is totally decoupled and arbitrarily read scalable. [^1] + + + + +[^1]: A datahike client replication prototype is working on top of the [dat + project](https://dat.foundation/) using its publish and subscribe system, + but we think other variants on [IPFS](https://ipfs.io/) or + [BitTorrent](http://www.bittorrent.org/) are also possible. It is even + conceivable with technologies like + [3df](https://github.com/sixthnormal/clj-3df) that soon most user interfaces + can be directly filled through an incrementally updating materialized view + on a client of the database. We are having a collaboration working on + support for 3df in datahike. -# The change we need +# Adding facts to Datopia But what about adding new facts to datopia and changing the database? To supply an interface to the user with similar ease as the query interface, we would have -to constrain it in a similar way. What if... we would use datalog also as a -language to just attach an invariant to each relation to hold after the change? -Since datalog is guaranteed to halt, compact to express against a database of -structured fact triples and in general considered powerful enough to do most -application logic, we can expose our `invariant` library through the datomic or -datahike transactor to the internet and let users deploy invariants to the -database that way similarly to smart contract systems like Ethereum. To be -sensible we of course also need to add a public-private key based identification -system and a cost model for the submission of transaction data, which we will -address briefly below. +to constrain it in a similar way. What if... we would use Datalog also as a +language to just attach an invariant to each relation? Since Datalog is +guaranteed to halt, compact to express against a database of structured fact +triples and in general considered powerful enough to do most application logic, +we can expose our [invariant](https://github.com/datopia/invariant) library +through the datomic or datahike transactor to the network and let users deploy +invariants to the database similarly to smart contract systems like Ethereum. To +be sensible we of course also need to add a public-private key based +identification system and a cost model for the submission of transaction data, +which we will sketch below. Why is this not possible with off-the-shelf PostgresSQL, CouchDB, MongoDB -datomic/datahike transactor functions or your favorite database? These databases -provide more powerful languages to express transaction operations because they -trust the code of the database is secured by manual selection of the -administrator. Besides being somewhat odd to use programming languages these -mechanisms are therefore all Turing-complete, which we consider unnecessary and -harmful for the suggested application to smart contract systems. A lot of effort -is spent to restrict functional languages to allow good smart contract -abstractions, yet we think simpler but almost equally expressive means have -barely been explored so far in a smart contract setting. - -Footnote: What if you could use SQL to check transactions into the same SQL -database? You should be able to build a similar library to `invariant` then. But -do you really not want to use a logic language with variables that allow a -compact implicit joins instead of throwing in another bunch of where clauses to -join over multiple "tables"? Datalog is so much more concise and easy to extend -by user-defined rules... +datomic or datahike transactor functions or your favorite database? These +databases provide more powerful languages to express transaction operations +because they trust the code of the database is secured by careful manual +safe-guarding of the administrator. Besides being [somewhat +odd](https://www.postgresql.org/docs/current/sql-createfunction.html) to use +programming languages these mechanisms are therefore all Turing-complete, which +we consider unnecessary and harmful for most practical purposes. A lot of effort +is spent to restrict +[functional](https://iohk.io/research/papers/#marlowe-financial-contracts-on-blockchain) +or +[imperative](https://solidity.readthedocs.io/en/v0.5.11/solidity-by-example.html) +languages to allow feasible smart contract abstractions, yet we think much +simpler but almost equally expressive means have barely been explored so far in +a smart contract setting. Arguably a lot of the current effort is trying to +reduce most of these more expressive semantics to something that looks a lot +like Datalog, but is still harder to reason about than a simple language like +Datalog. [^2] + +[^2]: What if you could use SQL to check transactions into the same SQL + database? You should be able to build a similar library to `invariant` then. But + do you really not want to use a logic language with variables that allow a + compact implicit joins instead of throwing in another bunch of where clauses to + join over multiple "tables"? Datalog is so much more concise and easy to extend + by user-defined rules... ## Desiderata -Ok, so after we have seen how we approach our database management setup, we -should summarize at least the following requirements that our `invariant` system -needs to satisfy: +Let's define a minimal set of requirements that each `invariant` query needs to +satisfy: 1. Our query results must be deterministic and verifiable by other peers later. -2. Each query must terminate. +2. Each query must terminate. This means it cannot be [Turing + complete](https://en.wikipedia.org/wiki/Turing_completeness). Most smart + contract language achieve this through a resource model, e.g. by requiring + gas to run. Datalog on the other hand allows to determine ahead of time how + many resources will be needed for a query. 3. The query might not interact with anything but the database. 4. We need to restrict write operations to a sandbox so that all invariants for attributes changed by the transaction are maintained. -5. We use the concise logic language datalog to verify transaction data, because - it is composable with the database and has everything available. It is a - natural fit for the first 4 points. -6. Access to the system must be permissionless, i.e. everybody can create - identities, deploy invariants and add transactions. This can be arbitrarily - restricted more, e.g. by initially deploying invariants for identity related - transactions that need to be signed by some known entity or by replacing it - with a conventional identity management system like LDAP. +5. The language for invariants must have meaningful and efficient access to the + database. +6. Access to the system must be operable in a permissionless setting, i.e. + potentially anybody can register, deploy invariants and add transactions for + a fee. This can be flexibly restricted, e.g. by regulating access through + another trusted system. 7. The schema for the database is extendable by each user for themselves through public-private key cryptography. - -We address the details of 6. in the following and 7. will be added for our -test-net implementation. +We naturally use our concise query language Datalog to verify transaction data. +The Datalog flavor implemented by datahike is a natural fit for the first 5 +points, in particular its combination with hitchhiker trees. We address the +details of 6 in the following and 7 will be added for our test-net +implementation. ## Invariant -But can we really express all the smart contract examples out there into -datalog? What exactly is an an invariant? Invariants in general describe things -that stay the same. While we think that invariants are the most important +What exactly is an an invariant? Invariants in general describe things that stay +the same. While we think that fairly simple invariants are the most important building blocks in describing interesting systems, e.g. for accounting, our -system is not limited to invariants, but can also verify properties that change -over time, maybe we should change the project name at some point (?). - -We have quite a bit of experience with datalog and we think that writing -reliable code with datalog is conceptually much more secure and better -understandable than in other smart contract environments. We note that almost -all interesting laws can be expressed as invariants, e.g. energy conservation in -physics. We are also able to extend datalog with custom extensions to provide -complicated logic efficiently without providing the full lambda calculus. TODO -link datafun +system can also express invariants that describe complicated dynamics, e.g. that +a value must be counted up on each change. This is possible because the +invariant queries can reason about the change itself. + +But can we really express all the smart contract examples out there in Datalog? +Our team has years of commercial and scientific experience with Datalog and we +believe that writing reliable code with Datalog is conceptually much more secure +and better understandable than in other smart contract environments. Datalog is +used in [large scale program verification](https://semmle.com/) for good +reasons. We also want to note that almost all interesting laws can be expressed +as invariants, e.g. energy conservation in physics. In case some primitives will +be missing it is as easy to add additional primitives as adding a pure Clojure +function to the datopia runtime and whitelisting it. Extensions with safe forms +of λ-calculus similar to [datafun](https://github.com/rntz/datafun) are possible +as well. # Warmup example - TODO sketch by drawing figures, then describe -- have simple self-explaining datalog example +- have simple self-explaining Datalog example - i like the idea of establishing some trivial graph theoretic property that could be discussed in the context of a social network or dbpedia-style @@ -153,14 +203,15 @@ Let's move on to the more practical example of accounting. [Accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of bookkeeping that has been around since humans have tracked their possessions. For simplicity we will model an asset we call `datacoin`. To deploy our contract -we use again our public key prefix `0x74703/datacoin`. +we use our public key prefix `0x64703/datacoin`. -In the spirit of logic programming we again do not describe how to do an asset -transfer, we only need to describe what properties need to be fulfilled for it -to be valid. Assuming asset transfer transactions have authenticated senders, -e.g. by public-private key cryptography that is provided by the system, we need -at least the following three invariants to have a contract in place that I would -risk putting money in: +We do not need to describe how to do an asset transfer, we only need to describe +what properties need to be fulfilled for it to be valid. The submitter of the +transaction data can use any program to generate the transaction data that will +be submitted later. Assuming asset transfer transactions have authenticated +senders, e.g. by public-private key cryptography that is provided by the system, +we need at least the following three invariants to have a contract in place that +I would risk putting money in: 1. Zero-Sum 2. Positivity of Accounts @@ -171,7 +222,7 @@ should not change. Positivity of accounts means that you cannot overdraft your account into a negative balance. Finally only a signing sender can spend money in a transaction. -The full invariant for `0x74703/datacoin` then looks like: +The full invariant for `0x64703/datacoin` then looks like: ~~~clojure [:find ?matches . @@ -185,9 +236,9 @@ The full invariant for `0x74703/datacoin` then looks like: :in $before $after $empty+txs $txs :where ;; Unify data from databases and transactions with affected-account - [$after ?affected-account :0x74703.account/balance ?balance-after] - [$empty+txs ?affected-account :0x74703.account/balance ?balance-change] - [(get-else $before ?affected-account :0x74703.account/balance 0) ?balance-before] + [$after ?affected-account :0x64703.account/balance ?balance-after] + [$empty+txs ?affected-account :0x64703.account/balance ?balance-change] + [(get-else $before ?affected-account :0x64703.account/balance 0) ?balance-before] ;; 2. Positivity [(>= ?balance-after 0)] @@ -208,7 +259,7 @@ Let's break it down. First we note that we support a `subquery` functionality by our invariant library for both Datomic and datahike. The subquery here unifies the database against each `?affected-account`. It first binds the respective balances from the supplied databases. This is effectively an extension of -datalog with aggregation. Additionally it provides a form of lambda abstraction +Datalog with aggregation. Additionally it provides a form of lambda abstraction that can be reused and adjusted to custom arguments and return types. Note that these attributes are easy to describe on a systematic level, but we @@ -227,6 +278,7 @@ this transaction data and finally about the list of transactions themselves. We think this setup is sufficient to express many common invariants conveniently and efficiently. + # Design aspects ## Cost model for datopia Reading from datopia will not cost anything as the database is replicated over a -p2p network freely. Writing to the database costs the execution of invariant -queries for each modified attribute though. We have not defined a full cost -model for aggregation yet, but we know already that generally index accesses -will cost most gas. This is in contrast to low-level gas models like Ethereum, -because we optimize for resources that are used after compiling a very efficient -executable of the contract in form of a query plan. The CPU time that is -required to operate the query engine is negligible compared to the cost to +peer to peer network freely. Writing to the database costs the execution of +invariant queries for each modified attribute though. We have not defined a full +cost model for aggregation yet, but we know already that generally index +accesses will cost most gas. This is in contrast to low-level gas models like +Ethereum, because we optimize for resources that are used after compiling a very +efficient executable of the contract in form of a query plan. The CPU time that +is required to operate the query engine is negligible compared to the cost to access the underlying storage. By decoupling of the resource cost model we can improve the runtime. Suppliers of transactions will automatically reap the benefits without any changes to the deployed invariants. We assume that that way @@ -261,40 +314,40 @@ How do we deploy invariants into the system then in the first place? We need to make sure that the deployed code does not harm the system when it is executed and that the code artifact does not affect the queries of other users. To make sure that the deployed code does not harm the system we parse it and check that -it only uses our supported set of datalog clauses and aggregates. Since these +it only uses our supported set of Datalog clauses and aggregates. Since these are not able to affect the environment and are guaranteed to halt every provider of the system should feel fine to accept them if a (profitable) fee is provided. -We will even add a good, established datalog query planning framework to ensure +We will even add a good, established Datalog query planning framework to ensure that each query will complete by upperbounding the costs of the query plan upfront. This is incredibly hard to do for Turing-complete programming languages, even if they have a strong type system. Since adding an invariant is just another form of transaction and its addition happens under the namespace of a public-key id of the sender, we need not -constrain users from supplying invariants. We can just ask to pay a minimum fee -for the IO operations that it costs to add one or a bunch of such contracts. It -will not pollute other index fragments, potentially causing additional costs to -other people's data or queries. And while in most blockchain systems users need -to fetch all data transacted to read arbitrarily from the blockchain, in datopia -it is enough to follow the Merkle proof to the leafs of each index tree. - -Footnote: -Technically we also need a way to verify the root of the tree, we can conceive -one way to do so by using a closed consensus system like Cosmos/Tendermint so -clients will be able to tell easily whether a block is valid by following the -global sequence and checking the majority validation of the root. +constrain users from supplying invariants. We can just ask to pay a moderate fee +for the IO operations that it costs to add one or a bunch of such contracts. ## Optimal interface -We speculate that with most meaningful contracts and apps, the partition in -index fragments will be almost information theoretically optimal for clients, -because the query plan will be minimized by detailed statistics of the -distribution of each attribute and these should cluster as well as they do for -conventional applications. In other words each client will only download the -data it needs from the giant database (plus an approximately constant size -overhead). Additionally we will gain the same expressivity as for the original -query language with the benefit from all optimizations to the query planner. + +While in most blockchain systems users need to fetch all data transacted to read +arbitrarily from the blockchain, in datopia it is enough to follow the Merkle +proof to the leafs of each index tree. [^3] We are confident that with most +meaningful contracts and apps, the partition in index fragments will be almost +information theoretically optimal for clients, because the query plan will be +minimized by detailed statistics of the distribution of each attribute and these +should cluster as well as they do for conventional applications. In other words +each client will only download the data it needs from the giant database (plus +an approximately constant size overhead). Additionally we will gain the same +expressivity as for the original query language with the benefit from all +optimizations to the query planner. + +[^3]: Technically we also need a way to verify the root of the tree, we can + conceive one way to do so by using a closed consensus system like + Cosmos/Tendermint so clients will be able to tell easily whether a block is + valid by following the global sequence and checking the majority validation + of the root. We want this interface to be widely available. In fact it is a middleware for @@ -305,17 +358,13 @@ run in any combination with a transaction mechanism. It is demonstrating one way to expose the query language to the transactor to achieve our objectives. - # Try it out Link to repo with datomic walk through (?) # Conclusion -... - - - +Smart contracts are solved. From 0ae402e89f70d802a7fe21545f3d5e9a9180792a Mon Sep 17 00:00:00 2001 From: Christian Weilbach Date: Mon, 15 Jun 2020 03:36:13 -0700 Subject: [PATCH 7/8] Fill in missing bits and text for first draft. --- _drafts/2019-06-03-invariant-intro.md | 270 +++++++++++++------------- 1 file changed, 137 insertions(+), 133 deletions(-) diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md index 1f07810979..acf61f69d1 100644 --- a/_drafts/2019-06-03-invariant-intro.md +++ b/_drafts/2019-06-03-invariant-intro.md @@ -1,10 +1,10 @@ --- layout: post -title: Invariants - Smart Contracts distilled +title: Invariants as Simple Smart Contracts author: Christian Weilbach -summary: Expressing invariants with Datalog provides a powerful smart contract system. +summary: Datalog provides simple and expressive invariants. tags: blockchain clojure code Datalog -date: 2019-09-01 12:00:00 +date: 2019-11-06 12:00:00 --- + We have [previously established](/2018/11/03/blockchain-information-system/) the appeal of a [Datalog based database](https://en.wikipedia.org/wiki/Datalog) in a blockchain setting. In summary, simplicity must be a [core design principle](https://www.infoq.com/presentations/Simple-Made-Easy) to manage complexity in (distributed) information systems. In the following we will lay -out how datopia can be managed by a novel, yet very simple transaction system. +out how Datopia can be managed by a novel, yet very simple transaction system. We will first give a motivation for our work and how it relates to other technologies, then describe its implementation with a simple example and a real-world accounting contract and finally look at design aspects like cost -models and finally we conclude. Since our concept is useful both in datomic and -datahike, we provide it as a light-weight library that is used by Datopia -instances. +models. Since our concept is useful both in Datomic and Datahike, we provide it +as a light-weight, open-source library that is used by Datopia instances. # Motivation @@ -49,20 +53,20 @@ composable programming model Almost every contemporary, partially automated social process uses one or more databases to manage its internal state. These databases often provide powerful relational logic languages like [SQL](http://www.mysql.com) or -[Datalog](http://datomic.com) to the user. Usually these query languages do most +[Datalog](http://Datomic.com) to the user. Usually these query languages do most of the hard work to extract information for a query, efficiently scanning the large body of accumulated knowledge. The rest of the application is often glue code to expose the information from the database to the surroundings in form of -user interfaces or APIs and manage access to it. The fact that each database is -contained in a silo that way requires endless, slow and error-prone integration -between different systems. - -Datopia instead provides support to selectively load index segments from a swarm -of peers directly into the client-side query engine. Our Datalog query engine -does not distinguish between the data hosted in datopia or locally hosted -private databases in [datahike](https://github.com/replikativ/datahike), in +user interfaces or APIs. The fact that each database is contained in a silo that +way requires endless, slow and error-prone integration between different +systems. + +Datopia provides support to selectively load index segments from a swarm of +peers directly into the client-side query engine instead. Our Datalog query +engine does not distinguish between the data hosted in Datopia or locally hosted +private databases in [Datahike](https://github.com/replikativ/Datahike), in other words an arbitrary number of databases can be joint at query time at the -reader. The system composes by datalog semantics and the efficiency of its query +reader. The system composes by Datalog semantics and the efficiency of its query planning. [We conceptualize](https://www.youtube.com/watch?v=A2CZwOHOb6U) Datalog as a universal language for distributed systems. Datopia will therefore automatically provide a straightforward extended Datalog dialect to extract @@ -74,39 +78,35 @@ pattern is totally decoupled and arbitrarily read scalable. [^1] -[^1]: A datahike client replication prototype is working on top of the [dat - project](https://dat.foundation/) using its publish and subscribe system, - but we think other variants on [IPFS](https://ipfs.io/) or - [BitTorrent](http://www.bittorrent.org/) are also possible. It is even - conceivable with technologies like - [3df](https://github.com/sixthnormal/clj-3df) that soon most user interfaces - can be directly filled through an incrementally updating materialized view - on a client of the database. We are having a collaboration working on - support for 3df in datahike. +[^1]: A Datahike client [replication + prototype](https://lambdaforge.io/2019/12/08/replicate-Datahike-wherever-you-go.html) + is working on top of the [dat project](https://dat.foundation/) using its + publish and subscribe system, but other variants on [IPFS](https://ipfs.io/) + or [BitTorrent](http://www.bittorrent.org/) are also possible. # Adding facts to Datopia -But what about adding new facts to datopia and changing the database? To supply +But what about adding new facts to Datopia and changing the database? To supply an interface to the user with similar ease as the query interface, we would have to constrain it in a similar way. What if... we would use Datalog also as a language to just attach an invariant to each relation? Since Datalog is guaranteed to halt, compact to express against a database of structured fact triples and in general considered powerful enough to do most application logic, we can expose our [invariant](https://github.com/datopia/invariant) library -through the datomic or datahike transactor to the network and let users deploy +through the Datomic or Datahike transactor to the network and let users deploy invariants to the database similarly to smart contract systems like Ethereum. To be sensible we of course also need to add a public-private key based identification system and a cost model for the submission of transaction data, which we will sketch below. -Why is this not possible with off-the-shelf PostgresSQL, CouchDB, MongoDB -datomic or datahike transactor functions or your favorite database? These -databases provide more powerful languages to express transaction operations -because they trust the code of the database is secured by careful manual -safe-guarding of the administrator. Besides being [somewhat +Why is this not possible with off-the-shelf PostgresSQL, CouchDB, MongoDB, +Datomic or Datahike transactor functions? These databases provide more powerful +languages to express transaction operations because they trust the code of the +database is secured by careful manual safe-guarding of the administrator. +Besides being [somewhat odd](https://www.postgresql.org/docs/current/sql-createfunction.html) to use -programming languages these mechanisms are therefore all Turing-complete, which +programming languages, these mechanisms are therefore all Turing-complete, which we consider unnecessary and harmful for most practical purposes. A lot of effort is spent to restrict [functional](https://iohk.io/research/papers/#marlowe-financial-contracts-on-blockchain) @@ -135,9 +135,9 @@ satisfy: 1. Our query results must be deterministic and verifiable by other peers later. 2. Each query must terminate. This means it cannot be [Turing complete](https://en.wikipedia.org/wiki/Turing_completeness). Most smart - contract language achieve this through a resource model, e.g. by requiring - gas to run. Datalog on the other hand allows to determine ahead of time how - many resources will be needed for a query. + contract languages achieve this through a resource model, e.g. by requiring + gas to run. A Datalog query planner on the other hand allows to upper bound + ahead of time how many resources will be needed for a query. 3. The query might not interact with anything but the database. 4. We need to restrict write operations to a sandbox so that all invariants for attributes changed by the transaction are maintained. @@ -145,25 +145,24 @@ satisfy: database. 6. Access to the system must be operable in a permissionless setting, i.e. potentially anybody can register, deploy invariants and add transactions for - a fee. This can be flexibly restricted, e.g. by regulating access through - another trusted system. + a fee. 7. The schema for the database is extendable by each user for themselves through public-private key cryptography. We naturally use our concise query language Datalog to verify transaction data. -The Datalog flavor implemented by datahike is a natural fit for the first 5 +The Datalog flavor implemented by Datahike is a natural fit for the first 5 points, in particular its combination with hitchhiker trees. We address the details of 6 in the following and 7 will be added for our test-net implementation. ## Invariant -What exactly is an an invariant? Invariants in general describe things that stay -the same. While we think that fairly simple invariants are the most important -building blocks in describing interesting systems, e.g. for accounting, our -system can also express invariants that describe complicated dynamics, e.g. that -a value must be counted up on each change. This is possible because the -invariant queries can reason about the change itself. +What exactly is an an invariant? Invariants in general describe attributes of +some process that stay the same. While we think that fairly simple invariants +are the most important building blocks in describing interesting systems, e.g. +for accounting, our system can also express invariants that describe complicated +dynamics, e.g. that a value must be counted up on each change. This is possible +because the invariant queries can reason about the change itself. But can we really express all the smart contract examples out there in Datalog? Our team has years of commercial and scientific experience with Datalog and we @@ -172,38 +171,85 @@ and better understandable than in other smart contract environments. Datalog is used in [large scale program verification](https://semmle.com/) for good reasons. We also want to note that almost all interesting laws can be expressed as invariants, e.g. energy conservation in physics. In case some primitives will -be missing it is as easy to add additional primitives as adding a pure Clojure -function to the datopia runtime and whitelisting it. Extensions with safe forms -of λ-calculus similar to [datafun](https://github.com/rntz/datafun) are possible -as well. +be missing, it is as easy to add additional primitives as adding a pure function +to the Datopia runtime and whitelisting it. Extensions with safe forms of +λ-calculus similar to [datafun](https://github.com/rntz/datafun) are possible as +well. # Warmup example +We start with a simple illustrative example. Let us assume we are storing +ancestor information, e.g. about family trees. To ensure that we really store +trees and do not introduce cycles into our database, we want to make sure that +nobody is ancestor of themselves. The following Datalog `query` is counting the +number of `?a`'s that are their own ancestors, and hence the total number of +people who participate in cycles. -- TODO sketch by drawing figures, then describe +~~~clojure +[:find (count ?a) . + :in $after % + :where + ($after ancestor ?a ?b) + [(= ?a ?b)]] +~~~ -- have simple self-explaining Datalog example +Let us assume we attempt to introduce a cycle by adding the following three +entities as a `transaction`, -- i like the idea of establishing some trivial graph theoretic property that - could be discussed in the context of a social network or dbpedia-style - ontology, because these are easy to visualize +~~~clojure +[{:db/id 1 + :ancestor 2} + {:db/id 2 + :ancestor 3} + {:db/id 3 + :ancestor 1}] +~~~ -- e.g. detecting cycles in category hierarchies, or even something more trivial - like enforcing account-blocking rules for a social network - maybe that's too - trivial, but you get the idea. - - -- explain 4 types of databases passed +We can describe the recursive ancestor relation in a concise Datalog `rules` +with two cases, +~~~ +'[[(ancestor ?a ?b) + [?a :ancestor ?b]] + [(ancestor ?a ?b) + [?a :ancestor ?t] + (ancestor ?t ?b)]] +~~~ + +either an entity `?a` is a direct ancestor of another entity `?b` or this +happens recursively through some transitive dependency `?t`. + +We can then use the query above to speculatively apply the transactions with +`d/with` and pass it as the database snapshot `$after` into the query engine of +either Datomic of Datahike like so + +~~~clojure +(d/q query + (:db-after (d/with @conn transaction)) + rules) +;; => +3 +~~~ + +and detect, as expected, that the resulting database has three elements +participating in the cycle. This allows us to reject the transaction outright +without it even passing into the transactor. # Accounting example -Let's move on to the more practical example of accounting. +Let's move on to the more complex example of accounting. [Accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of -bookkeeping that has been around since humans have tracked their possessions. -For simplicity we will model an asset we call `datacoin`. To deploy our contract -we use our public key prefix `0x64703/datacoin`. +bookkeeping that has been around since humans have tracked their possessions +[^3] For simplicity we will model an asset we call `datacoin`. To deploy our +contract we use our public key prefix `0x64703/datacoin`. + +[^3]: An opinionated, but interesting, perspective of different monetary devices + to account for fairness and facilitate the co-evolution of game theoretic + mechanisms are [accounted for by Nick + Szabo](https://nakamotoinstitute.org/shelling-out/#evolution-cooperation-and-collectibles). [This lecture of Robert Sapolsky](https://www.youtube.com/watch?v=NNnIGh9g6fA) describes the evolutionary background in more depth. + + We do not need to describe how to do an asset transfer, we only need to describe what properties need to be fulfilled for it to be valid. The submitter of the @@ -256,7 +302,7 @@ The full invariant for `0x64703/datacoin` then looks like: ~~~ Let's break it down. First we note that we support a `subquery` functionality by -our invariant library for both Datomic and datahike. The subquery here unifies +our invariant library for both Datomic and Datahike. The subquery here unifies the database against each `?affected-account`. It first binds the respective balances from the supplied databases. This is effectively an extension of Datalog with aggregation. Additionally it provides a form of lambda abstraction @@ -276,7 +322,7 @@ selective queries, but might be prohibitively expensive to aggregate. For this reason $empty+txs allows to reason about an empty database populated only with this transaction data and finally about the list of transactions themselves. We think this setup is sufficient to express many common invariants conveniently -and efficiently. +and efficiently, but might adapt it depending on the usage of the invariants. -
"The principle of least action is the basic +# Goals +{% quote Principle of Least Action, Scholarpedia|http://www.scholarpedia.org/article/Principle_of_least_action) %} +The principle of least action is the basic variational principle of particle and continuum systems. In Hamilton's formulation, a true dynamical trajectory of a system between an initial and final configuration in a specified time is found by imagining all possible trajectories that the system could conceivably take, computing the action (a functional of the trajectory) for each of these trajectories, and selecting one that makes the action locally stationary (traditionally called "least"). True -trajectories are those that have least action." -Principle of Least Action about the fundamental role of invariants in Physics, Scholarpedia -
+trajectories are those that have least action. +{% endquote %} @@ -83,10 +83,9 @@ pattern is totally decoupled and arbitrarily read scalable. [^1] is working on top of the [dat project](https://dat.foundation/) using its publish and subscribe system, but other variants on [IPFS](https://ipfs.io/) or [BitTorrent](http://www.bittorrent.org/) are also possible. - -# Adding facts to Datopia - +# Adding Facts to Datopia + But what about adding new facts to Datopia and changing the database? To supply an interface to the user with similar ease as the query interface, we would have to constrain it in a similar way. What if... we would use Datalog also as a @@ -117,7 +116,7 @@ simpler but almost equally expressive means have barely been explored so far in a smart contract setting. Arguably a lot of the current effort is trying to reduce most of these more expressive semantics to something that looks a lot like Datalog, but is still harder to reason about than a simple language like -Datalog. [^2] +Datalog.[^2] [^2]: What if you could use SQL to check transactions into the same SQL database? You should be able to build a similar library to `invariant` then. But @@ -126,8 +125,7 @@ Datalog. [^2] join over multiple "tables"? Datalog is so much more concise and easy to extend by user-defined rules... - -## Desiderata +## Desiderata Let's define a minimal set of requirements that each `invariant` query needs to satisfy: @@ -145,7 +143,7 @@ satisfy: database. 6. Access to the system must be operable in a permissionless setting, i.e. potentially anybody can register, deploy invariants and add transactions for - a fee. + a fee. 7. The schema for the database is extendable by each user for themselves through public-private key cryptography. @@ -173,10 +171,10 @@ reasons. We also want to note that almost all interesting laws can be expressed as invariants, e.g. energy conservation in physics. In case some primitives will be missing, it is as easy to add additional primitives as adding a pure function to the Datopia runtime and whitelisting it. Extensions with safe forms of -λ-calculus similar to [datafun](https://github.com/rntz/datafun) are possible as +λ-calculus similar to [Datafun](https://github.com/rntz/datafun) are possible as well. -# Warmup example +# Warmup Example We start with a simple illustrative example. Let us assume we are storing ancestor information, e.g. about family trees. To ensure that we really store @@ -187,7 +185,7 @@ people who participate in cycles. ~~~clojure [:find (count ?a) . - :in $after % + :in $after % :where ($after ancestor ?a ?b) [(= ?a ?b)]] @@ -197,11 +195,11 @@ Let us assume we attempt to introduce a cycle by adding the following three entities as a `transaction`, ~~~clojure -[{:db/id 1 +[{:db/id 1 :ancestor 2} - {:db/id 2 + {:db/id 2 :ancestor 3} - {:db/id 3 + {:db/id 3 :ancestor 1}] ~~~ @@ -235,13 +233,12 @@ and detect, as expected, that the resulting database has three elements participating in the cycle. This allows us to reject the transaction outright without it even passing into the transactor. - -# Accounting example +# Accounting Example Let's move on to the more complex example of accounting. [Accounting](https://en.wikipedia.org/wiki/Accounting) is a fundamental form of -bookkeeping that has been around since humans have tracked their possessions -[^3] For simplicity we will model an asset we call `datacoin`. To deploy our +bookkeeping that has been around since humans have tracked their possessions.[^3] +For simplicity we will model an asset we call `datacoin`. To deploy our contract we use our public key prefix `0x64703/datacoin`. [^3]: An opinionated, but interesting, perspective of different monetary devices @@ -249,8 +246,6 @@ contract we use our public key prefix `0x64703/datacoin`. mechanisms are [accounted for by Nick Szabo](https://nakamotoinstitute.org/shelling-out/#evolution-cooperation-and-collectibles). [This lecture of Robert Sapolsky](https://www.youtube.com/watch?v=NNnIGh9g6fA) describes the evolutionary background in more depth. - - We do not need to describe how to do an asset transfer, we only need to describe what properties need to be fulfilled for it to be valid. The submitter of the transaction data can use any program to generate the transaction data that will @@ -259,43 +254,53 @@ senders, e.g. by public-private key cryptography that is provided by the system, we need at least the following three invariants to have a contract in place that I would risk putting money in: -1. Zero-Sum -2. Positivity of Accounts -3. Sender is spending +Zero-Sum +: Maintain a constant global asset sum; transfers can't inflate/deflate supply. + +Balance Positivity +: No overdrafts; balances bottom-out at zero. -Zero-Sum means that after each transaction the total sum of assets in the system -should not change. Positivity of accounts means that you cannot overdraft your -account into a negative balance. Finally only a signing sender can spend money -in a transaction. +Sender spends +: Expenditure is restricted to the signing sender/s of the transaction. -The full invariant for `0x64703/datacoin` then looks like: +## Full Invariant ~~~clojure [:find ?matches . - :in $before $after $empty+txs $txs + :in $before $after $empty+txs $txs :where - ;; run the sub-query - [(subquery [:find (sum ?balance-before) - (sum ?balance-after) - (sum ?balance-change) - :with ?affected-account - :in $before $after $empty+txs $txs - :where - ;; Unify data from databases and transactions with affected-account - [$after ?affected-account :0x64703.account/balance ?balance-after] - [$empty+txs ?affected-account :0x64703.account/balance ?balance-change] - [(get-else $before ?affected-account :0x64703.account/balance 0) ?balance-before] - - ;; 2. Positivity - [(>= ?balance-after 0)] - - ;; 3. Sender spending - [$txs _ _ :transaction/signed-by ?sender] - [(= ?sender ?affected-account) ?is-sender] - [(>= ?balance-change 0) ?pos-change] - [(or ?is-sender ?pos-change)]] - $before $after $empty+txs $txs) + [(subquery + [:find (sum ?balance-before) + (sum ?balance-after) + (sum ?balance-change) + :with ?affected-account + :in $before $after $empty+txs $txs + :where + ;; Unify data from databases and transactions with affected-account + [$after + ?affected-account + :0x64703.account/balance + ?balance-after] + + [$empty+txs + ?affected-account + :0x64703.account/balance + ?balance-change] + + [(get-else $before ?affected-account :0x64703.account/balance 0) + ?balance-before] + + ;; 2. Positivity + [(>= ?balance-after 0)] + + ;; 3. Sender spending + [$txs _ _ :transaction/signed-by ?sender] + [(= ?sender ?affected-account) ?is-sender] + [(>= ?balance-change 0) ?pos-change] + [(or ?is-sender ?pos-change)]] + $before $after $empty+txs $txs) [[?sum-before ?sum-after ?sum-change]]] + ;; 1. Zero-Sum aggregated [(= ?sum-before ?sum-after)] [(= ?sum-change sum-change-expected) ?matches]] @@ -334,9 +339,9 @@ as an exercise to the reader :). --> -# Design aspects +# Design Aspects -## Cost model for Datopia +## Datopia Cost Model Reading from Datopia will not cost anything as the database is replicated over a peer to peer network freely. Writing to the database costs the execution of @@ -363,20 +368,20 @@ sure that the deployed code does not harm the system we parse it and check that it only uses our supported set of Datalog clauses and aggregates. Since these are not able to affect the environment and are guaranteed to halt, every provider of the system should feel fine to accept them if a (profitable) -deployment fee is provided. +deployment fee is provided. Since adding an invariant is just another form of transaction and its addition happens under the namespace of a public-key id of the sender, we need not constrain users from supplying invariants. We can just ask to pay a consistent fee -for the IO operations that it costs to add one or a bunch of such contracts. +for the IO operations that it costs to add one or a bunch of such contracts. -## Optimal interface +## Optimal Interface While in most blockchain systems users need to fetch all data transacted to read arbitrarily from the blockchain, in Datopia it is enough to follow the Merkle -proof to the leafs of each index tree[^4] We are confident that with most +proof to the leafs of each index tree[^4]. We are confident that with most meaningful contracts and apps, the partition in index fragments will be almost information theoretically optimal for clients, because the query plan will be minimized by detailed statistics of the distribution of each attribute and these @@ -392,7 +397,6 @@ optimizations to the query planner. whether a block is valid by following the global sequence and checking the majority validation of the root. - We want this interface to be widely available. In fact it is a middleware for both Datomic and Datahike right now and can be combined with different transactor implementations based on Cosmos/Tendermint, a proof-of-work based @@ -400,7 +404,6 @@ transactor or a managed, privileged set of servers. In other words Datopia can run in any combination with a transaction mechanism. It is demonstrating one way to expose the query language to the transactor to achieve our objectives. - # Conclusion By deploying Datalog, one of the most expressive - yet effective - languages in @@ -409,14 +412,9 @@ requirements often identified in smart contract systems. We are still evolving the ideas around Datopia and are happy about your feedback! (TODO link communication channel) - -# Try it out +## Try It Out You can find the code in our [invariant repository](https://github.com/datopia/invariant). - - - - - +# Footnotes diff --git a/_includes/head.html b/_includes/head.html index d08ec4d319..18e182c763 100644 --- a/_includes/head.html +++ b/_includes/head.html @@ -26,11 +26,10 @@ {% if site.extended_fonts %} - - - + + {% else %} - + {% endif %} {% if site.show_social_icons or site.show_sharing_icons %} diff --git a/_plugins/quote.rb b/_plugins/quote.rb new file mode 100644 index 0000000000..348b73a63d --- /dev/null +++ b/_plugins/quote.rb @@ -0,0 +1,21 @@ +class QuoteTag < Liquid::Block + def initialize(tag_name, input, tokens) + super + @input = input + @tag_name = tag_name + end + + def render(context) + text = super + cls = @tag_name == 'quote' ? '' : ' left' + title, url = @input.split('|') + return %{
+ “#{text.strip}” +
— #{title}
+
+ } + end +end + +Liquid::Template.register_tag('quote', QuoteTag) +Liquid::Template.register_tag('quote_left', QuoteTag) diff --git a/_posts/2018-11-03-blockchain-information-system.md b/_posts/2018-11-03-blockchain-information-system.md index 43e76410a5..9b2461bd64 100644 --- a/_posts/2018-11-03-blockchain-information-system.md +++ b/_posts/2018-11-03-blockchain-information-system.md @@ -8,21 +8,17 @@ tags: blockchain database vision # Axioms -
-
    -
  1. A blockchain is a history of facts.
    2. -
  2. Inference is the application of reason to histories of facts.
    3. -
-
+1. A blockchain is a history of facts. +2. Inference is the application of reason to histories of facts. # Goals -
+
An integrated set of components for collecting, storing, and processing data and for providing information, knowledge, and digital products.
— Zwass, Vladimir. "Information system." The Encyclopedia Britannica.
-
+
Below, we'll attempt to convince you that neither traditional databases nor blockchains represent epistemologically robust _information systems_ --- the @@ -197,7 +193,6 @@ contract Ballot { } ... } - ``` This is fairly typical Solidity code --- after an imperative sequence of runtime diff --git a/_sass/_custom.scss b/_sass/_custom.scss index b4a8615d7a..0143a940f0 100644 --- a/_sass/_custom.scss +++ b/_sass/_custom.scss @@ -1,156 +1,161 @@ html, body { - font-weight: 300; - background-color: $datopia-bg-light; + font-weight: 300; + background-color: $datopia-bg-light; } .site-header { - padding: 0; + padding: 0; } a:hover, .share-links a:hover { - color: darken($datopia-primary-blue, 25%); + color: darken($datopia-primary-blue, 25%); } .datopia-home-link img { - height: 8em; + height: 8em; } .post-meta { - text-align: right; - font-style: normal; - font-family: $heading-font-family; - font-size: 90%; - display: block; + text-align: right; + font-style: normal; + font-family: $heading-font-family; + font-size: 90%; + display: block; } a.post-link, .post-title { - font-weight: 900 !important; - color: $datopia-primary-blue !important; + font-weight: 900 !important; + color: $datopia-primary-blue !important; } .post-link .post-summary { - font-weight: 300; + font-weight: 300; } .posts .py3:first-of-type { - padding-top: 0; + padding-top: 0; } .post-header h1 { - padding-top: 0; - margin-top: 0; + padding-top: 0; + margin-top: 0; + clear: both; } .post-summary { - text-indent: 2em; - display: block; - font-size: 90%; + text-indent: 2em; + display: block; + font-size: 90%; } -.post-header .post-summary { - font-style: italic; - font-size: 80%; - margin-left: 2em; +blockquote { + border-left: 1px dashed $datopia-primary-blue; + padding: 1rem; } -blockquote { - border-left: 2px solid $datopia-primary-blue; - padding: 1rem; +.post-header .post-summary { + font-style: italic; + font-size: 80%; + margin-left: 2em; } a, a:hover { - background-image: none; - font-weight: 700; + background-image: none; + font-weight: 700; } .post-content > p { - text-indent: 2em; + text-indent: 2em; } .post-author { - font-size: 120%; + font-size: 120%; } h1, h2, h3, h4 { - font-weight: 300; + font-weight: 300; + clear: both; } .footnote { - font-style: italic; - margin-left: 2em; + font-style: italic; + margin-left: 2em; } body sup { - font-family: monospace; + font-family: monospace; } pre { - background-color: transparent; + background-color: transparent; } -.literal { - float: right; - display: block; - max-width: 35%; - font-size: 80%; - margin-top: 0; - margin: 0 0 0.75ex 4ex; - border-width: 0; - font-style: normal; - font-weight: 700; - color: #777777; +blockquote.literal { + float: right; + display: block; + max-width: 35%; + font-size: 80%; + margin: 0 0 1ex 2ex; + font-style: italic; + text-indent: 2em; + font-style: italic; + border-style: dashed; + border-width: 0 0 0 1px; + border-color: $datopia-lighter-blue; + padding: 1.25rem; } -.left.literal { - float: left; - margin-left: 0; +blockquote.literal.left { + float: left; + margin: 0 3ex 1ex 0; + border-width: 0 1px 0 0; } .attrib { - text-align: right; - padding-top: 0.5ex; - font-style: italic; + text-align: right; + padding-top: 0.5ex; + font-style: normal; } .footnote { - line-height: 1rem; + line-height: 1rem; } small, .small { - font-size: 0.707rem; + font-size: 0.707rem; } .infobox-title { - color: #666666; - font-family: 'Lato', 'Helvetica Neue', Helvetica, sans-serif; - border-bottom: solid 2px $datopia-primary-blue; - margin-left: 90px; - margin-bottom: 8px; - padding-bottom: 8px; - font-size: 1.5rem; + color: #666666; + font-family: 'Lato', 'Helvetica Neue', Helvetica, sans-serif; + border-bottom: solid 2px $datopia-primary-blue; + margin-left: 90px; + margin-bottom: 8px; + padding-bottom: 8px; + font-size: 1.5rem; } .infobox { - background-image: url(/images/info.svg); - background-repeat: no-repeat; - background-position: top left; - background-size: 80px 80px; - background-opacity: .4; - margin: 1.5rem 0 1.5rem; - min-height: 90px; + background-image: url(/images/info.svg); + background-repeat: no-repeat; + background-position: top left; + background-size: 80px 80px; + background-opacity: .4; + margin: 1.5rem 0 1.5rem; + min-height: 90px; } .infobox p { - font-size: .8rem; - padding-left: 90px; - margin-bottom: 0px; - margin-top: 1rem; - text-indent: 2em; + font-size: .8rem; + padding-left: 90px; + margin-bottom: 0px; + margin-top: 1rem; + text-indent: 2em; } .bot-left { - position: relative; - padding: 4ex 0 4ex 4ex; + position: relative; + padding: 4ex 0 4ex 4ex; } .bot-left:before, .bot-left:after { @@ -178,69 +183,113 @@ small, .small { } body pre, body code { - background-color: transparent; + background-color: transparent; } .thumbnail-right { - float: right; - margin-left: 1rem; + float: right; + margin-left: 1rem; } img.center { - padding-top: 0.5rem; - padding-bottom: 0.5rem; + padding-top: 0.5rem; + padding-bottom: 0.5rem; } table.small, table.small td { - border-width: 0; + border-width: 0; } table.small thead { - font-weight: bold; + font-weight: bold; } .share-links { - border: solid 2px $datopia-primary-blue; - border-width: 2px 0 2px 0; - font-size: 400%; - text-align: center; - margin-top: 2rem; + border: solid 2px $datopia-primary-blue; + border-width: 2px 0 2px 0; + font-size: 400%; + text-align: center; + margin-top: 2rem; } body #mc_embed_signup { - background: transparent; - font-family: $heading-font-family; + background: transparent; + font-family: $heading-font-family; } body #mc_embed_signup .button { - text-transform: uppercase; - background-color: $datopia-primary-blue; + text-transform: uppercase; + background-color: $datopia-primary-blue; } body #mc_embed_signup .button:hover { - background-color: darken($datopia-primary-blue, 25%); + background-color: darken($datopia-primary-blue, 25%); } body #mc_embed_signup #mc-embedded-subscribe-form div.mce_inline_error { - background-color: transparent; + background-color: transparent; } .diag { - padding-bottom: 1ex; + padding-bottom: 1ex; } - table { - border-collapse: collapse; + border-collapse: collapse; } th, td { - padding: 0; + padding: 0; } .twitter-top { - float: right; + float: right; } .mini-nav td { - border-width: 0; + border-width: 0; +} + +sup > a.footnote { + margin-left: 0; + margin-right: 1em; +} + +ol { + counter-reset: item; +} + +ol, dl { + margin: 0 0 1.5em 2em; + padding: 0 0 0 1em; + border-left: 1px dashed $datopia-primary-blue; +} + +ol > li { + counter-increment: item; + margin: 0 0 1em 0; + padding: 0 0 0 2em; + text-indent: -2em; + list-style-type: none; +} + +dd { + margin-bottom: 1em; + font-style: italic; +} + +ol > li:before { + font-weight: bold; + content: counter(item) "."; + display: inline-block; + text-align: right; + width: 1em; + padding-right: 0.5em; +} + +div.footnotes ol > li > p { + display: inline; +} + +dt { + font-weight: bold; } diff --git a/_sass/_variables.scss b/_sass/_variables.scss index 04fa2454a5..21c2661a2e 100644 --- a/_sass/_variables.scss +++ b/_sass/_variables.scss @@ -1,17 +1,19 @@ // Custom $datopia-bg-light: rgb(247,246,244); $datopia-primary-blue: rgb(76, 153, 178); +$datopia-lighter-blue: lighten($datopia-primary-blue, 20%); $datopia-secondary-blue: rgb(52, 121, 242); $datopia-teal: rgb(190, 211, 215); + // Typography $base-font-size: 14px !default; $bold-font-weight: bold !default; -$font-family: 'Roboto'; +$font-family: 'Comfortaa', 'Helvetica Neue', Helvetica, sans-serif !default; $line-height: 1.5 !default; -$heading-font-family: 'Lato', 'Helvetica Neue', Helvetica, sans-serif !default; +$heading-font-family: 'Comfortaa', 'Helvetica Neue', Helvetica, sans-serif !default; $heading-font-weight: 700 !default; $heading-line-height: 1.25 !default; -$monospace-font-family: 'Source Code Pro', Consolas, monospace !default; +$monospace-font-family: Inconsolata, Consolas, monospace !default; $h1: 2.25rem !default; $h2: 1.5rem !default; $h3: 1.25rem !default;