From 02af75f4b79ff0a193ac8282bf6cf229a9b00b49 Mon Sep 17 00:00:00 2001 From: Moe Aboulkheir Date: Sun, 19 Jul 2020 14:26:09 +0100 Subject: [PATCH] Rework invariant post --- _drafts/2019-06-03-invariant-intro.md | 420 -------------------------- _drafts/2020-07-19-invariant-intro.md | 306 +++++++++++++++++++ _layouts/post.html | 4 +- _plugins/infobox.rb | 19 ++ _plugins/notpara.rb | 10 + _sass/_custom.scss | 18 +- 6 files changed, 352 insertions(+), 425 deletions(-) delete mode 100644 _drafts/2019-06-03-invariant-intro.md create mode 100644 _drafts/2020-07-19-invariant-intro.md create mode 100644 _plugins/infobox.rb create mode 100644 _plugins/notpara.rb diff --git a/_drafts/2019-06-03-invariant-intro.md b/_drafts/2019-06-03-invariant-intro.md deleted file mode 100644 index d0671b12fa..0000000000 --- a/_drafts/2019-06-03-invariant-intro.md +++ /dev/null @@ -1,420 +0,0 @@ ---- -layout: post -title: Invariants as Simple Smart Contracts -author: Christian Weilbach -summary: Datalog provides simple and expressive invariants. -tags: blockchain clojure code Datalog -date: 2019-11-06 12:00:00 ---- - - - -# 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. -{% endquote %} - - - -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. 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 - - - -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. 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 -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](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 -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 -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? 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 - -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. This means it cannot be [Turing - complete](https://en.wikipedia.org/wiki/Turing_completeness). Most smart - 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. -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. -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 -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 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 -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 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. - -~~~clojure -[:find (count ?a) . - :in $after % - :where - ($after ancestor ?a ?b) - [(= ?a ?b)]] -~~~ - -Let us assume we attempt to introduce a cycle by adding the following three -entities as a `transaction`, - -~~~clojure -[{:db/id 1 - :ancestor 2} - {:db/id 2 - :ancestor 3} - {:db/id 3 - :ancestor 1}] -~~~ - -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 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 -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 -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: - -Zero-Sum -: Maintain a constant global asset sum; transfers can't inflate/deflate supply. - -Balance Positivity -: No overdrafts; balances bottom-out at zero. - -Sender spends -: Expenditure is restricted to the signing sender/s of the transaction. - -## Full Invariant - -~~~clojure -[:find ?matches . - :in $before $after $empty+txs $txs - :where - [(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]] -~~~ - -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, but might adapt it depending on the usage of the invariants. - - - -# Design Aspects - -## 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 -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) -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. - - -## 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 -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. - -[^4]: 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 or Avalanche such that 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 -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. - -# Conclusion - -By deploying Datalog, one of the most expressive - yet effective - languages in -database systems today, we propose a simple solution to a large subset of the -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 - -You can find the code in our [invariant -repository](https://github.com/datopia/invariant). - -# Footnotes diff --git a/_drafts/2020-07-19-invariant-intro.md b/_drafts/2020-07-19-invariant-intro.md new file mode 100644 index 0000000000..8b1943d518 --- /dev/null +++ b/_drafts/2020-07-19-invariant-intro.md @@ -0,0 +1,306 @@ +--- +layout: post +title: Validating Database Transactions With Datalog +author: Christian Weilbach, Moe Aboulkheir +summary: Using declarative logic to expressing and enforce complex data contracts. +tags: blockchain clojure code Datalog +date: 2020-07-19 00:00:00 +--- + + + +# Introduction + + + +In Datopia --- [our open, distributed +database](https://blog.datopia.io/2018/11/03/blockchain-information-system/) +--- the fundamental network interaction is transaction submission: the +atomic assertion of one or more facts, which, if accepted, are +incorporated into a globally available database. These transactions +may introduce attributes by providing schemas, as well as describe +arbitrary data in terms of previously deployed attributes. To ensure +data coherence in an open network, the originator of an attribute +requires some means of representing the conditions under which it may +sensibly be used. + +Given our use of [Datalog](https://en.wikipedia.org/wiki/Datalog) on +the query side, we found it natural to express data properties as +declarative queries: a transaction is applied only if we're able to +unify all invariants associated with its attributes. While a given +invariant check is triggered by its attribute's _use_, the invariant's +query has access to the wider database, as well as the values in the +transaction itself. In practice, this allows for the expression of +anything from simple write controls to surprisingly complex data +contracts (e.g. value exchange via direct balance manipulation, +double-entry accounting, enforcement of acyclic graphs). + +Our specific solution is available as +[invariant](https://github.com/datopia/invariant): a lightweight, +independent Clojure library usable with +[Datahike](https://github.com/replikativ/datahike) and +[Datomic](https://datomic.com). We believe it's both simple and +general enough to be of use to those developing applications atop +those databases, regardless of context --- and would appreciate +contributions and API input. Below, we'll describe how we settled +on this approach, and detail how it's used in Datopia. + +{%notpara%} + +This post assumes knowledge of both Datalog and Clojure. + +{%endnotpara%} + +# Requirements + +Invariants aren't only used in for application-level expectation +enforcement: Datopia's operation relies on the coherent, restricted +use of a set of fundamental attributes described in the _origin +schema_. When evaluating possible approaches, we ideally wanted to +rely on a single mechanism for verifying _all_ writes, and +determined the solution ought to address the following criteria: + +Inviolable +: Database-external validation (e.g. in application code) is +impractical with a diverse/open set of clients, or a large volume of +interdependent data --- and is trivial to circumvent by omission. + +Contextual +: Complex invariants may have a need to incorporate inputs beyond +a single attribute write, or writes in the current transaction. + +Deterministic +: Block producers are required to agree on the database contents after + processing each block of transactions --- invariants must reproducibly + pass/fail given the same inputs. + +Quantifiable +: The complexity of an invariant must be calculable prior to +execution, and ideally at the time the invariant is deployed. + +# Solution + +As outlined above, `invariant` allows for Datalog queries to be +persistently associated with individual attributes --- and provides an +API which ensures the queries unify whenever the corresponding +attribute is used in a transaction. The benefits are several: Datalog +is [Turing +incomplete](https://en.wikipedia.org/wiki/Turing_completeness), +deterministic[^1] --- and upper bounds on a query's resource +consumption are obtainable in principle via query planning. + +[^1]: While pure Datalog is non-deterministic, Datahike and Datomic + support non-deterministic aggregates (e.g. `rand`, `sample`). + Datopia permits aggregation, but forbids user-defined functions or + non-deterministic expressions. + +To better understand where invariants fit in with Datopia's transaction +processing, let's go over the relevant steps a block producer +follows when receiving a transaction over the network.[^2] + +[^2]: There'd be additional verification if the transaction were + deploying an attribute, or introducing an invariant --- for + simplicity, we'll cover the simple case. + +1. Augment transaction with attributes synthesized from the envelope (e.g. `datopia.tx/signed-by`). +2. Interrogate database deployment for invariant queries associated +with any attribute used in the transaction. +3. Assert that all invariant queries unify. +4. Apply the transaction itself. + +{%notpara%} + +Further to #3, each invariant is provided the following four +relations, named by convention: + +{%endnotpara%} + + +`$before` +: The database prior to applying the transaction. + +`$after` +: The database after speculatively applying the transaction --- `(db-with db tx)` + +`$empty+tx` +: An empty (i.e. schema-only) database containing only the + speculatively applied transaction --- `(db-with (empty-db) tx)`. + +`$tx` +: The transaction vector itself. + +# Accounting Example + +{%infobox Public Keys & Namespaces%} +To prevent squatting, all attributes are created with a namespace +consisting of the deployer's public key. Below, we're assuming the +existence of an account with public key `0x64...` --- referred to as +`0x64` for brevity (with a namespace of `x64`). +{%endinfobox%} + +{%notpara%} + +Our user wants to model an asset called `lcoin` (Lambdacoin), and +submits the following (idealized) transaction to the Datopia network: + +{%endnotpara%} + +```clojure +#:db{:ident :x64.lcoin/balance + :valueType :db.type/bigdec + :cardinality :db.cardinality/one} +``` + +{%notpara%} + +If everything goes well, anyone can now give themselves whatever +Lamdacoin balance they want! Unfortunately, that's not exactly what +`0x64` had in mind. Let's augment the attribute with an invariant +query which enforces the following properties: + +{%endnotpara%} + +Zero-Sum +: Maintain a constant global asset sum; transfers can't inflate/deflate supply. + +Balance Positivity +: No overdrafts; balances bottom-out at zero. + +Sender Spends +: Expenditure is restricted to the signing sender/s of the transaction. + +{%notpara%} + +The invariant is associated with the attribute by populating the database +with an entity having an `:invariant/rule` of `:x64.lcoin/balance` and +an `:invariant/query` attribute containing a string representation of the +query. + +{%endnotpara%} + +## Query + +{%notpara%} + +To begin with, an intermediate query yielding the aggregate difference +across all affected balances: + +{%endnotpara%} + +```clojure +[:find (sum ?balance-change) . + :in $before $after $empty+tx $tx + :with ?entity + :where + ; Only consider entities affected by the transaction. + [$empty+tx ?entity :x64.lcoin/balance _] + + [$after ?entity :x64.lcoin/balance ?balance-after] + ; Bail-out early if the entity's balance will be negative. + [(>= ?balance-after 0M)] + + [(get-else $before ?entity :x64.lcoin/balance 0M) ?balance-before] + [(- ?balance-after ?balance-before) ?balance-change] + + [$empty+tx _ :datopia.tx/signed-by ?sender] + [(= ?sender ?entity) ?is-sender] + [(>= ?balance-change 0M) ?pos-change] + ; If the balance is decreasing, it must belong to a signatory. + [(or ?is-sender ?pos-change)]] +``` + +{%notpara%} + +We'll embed this as a sub-query within our invariant, though it's +doing all of the lifting itself. Now, let's assume database +containing the following entities (with angle-bracketed names serving +as placeholders for irrelevant values): + +{%endnotpara%} + +```clojure +[{:datopia/id + :x64.lcoin/balance 1M} + {:datopia/id }] +``` + +{%notpara%} + +We then evaluate our query against it, in the context of the following +transaction, which looks to move one Lamdacoin unit from `` to +``: + +{%endnotpara%} + +```clojure +[[:datopia.fn/call + :x64.lcoin/balance -1M] + [:datopia.fn/call + :x64.lcoin/balance +1M] + ;; As noted above, this is derived by the block producer; it's + ;; included here for clarity + {:datopia.tx/signed-by }] +``` + +{%notpara%} + +Which'll yield `0`, the total difference between all affected balances +before and after the transaction is considered. The balance writes +are expressed commutatively, in terms of the transactional utility +function `+`. + +The invariant evaluator expects us to supply a query which won't unify +on failure, so we'll nest our query above within another which +requires the aggregate to total `0`: + +{%endnotpara%} + +```clojure +[:find ?sum-change . + :in $before $after $empty+tx $tx + :where + [(subquery + [:find (sum ?balance-change) . + ... ;; query as above + ] $before $after $empty+tx $tx) ?sum-change] + [(zero? ?sum-change)]] +``` + +{%notpara%} + +The `subquery` form is expanded by the `invariant` library into a +backend-specific (i.e. Datahike, Datomic) query expression --- here, +we pass it the sources available to the top-level query, and bind its +result to the scalar `?sum-change`. + +The result of this query --- nothing, if the subquery yields an +unacceptable value for `?sum-change`, and some truthy value otherwise +--- determines whether a transaction writing to `:x64.account/balance` +will succeed. + +{%endnotpara%} + +# Conclusion + +Datalog --- one of the more expressive, effective languages used in +database systems today --- promises a simple solution to a large +subset of the problems addressed by procedural smart contracts. + +We're still evolving the ideas around Datopia and are looking forward +to community feedback! + +## Try It Out + +{%notpara%} + +You can find the code at +[datopia/invariant](https://github.com/datopia/invariant) on Github. + +{%endnotpara%} + +# Footnotes diff --git a/_layouts/post.html b/_layouts/post.html index 515e91538d..5df8da08a1 100644 --- a/_layouts/post.html +++ b/_layouts/post.html @@ -32,8 +32,8 @@

{{ page.title }}

Subscribe to Datopia Updates

-If you've an interest in receiving infrequent project updates, or details -of any future Datopia token sale, please enter your email address below. +If you've an interest in receiving infrequent project updates, please +enter your email address below. diff --git a/_plugins/infobox.rb b/_plugins/infobox.rb new file mode 100644 index 0000000000..5b56f0cb74 --- /dev/null +++ b/_plugins/infobox.rb @@ -0,0 +1,19 @@ +class InfoboxTag < Liquid::Block + def initialize(tag_name, input, tokens) + super + @input = input + end + + def render(context) + site = context.registers[:site] + conv = site.find_converter_instance(::Jekyll::Converters::Markdown) + text = conv.convert(super) + return %{
+
#{@input.strip}
+

#{text}

+
+ } + end +end + +Liquid::Template.register_tag('infobox', InfoboxTag) diff --git a/_plugins/notpara.rb b/_plugins/notpara.rb new file mode 100644 index 0000000000..8a11eb4b4b --- /dev/null +++ b/_plugins/notpara.rb @@ -0,0 +1,10 @@ +class NotParaTag < Liquid::Block + def render(context) + site = context.registers[:site] + conv = site.find_converter_instance(::Jekyll::Converters::Markdown) + text = conv.convert(super) + return "
#{text}
" + end +end + +Liquid::Template.register_tag('notpara', NotParaTag) diff --git a/_sass/_custom.scss b/_sass/_custom.scss index 0143a940f0..798c496ce8 100644 --- a/_sass/_custom.scss +++ b/_sass/_custom.scss @@ -68,6 +68,10 @@ a, a:hover { text-indent: 2em; } +.post-content > p.notpara { + text-indent: 0; +} + .post-author { font-size: 120%; } @@ -102,12 +106,12 @@ blockquote.literal { border-style: dashed; border-width: 0 0 0 1px; border-color: $datopia-lighter-blue; - padding: 1.25rem; + padding: 0.75rem 1.25rem 0.75rem 1.25rem; } blockquote.literal.left { float: left; - margin: 0 3ex 1ex 0; + margin: 0 2ex 1ex 0; border-width: 0 1px 0 0; } @@ -182,10 +186,18 @@ small, .small { background-image: -o-linear-gradient(left, $datopia-primary-blue, transparent); } +article > p > code, article dt code, article code.highlighter-rouge { + color: black; +} + body pre, body code { background-color: transparent; } +body div.highlight pre .c1 { + color: black; +} + .thumbnail-right { float: right; margin-left: 1rem; @@ -251,7 +263,7 @@ th, td { sup > a.footnote { margin-left: 0; - margin-right: 1em; + margin-right: 0px; } ol {