Introduction
The Take Home Points
Take "Consensus as Court" Seriously
Solve Scaling, Interoperability, dApps
Contracts are to not evaluate code on the blockchain
Contract languages are way too low-level — use Formal Methods
Introduction
Advancement Status
This talk: only a BIG PICTURE
Mutual Knowledge Systems: we released a MVP for
Current status: Mock on Ethereum
Introduction
First Problem: Scaling Issue
Throughput: 7 tps for BTC, 15 for ETH (vs > 2000 tps for CC)
Latency: 60 min for BTC, 30 for ETH (vs 7 s for CC)
Too little, too slow for casual payments!
Gas, groceries, drinks, meals, etc.
Introduction
Usual solution?
Fiat currencies: fast payment via payment cards.
Why can't we have payment card equivalent for cryptocurrency?
Fiat "solutions" are centralized...
Real issue: not their being centralized, but custodial.
Consensus as Court
What is a distributed consensus for?
If everyone is honest and competent, a signed check is gold.
You could re-endorse it eternally and never clear it.
The Consensus is to prevent and resolve disputes.
It is analogous to a Court — Necessarily slow and expensive.
Consensus as Court
Don't go to Court for Casual Payment
Court: yes to buy a house, a car.
Court: not to buy coffee.
Make casual payments with payment processors: it scales!
Only go to Court to prevent and resolve disputes.
Consensus as Court
Analogy between Consensus & Court
| human law | smart law |
|---|
| participants | humans | machines |
|---|
| enforcement | social | algorithmic |
|---|
| arbiter | judge | consensus |
|---|
| register | court clerk, etc. | account table, utxos |
|---|
| interpretation | flexible | rigid |
|---|
| outcome | uncertain | certain (*) |
|---|
Consensus as Court
Analogies for Functional Programmers
Analogy: one Abstraction applied twice...
Break down: ... to different parameters.
Common Abstraction: Adjudication
Different Parameters: Humans vs Machines
Consensus as Court
What Law CANNOT do
Why don't we just make X illegal?
You can't decree bad behavior away.
Murder is illegal, yet it still happens.
Law can never prevent anyone from ever doing anything.
Consensus as Court
What Law CAN do
It can only hold actors accountable for what they do.
Provide incentives. Game Theory
Skin in the game.
Human Law: can get caught. Smart Law: must deposit collateral.
Consensus as Court
Economic Analysis of Law
Branch of Economics.
Study how Law affects incentives of all participants.
Consequences, not intentions.
Applies to lawmakers, too (Public Choice Theory)
Consensus as Court
Kinds of Freedom vs Alignment of Interests
| Allowed Individual Action | Effect on Interests |
|---|
| None | Just shut up & obey | Generate Chaos, Oppose Interests |
|---|
| Voice | Say whatever you want, Vote | Create Coordination, Consumes Alignment |
|---|
| Exit | Repudiate a bad provider | Finds Alignment,
Within Limited Choice |
|---|
| Enter | Found a new competitor | Create Alignment, Generate Order |
|---|
Consensus as Court
Aligning interests of Payment Processors
On a blockchain, limited Voice, but unlimited Exit and Enter.
Keep payment processors honest via Exit and Enter.
Exit: Repudiation, on chain, or en masse to another processor!
Enter: Anyone can cook.
Consensus as Court
Consensus as Court
Fruitful Point of View
Consensus provides arbitration, not transactions
Fast Transactions on a side-chain
Go to consensus only to resolve disputes
Smart Contracts for Side-Chains
Smart Contracts for Side-Chains
First good news! Solving Scaling
Do not publish transactions on the main chain — WIN!
Non-publication is infinitely faster than publication.
Publish title registration, in large batches.
Publish law suits — few and far between thanks to good incentives
Smart Contracts for Side-Chains
Non publication is for contracts, too!
Publish contract with salted hashes of the clauses (Bitcoin MAST).
Fulfill all obligations, then settle contract.
Only if one party fails, reveal one clause to get compensation.
Smaller, Cheaper, Faster, More Private.
Smart Contracts for Side-Chains
What are contracts for?
Mechanism to create alignment of interests.
Plan A: Never going to Court.
Contracts are not for "evaluating code on the blockchain"
Do all the work in side-chains.
Smart Contracts for Side-Chains
What do contracts consist in?
Mutual obligations.
A series of clauses.
In each clause, a participant makes a promise.
If they break their promise, a sanction punishes them.
Smart Contracts for Side-Chains
Example Contract: Atomic Swap
Exchange $1000 worth between Monero and Zcash.
Sign Ethereum contract each¹ posting a bond worth $4000.
Settlement is slow, but the contract is binding as soon as confirmed.
Beware DDoS: hide behind Tor, have backup route.
Smart Contracts for Side-Chains
Second Good News! Solving Interoperability
No trust needed, only well-written software.
Neither currency swapped needs support contracts!
The two currency swapped need not share cryptographic primitives.
Free option
problem? Use matching facilitator.
Smart Contracts for Side-Chains
Swapping without a large stake
Full bond needed to ensure complete transaction.
Partial bond enough to ensure balanced exchange.
Use Lightning Network style payment channels.
Exchange $1000 at a time, repeat a thousand times.
A Logic for Smart Contract
A Logic for Smart Contract
Logic? What Logic?
Law: verifying compliance, punishing non-compliance
Smart: term of art for "Algorithmic"
Smart Law: compliance with algorithmically verifiable rules
Computational Logic — but what logic?
A Logic for Smart Contract
What is a legal argument?
Two parties disagree about a claim.
Each party argues it case.
At the end, the judge finds who's right.
It's an Interactive proof.
A Logic for Smart Contract
What is an interactive proof?
Let's argue: "All sheep are the same color as mine" (in Colorado)
∃x ∀y P(x,y)
vs
∀x ∃y ¬P(x,y)
Brute force: show half a million sheep to the judge.
Interaction: I exhibit my witness x0, you exhibit yours y1
Each witness removes a quantifier.
The judge evaluates a closed formula.
A Logic for Smart Contract
Game Semantics
Translate any formula into a game.
If the formula is decidable, then good guys have a winning strategy.
If all quantifiers are over known finite data structure, good guys win.
What is the logic built on Game Semantics?
A Logic for Smart Contract
Computability Logic
Game Semantics first, syntax second.
Contains fragment of Classical, Intuitionnistic and Linear logic.
Define your own logic operators in terms of games to play.
Add fragments for Blockchain: epistemic, temporal... logic.
A Logic for Smart Contract
Higher-Level View of Smart Contracts
A contract (logical specification) is a small piece of a dApp.
A lawsuit (interactive proof) is a small piece of a contract.
An contract invocation (interaction step) is a small piece of a lawsuit.
A "contract VM" operation is a small piece of a contract invocation.
A Logic for Smart Contract
Programming using Logic
A programming language is low level when its programs
require attention to the irrelevant.
— Alan Perlis
Contract invocation, even with FP, is way too low-level.
Program in terms of logical invariants and variants of your dApp.
Use a DSL based on the appropriate logic: Computability Logic.
A Logic for Smart Contract
What Low-level VM for Contracts?
Of course use Functional Programming — Logic made computable.
Verification, not computation: no unbounded recursion.
All cryptographic primitives of all blockchains to contract about.
Access to blockchain (and other?) data via "oracles".
A Logic for Smart Contract
Issue: number of interaction steps
Number of steps: alternations of ∃ vs ∀; dichotomies
Minimize steps: Skolemization.
∀x:X ∃y:Y P(x,y) ⇔ ∃f:X→Y ∀x:X P(x,f(x))
Group all the ∃ to the left. All proofs in two steps max!
In practice: publish a detailed indexed trace of the computation.
Expensive, but paid for by the bad guy.
Trade-off between space and time.
A Logic for Smart Contract
Third Party Litigation
What if Alice and Trent collude to defraud Bob & other users?
Alice (Sybil attacker): "Gimme one million dollars!"
Trent (dishonest contract manager): "You're right, I concede."
Bob (contract user): "Hey, there's no money left in the contract!"
Solution: Bob (or anyone) can offer a better argument than Trent's
A Logic for Smart Contract
Why Formal methods?
Solutions: obvious with the right POV, unconceivable without.
Many moving parts. The least discrepancy and the edifice crumbles.
Most parts can be fixed after deployment. Contracts cannot.
If the greatest specialists lost 280M$ to a mistake in 400 loc...
A Logic for Smart Contract
Moving parts that need be consistent
- Logical specification.
- Actual code for clients.
- Actual code for servers.
- Actual code for verifiers.
- On-chain Contract to hold actors accountable.
- On-chain lawyer strategies to invoke the contract.
- Off-chain lawyer strategy to watch others and advise users.
- Tests to convince bad guys not to try.
A Logic for Smart Contract
Solution: Extract Everything from a Same Spec
Ensure all parts are in synch with each other:
Generate everything from a single specification
Reason about the specification
Reason about the generators
The Court Registry
The Need for Mutual Knowledge
Black sheep hidden in hangar.
Winning strategy requires truth + knowledge.
Good Guy Wins requires Mutual Knowledge.
Closed contract: Mutual Knowledge easy, but no Scaling.
Open contract: Scaling easy, but no Mutual Knowledge. Solution???
The Court Registry
Court Registry
"Oracle" for public data availability.
Allows for third-party verification of all transactions.
Solution to "Block Withholding Attack" (see Plasma)
Preimage not enough: Must transitively validate against schema.
The Court Registry
Court Registry Issues
WE HAVE THE SAME ISSUES AS EVERYONE ELSE
Usual 51% and 34% attacks. Consider quorum q of underwriting registrars.
If q collude: block withholding. If 1-q collude, registration denial.
"Oracle" dilemma: Closed (oligopoly), or Open (bribing is legal!)
Ideally, register on the main chain — but can it already scale?
The Court Registry
Mutual Knowledge vs Common Knowledge
Concepts from Epistemic Logic
Mutual Knowledge: what everybody knows
Gossip Network. Detects double-spending. Prevents Triple-spending.
Common Knowledge: what everybody knows that everybody knows…
Consensus. Resolves double-spending. Much more expensive.
The Court Registry
Repudiable Facilitators
Managers for Open Contracts.
Everyone can verify integrity, denounce fraud (Voice)
Repudiable / Non-custodial (Exit)
Anyone can open a rival side-chain (Enter)
Bonded so they can't profitably cheat (Skin in the Game)
Can only do the Right Thing. At worst: fail to advance.
Double as mutual verifiers. May be part of Court Registry.
The Court Registry
Fast Payment via Repudiable Facilitators
Can Solve Fast Payment at Scale: locally centralized.
Only Floating is unsafe (Limited Damages, Insurable)
Bond >> Floating (Interests Aligned)
Merchant chooses whom to trust. Fallback to slow payment.
The Court Registry
Beyond Fast Payment
DApps that extend Fast Payment: non-custodial exchange…
Anonymous rather than fast: Zcash-on-Ethereum…
Future: Develop arbitrary DApps with Computability Logic.
(Computability) Logic is not just for cryptocurrency DApps…