-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathsplash-i.html
134 lines (123 loc) · 39.4 KB
/
splash-i.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="stylesheet" href="resources/my.css" />
<link rel="stylesheet" href="resources/reveal/css/reveal.css" />
<link rel="stylesheet" href="resources/reveal/css/theme/black.css" />
<link rel="stylesheet" href="resources/reveal/lib/css/zenburn.css" />
<link rel="stylesheet" href="resources/my.css" /></head>
<body><div class="reveal"><div class="slides"><section><h1>Verifying dApp Computations on a Blockchain</h1><p> </p><p> </p><p>François-René Rideau, <em>LegiLogic</em></p><div align="center">fare@legilogic.com</div><p> </p><p> </p><p>SPLASH-I 2018, 2018-11-06</p><a href="https://gitlab.com/legicash/bbtwatcl/blob/master/splash-i.rkt"><tt>https://gitlab.com/legicash/bbtwatcl/blob/master/splash-i.rkt</tt></a></section><section><section><h1>Introduction</h1></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>The Take Home Points</h1><p> </p><div align="left">Make Blockchain dApps secure, scalable, private</div><div align="left">Offer a suitably high-level programming model</div><p> </p><div align="left">A "Blockchain" is a Verifiable Trace of Computation</div><div align="left">Use Game Semantics to prove arbitrary invariants</div><p> </p><div align="left">We're building a "Blockchain Layer 2 Operating System"</div><div align="left">Come join our R&D consortium, BELVEDERE</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Advancement Status</h1><p> </p><div align="left">This talk: BIG PICTURE ONLY.</div><div align="left">Vision of where we're going.</div><p> </p><div align="left">Current status: demo on Ethereum.</div><div align="left">Happy case only, but in good style.</div><p> </p><div align="left"><em>LegiLogic</em>: currently 2 full-time developers, hiring.</div><div align="left">Code: LGPL 2.1, but not released yet. — ASK ME FOR A PREVIEW!</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Why Blockchain matters</h1><!--This is a technical conference.
Why should anyone here even care about improving Blockchain technology?
Isn't it all a scam?
Well, just because the most visible use by volume is negative
doesn't mean it has no good uses.
Think of the Internet. Just because most uses of it are stupid or evil
doesn't mean it has no good uses. The Internet brought us together today.
And today, some people in Venezuela avoided starvation thanks to Bitcoin.--><div align="left">Bitcoin? It's for drugs, scamming, and mindless hodling!</div><div align="left">The Internet? It's for porn, spamming, and mindless trolling!</div><p> </p><!--Of course, YOUR government would never inflate the money supply
to fund world wars that leave tens of millions of innocents slaugthered.
You were born, or moved to, a country with the best political regime possible.
But for all other people, cryptocurrencies offer a chance to survive starvation
and cooperate with other individuals worldwide despite their bad government.--><div align="left">YOU live under the best government ever, with the best fiat currency.</div><div align="left">For everyone else, there's cryptocurrency.</div><p> </p><div align="left">Better technology can improve billions of lives, filter out the scams.</div><div align="left">Cryptocurrencies pressure towards better fiat currencies.</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Blockchain Problem: Scaling</h1><!--Here's one kind of problem we're trying to solve--><p> </p><div align="left">Max throughput: 7 tps for BTC, 15 for ETH (vs > 20000 tps for VISA)</div><div align="left">Latency: 60 min for BTC, 10-30 min for ETH (vs < 7 s for VISA)</div><p> </p><div align="left">Too little, too slow for casual payments!</div><div align="left">Gas, groceries, drinks, meals, etc.</div><!--flowers when you're late for mommy's birthday--><p> </p><div align="left">Reason to current limits: every node checks everything.</div><div align="left">Fundamental architecture changes needed for scaling.</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Second Blockchain Problem: Security</h1><div align="left">Writing a "smart contract" correctly is insanely hard.</div><div align="left">Parity Wallet: 400 lines, one bug, 280 M$ disappeared!</div><p> </p><div align="left">Even posting a transaction reliably is surprisingly hard.</div><div align="left">Opposition: not accidental mistakes, but deliberate attacks.</div><p> </p><div align="left">Need better languages to safely build applications.</div><div align="left">Need robust runtimes and libraries for basic services.</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Bonus Blockchain Problem: Privacy</h1><div align="left">Account holders want identities and amounts hidden</div><div align="left">In a multiparty application, minimize information sharing</div><!--Where the OO slogan of "Information hiding" is actually meaningful--><p> </p><div align="left">Pseudonymity is not anonymity.</div><div align="left">Consensus is intrinsically public.</div><p> </p><div align="left">Homomorphic Encryption. Onion Routing. MAST...</div><div align="left">A complete development platform must support many such tools.</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Usual solution?</h1><p> </p><!--Fiat currencies used to have a similar issue, in that
it used to take weeks or months for checks to clear.
But nowadays, people don't use checks anymore, they use payment cards,
which can confirm payment in a few seconds...
even though it may still take months for funds to clear in the backend.--><div align="left">Fiat currencies: fast payment via payment cards.</div><div align="left">Pro: fast because centralized. Con: custodial, trusted third party.</div><p> </p><div align="left">Why can't we have payment card equivalent for cryptocurrency?</div><div align="left">"Trusted Third Parties are security holes" — Nick Szabo</div><p> </p><div align="left">Technical centralization with economic decentralization?</div><div align="left">Centralized acceptable, custodial bad.</div></section><section><p align="right" valign="top"><font size="4"><b>Introduction</b></font></p><h1>Our Approach</h1><p> </p><div align="left">Back to Principle: What is a Blockchain?</div><div align="left">Find its essential logic, offer according tools</div><p> </p><div align="left">Take the "smart contract" analogy seriously</div><div align="left">The consensus is a court system</div><p> </p><div align="left">Write dApps using Logic</div><div align="left">Extract the computations from the Logic</div></section></section><section><section><h1>Consensus as Court</h1></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>What is a distributed consensus for?</h1><p> </p><div align="left"><em>If</em> everyone is honest and competent, a signed check is gold.</div><p> </p><div align="left">You could re-endorse it eternally and never clear it.</div><p> </p><div align="left">The Consensus is to prevent and resolve disputes.</div><p> </p><div align="left">It is analogous to a <em>Court</em> — Necessarily slow and expensive.</div><!--They involve making public pronouncements that are unequivocally recognized
by everyone all around the globe.--></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Don't go to Court for Casual Payment</h1><p> </p><div align="left">Court: yes to buy a house, a car.</div><p> </p><div align="left">Court: not to buy coffee.</div><p> </p><div align="left">Make casual payments with payment processors: it scales!</div><p> </p><div align="left">Only go to Court to prevent and resolve disputes.</div></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Analogy between Consensus & Court</h1><table align="right" width="100%"><tr><th width="8%"><font size="6"><span style="color:#ffffff;"></span></font></th><th width="8%"><font size="6"><span style="color:#ffffff;">human law</span></font></th><th width="8%"><font size="6"><span style="color:#ffffff;">smart law</span></font></th></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">participants</span></font></th><td><span style="color:#ffffff;">humans</span></td><td><span style="color:#ffffff;">machines</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">enforcement</span></font></th><td><span style="color:#ffffff;">social</span></td><td><span style="color:#ffffff;">algorithmic</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">arbiter</span></font></th><td><span style="color:#ffffff;">judge</span></td><td><span style="color:#ffffff;">consensus</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">register</span></font></th><td><span style="color:#ffffff;">court clerk, etc.</span></td><td><span style="color:#ffffff;">account table, utxos</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">interpretation</span></font></th><td><span style="color:#ffffff;">flexible</span></td><td><span style="color:#ffffff;">rigid</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">outcome</span></font></th><td><span style="color:#ffffff;">uncertain</span></td><td><span style="color:#ffffff;">certain (*)</span></td></tr></table><!--(*) certain within operating parameters--></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Analogies for Functional Programmers</h1><p> </p><div align="left">Analogy: one Abstraction applied twice...</div><p> </p><div align="left">Break down: ... to different parameters.</div><p> </p><p> </p><div align="left">Common Abstraction: Adjudication</div><p> </p><div align="left">Different Parameters: Humans vs Machines</div><!--Of course, neither is a substitute for the other.
That ought to be obvious, but apparently isn't,
so it is important to mention it.--></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>What Law <em>CANNOT</em> do</h1><p> </p><div align="left"><q>Why don't we just make X illegal?</q></div><p> </p><div align="left">You can't decree bad behavior away.</div><p> </p><div align="left">Murder is illegal, yet it still happens.</div><p> </p><div align="left">Law can never prevent anyone from ever doing anything.</div></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>What Law <em>CAN</em> do</h1><p> </p><div align="left">It can only hold actors accountable for what they do.</div><p> </p><div align="left">Provide <em>incentives</em>. Game Theory</div><p> </p><div align="left">Skin in the game.</div><p> </p><div align="left">Human Law: can get caught. Smart Law: must deposit collateral.</div></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Economic Analysis of Law</h1><p> </p><div align="left">Branch of Economics.</div><p> </p><div align="left">Study how Law affects incentives of all participants.</div><p> </p><div align="left">Consequences, not intentions.</div><p> </p><div align="left">Applies to lawmakers, too (Public Choice Theory)</div></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Kinds of Freedom vs Alignment of Interests</h1><table align="right" width="100%"><tr><th width="8%"><font size="6"><span style="color:#ffffff;"></span></font></th><th width="8%"><font size="6"><span style="color:#ffffff;">Allowed Individual Action</span></font></th><th width="8%"><font size="6"><span style="color:#ffffff;">Effect on Interests</span></font></th></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">None</span></font></th><td><span style="color:#ffffff;">Just shut up & obey</span></td><td><span style="color:#ffffff;">Generate Chaos, Oppose Interests</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">Voice</span></font></th><td><span style="color:#ffffff;">Say whatever you want, Vote</span></td><td><span style="color:#ffffff;">Create Coordination, Consumes Alignment</span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">Exit</span></font></th><td><span style="color:#ffffff;">Repudiate a bad provider</span></td><td><span style="color:#ffffff;"><div>Finds Alignment, <br /> Within Limited Choice</div></span></td></tr><tr><th width="8%"><font size="6"><span style="color:#ffffff;">Enter</span></font></th><td><span style="color:#ffffff;">Found a new competitor</span></td><td><span style="color:#ffffff;">Create Alignment, Generate Order</span></td></tr></table></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Aligning interests of Payment Processors</h1><p> </p><div align="left">On a blockchain, limited Voice, but unlimited Exit and Enter.</div><p> </p><div align="left">Keep payment processors honest via Exit and Enter.</div><p> </p><div align="left">Exit: Repudiation, on chain, or <em>en masse</em> to another processor!</div><p> </p><div align="left">Enter: Anyone can cook.</div></section><section><p align="right" valign="top"><font size="4"><b>Consensus as Court</b></font></p><h1>Consensus as Court</h1><p> </p><div align="left">Fruitful Point of View</div><p> </p><div align="left">Consensus provides arbitration, not transactions</div><p> </p><div align="left">Fast Transactions on a side-chain</div><p> </p><div align="left">Go to consensus only to resolve disputes</div></section></section><section><section><h1>Smart Contracts for Side-Chains</h1></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>First good news! Solving Scaling</h1><p> </p><div align="left">Do <em>not</em> publish transactions on the main chain — WIN!</div><p> </p><div align="left">Non-publication is infinitely faster than publication.</div><!--In the time you publish one transaction,
I can "not publish" one billion trillion bajillion transactions, even ℵ₄₂--><p> </p><div align="left">Publish title registration, in large batches.</div><p> </p><div align="left">Publish law suits — few and far between thanks to good incentives</div></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>Non publication is for contracts, too!</h1><p> </p><div align="left">Publish contract with salted hashes of the clauses (Bitcoin MAST).</div><p> </p><div align="left">Fulfill all obligations, then settle contract.</div><p> </p><div align="left">Only if one party fails, reveal one clause to get compensation.</div><p> </p><div align="left">Smaller, Cheaper, Faster, More Private.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>What are contracts for?</h1><p> </p><div align="left">Mechanism to create alignment of interests.</div><!--Toward a common activity, when these interests would otherwise be antagonistic.--><p> </p><div align="left">Plan A: <em>Never</em> going to Court.</div><!--Having the judge decide is plan Z.--><p> </p><div align="left">Contracts are <em>not</em> for "evaluating code on the blockchain"</div><!--Evaluating code on the blockchain is extremely slow and expensive,
literally millions of times more so than doing it on a regular computer.
That's never a good first choice.
[Justification for million:
You can rent a Cloud VM for about $10 per month. That's 3.8e-8 USD/s.
You pay for on-chain computations at about 1 GAS per microsecond, at 555 USD/ETH and 10e-8 ETH per GAS,
for 5.55 USD/s.
https://docs.google.com/spreadsheets/d/1m89CVujrQe5LAFJ8-YAUCcNK950dUzMQPMJBxRtGCqs/edit#gid=0
See also
https://youtu.be/a-xHiI-G_CQ
]--><p> </p><div align="left">Do all the work in side-chains.</div><!--Stay off the main chain.--></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>What do contracts consist in?</h1><p> </p><div align="left">Mutual obligations.</div><p> </p><div align="left">A series of clauses.</div><p> </p><div align="left">In each clause, a participant makes a promise.</div><p> </p><div align="left">If they break their promise, a sanction punishes them.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>Example Contract: Atomic Swap</h1><p> </p><div align="left">Exchange $1000 worth between Monero and Zcash.</div><!--But neither of us wants to be first to send.--><p> </p><div align="left">Sign Ethereum contract each¹ posting a bond worth $4000.</div><!--I will promise to pay you $1000 worth of Bitcoin, or I'll lose a $4000 worth stake in Ethereum.
You will promise to pay me $1000 worth of Zcash, or you'll lose a $4000 worth stake in Ethereum.--><!--Actually, only the one who will pay second needs to be bonded--><!--Bound parties are strongly interested in doing their part.--><p> </p><div align="left">Settlement is slow, but the contract is binding as soon as confirmed.</div><p> </p><div align="left">Beware DDoS: hide behind Tor, have backup route.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>Second Good News! Solving Interoperability</h1><!--And that's what I mean by "Binding Blockchains Together"--><p> </p><div align="left">No trust needed, only well-written software.</div><!--In the end, if we both use competently written software,
we will be able to complete the trade, even though we don't trust each other.--><p> </p><div align="left">Neither currency swapped needs support contracts!</div><!--As long as short term parameters for the Proof-of-Work or Proof-of-Stake algorithm
for each chain can be modelled in the chain in which the contracts are signed.--><p> </p><div align="left">The two currency swapped need not share cryptographic primitives.</div><!--Once again, the chain with the contracts needs support the other ones,
but they need not support each other.
Another very different way to bridge cryptographic primitives in some cases
could be to use zk-SNARK to show that some precursor on one chain corresponds
to another precursor on the other chain.--><p> </p><div align="left"><q>Free option</q> problem? Use matching facilitator.</div><!--Problem intrinsic to all smart contracts:
The last one to sign always has the option not to sign.
There are various alternatives in incentive design.--></section><section><p align="right" valign="top"><font size="4"><b>Smart Contracts for Side-Chains</b></font></p><h1>Swapping without a large stake</h1><p> </p><div align="left">Full bond needed to ensure complete transaction.</div><p> </p><div align="left">Partial bond enough to ensure balanced exchange.</div><p> </p><div align="left">Use Lightning Network style payment channels.</div><p> </p><div align="left">Exchange $1000 at a time, repeat a thousand times.</div><!--You get a smaller guarantee, for a smaller bond.
Social enforcement: whoever fails to complete their part
will be kicked out of exchanges forever.--></section></section><section><section><h1>A Logic for Smart Contract</h1></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Logic? What Logic?</h1><p> </p><div align="left">Law: verifying compliance, punishing non-compliance</div><p> </p><div align="left">Smart: term of art for "Algorithmic"</div><p> </p><div align="left">Smart Law: compliance with algorithmically verifiable rules</div><p> </p><div align="left">Computational Logic — but <em>what</em> logic?</div><!--
--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>What is a legal argument?</h1><p> </p><div align="left">Two parties disagree about a claim.</div><p> </p><div align="left">Each party argues it case.</div><p> </p><div align="left">At the end, the judge finds who's right.</div><p> </p><div align="left">It's an <em>Interactive proof</em>.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>What is an interactive proof?</h1><div align="left">Let's argue: "All sheep are the same color as mine" (in CO)</div><span class="fragment" data-fragment-index="1"><div align="center"><em>∃x ∀y P(x,y)</em></div></span><span class="fragment" data-fragment-index="3"><div align="center"><em>vs</em></div>
<div align="center"><em>∀x ∃y ¬P(x,y)</em></div></span><p> </p><span class="fragment" data-fragment-index="2"><div align="left">Brute force: show half a million sheep to the judge.</div></span><!--How can we argue in front of a judge whose time is very expensive?
We could exhibit all the sheep one after the other in front of the court.
It would take a lot of time to exhibit half a million sheep while following all legal procedures,
and would cost a fortune to complete,
assuming the judge doesn't quickly fall asleep, doesn't die of boredom,
and doesn't die of old age either
--- before we're done.--><p> </p><span class="fragment" data-fragment-index="4"><div align="left">Interaction: I exhibit my witness <em>x0</em>, you exhibit yours <em>y1</em></div></span><!--Another solution is to find two honest lawyers who will each
honestly and capably argue their case the best possible way.
If I argue that all sheep in Colorado are white,
the judge will ask my lawyer to produce a sheep, and the sheep has better be white;
this establishes existence.
To prove universality, I cannot afford to show all the other sheep to the judge,
or even a large fraction.
But I can challenge you to show a sheep of a different color.--><span class="fragment" data-fragment-index="5"><div align="left">Each witness removes a quantifier.</div>
<div align="left">The judge evaluates a closed formula.</div></span><!--Interestingly, they are called witnesses in formal logic as well as in law.
And of course, interactive proofs are not just for sheep.
I can argue that the latest entry for my account on the blockchain has ETH 1000, that you owe me.
You now have to either show a more recent entry for my account with less than that, or you owe me.
The formula for the latest entry is that there exists an entry such that for all entries,
the second entry is earlier than the former.--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Game Semantics</h1><p> </p><div align="left">Translate any formula into a game.</div><p> </p><div align="left"><em>If</em> the formula is decidable, then good guys have a winning strategy.</div><p> </p><div align="left">If all quantifiers are over known finite data structure, good guys win.</div><p> </p><div align="left">What is the logic built on Game Semantics?</div><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Computability Logic</h1><p> </p><div align="left">Game Semantics first, syntax second.</div><p> </p><div align="left">Contains fragment of Classical, Intuitionnistic and Linear logic.</div><p> </p><div align="left">Define your own logic operators in terms of games to play.</div><p> </p><div align="left">Add fragments for Blockchain: epistemic, temporal... logic.</div><!--Propositional Logic + Quantification over large data structures
Resource Conservation: Linear Logic
Conservation through Time & Timeouts: Temporal Logic
Ownership: Epistemic Logic
Third party litigation: Multi-player games!--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Higher-Level View of Smart Contracts</h1><p> </p><div align="left">A contract (logical specification) is a small piece of a dApp.</div><p> </p><div align="left">A lawsuit (interactive proof) is a small piece of a contract.</div><p> </p><div align="left">An contract invocation (interaction step) is a small piece of a lawsuit.</div><p> </p><div align="left">A "contract VM" operation is a small piece of a contract invocation.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Programming using Logic</h1><p><br />
<cite>A programming language is low level when its programs <br /> require attention to the irrelevant.</cite>
— Alan Perlis</p><p> </p><div align="left">Contract invocation, even with FP, is <em>way</em> too low-level.</div><p> </p><div align="left">Program in terms of logical invariants and variants <em>of your dApp</em>.</div><p> </p><div align="left">Use a DSL based on the appropriate logic: Computability Logic.</div><p> </p><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>What Low-level VM for Contracts?</h1><p> </p><div align="left">Of course use Functional Programming — Logic made computable.</div><p> </p><div align="left">Verification, not computation: no unbounded recursion.</div><!--No "Turing-equivalence" needed. Bitcoiners will be happy.--><p> </p><div align="left">All cryptographic primitives of all blockchains to contract about.</div><p> </p><div align="left">Access to blockchain (and other?) data via "oracles".</div><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Issue: number of interaction steps</h1><div align="left">Number of steps: alternations of ∃ vs ∀; dichotomies</div><!--Mind though that each time you challenge the other party,
you have to give them ample enough time to respond; say two hours.
This means that a formula with a lot of alternations between ∃ vs ∀
(or non-dependent sums and products),
say to do a dichotomy search or two, may take a week;
a badly written specification with a thousand alternations
may lead taking months to interactively argue a case.
Unary representations, such as naïve blockchaining,
are worst of all.--><p> </p><!--Happily, there are techniques to minimize the number of steps required
to complete an interactive proof.--><div align="left">Minimize steps: Skolemization.</div><div align="center"><em>∀x:X ∃y:Y P(x,y) ⇔ ∃f:X→Y ∀x:X P(x,f(x))</em></div><div align="left">Group all the ∃ to the left. All proofs in two steps max!</div><!--In the first case, the adversary challenges you with an X, and you reply with a Y.
In the second case, you publish in advance a map associating to whichever potential challenge in X
your response in Y, then you challenge the adversary with an X.
Actually, publishing a map in advance also lets the adversary search the map for data,
so he further doesn't have to go through a lengthy round of challenges and responses
to search the map for content.
On the other hand, data that is so well indexed as to be searchable for justifications
and counter-justifications to an exit transaction could potentially be used
to survive the lack of a court registry(?)
Lambda-lifting? not really.--><p> </p><div align="left">In practice: publish a detailed indexed trace of the computation.</div><div align="left">Expensive, but paid for by the bad guy.</div><div align="left">Trade-off between space and time.</div><!--If the full index can be too expensive, keep it four steps, or six, etc.
(Beware though that proofs in more than two steps require third-party litigation.)--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Third Party Litigation</h1><p> </p><div align="left">What if Alice and Trent collude to defraud Bob & other users?</div><p> </p><div align="left">Alice (Sybil attacker): "Gimme one million dollars!"</div><div align="left">Trent (dishonest contract manager): "You're right, I concede."</div><div align="left">Bob (contract user): "Hey, there's no money left in the contract!"</div><p> </p><div align="left">Solution: Bob (or anyone) can offer a better argument than Trent's</div><!--Alice gets thrown out of court, Trent loses his license,
Bob gets rewarded based on court fees, etc.
Of course, to avoid double jeopardy (and double-spending of damages),
only the first successful counter-claimant wins.
Unlike Human law, no verifiable notion of "having standing/interest in the case"
All identities are pseudonymous, anyway.--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Why Formal methods?</h1><p> </p><div align="left">Solutions: obvious with the right POV, unconceivable without.</div><!--You might not even see the issue without Formal Methods.--><p> </p><div align="left">Many moving parts. The least discrepancy and the edifice crumbles.</div><p> </p><div align="left">Most parts can be fixed after deployment. Contracts cannot.</div><p> </p><div align="left">If the greatest specialists lost 280M$ to a mistake in 400 loc...</div><!----></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Moving parts that need be consistent</h1><div align="left">- Logical specification.</div><div align="left">- Actual code for clients.</div><div align="left">- Actual code for servers.</div><div align="left">- Actual code for verifiers.</div><div align="left">- On-chain Contract to hold actors accountable.</div><div align="left">- On-chain lawyer strategies to invoke the contract.</div><div align="left">- Off-chain lawyer strategy to watch others and advise users.</div><!--Watch activity on the chain,
take correct steps,
stop users from making mistakes,
explain what's happening to users.--><div align="left">- Tests to convince bad guys not to try.</div><!--Proving it correct is necessary but not enough.--></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Solution: Extract Everything from a Same Spec</h1><p> </p><div align="left">Ensure all parts are in synch with each other:</div><div align="left">Generate everything from a single specification</div><p> </p><div align="left">Present: run a multiparty distributed computation</div><div align="left">Past: check invariants of verifiable traces</div><div align="left">Future: reason about all possible future traces</div></section><section><p align="right" valign="top"><font size="4"><b>A Logic for Smart Contract</b></font></p><h1>Alternate Validation Backends</h1><small><table><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff"></th><th fgcolor="#00ff00" bgcolor="#b4b4ff" width="25%">Economic validation</th><th fgcolor="#00ff00" bgcolor="#b4b4ff" width="25%">Interactive Proof</th><th fgcolor="#00ff00" bgcolor="#b4b4ff" width="25%">Non-Interactive Proof</th></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Consensus</th><td fgcolor="#00ff00" bgcolor="#b4ffb4">Provided!</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">Required</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">Required</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Captured at</th><td fgcolor="#00ff00" bgcolor="#ffb4b4">34%</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">100%</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">100%</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Cost</th><td fgcolor="#00ff00" bgcolor="#ffb4b4">Capital-intensive</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">Cheap</td><td fgcolor="#00ff00" bgcolor="#b4b4ff">Expensive</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Who pays</th><td fgcolor="#00ff00" bgcolor="#ffb4b4">Everyone</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">Bad guy</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">Good guy</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Latency</th><td fgcolor="#00ff00" bgcolor="#b4ffb4">milliseconds</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">hours</td><td fgcolor="#00ff00" bgcolor="#b4b4ff">seconds</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Quantifiers</th><td fgcolor="#00ff00" bgcolor="#b4ffb4">∃ ∀</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">+ ∃ ∀</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">∃ only</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Privacy</th><td fgcolor="#00ff00" bgcolor="#ffb4b4">Must be public</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">Can be private</td><td fgcolor="#00ff00" bgcolor="#b4ffb4">Can be private</td></tr><tr><th fgcolor="#00ff00" bgcolor="#b4b4ff">Complexity</th><td fgcolor="#00ff00" bgcolor="#b4ffb4">Done already</td><td fgcolor="#00ff00" bgcolor="#ffb4b4">Lots of moving parts</td><td fgcolor="#00ff00" bgcolor="#b4b4ff">Few complex parts</td></tr></table></small></section></section><section><section><h1>The Court Registry</h1></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>The Need for Shared Knowledge</h1><p> </p><div align="left">Black sheep hidden in hangar.</div><p> </p><div align="left">Winning strategy requires truth + knowledge.</div><div align="left">Good Guy Wins requires <em>Shared Knowledge</em>.</div><p> </p><div align="left"><em>Closed contract</em>: Shared Knowledge easy, but no Scaling.</div><div align="left"><em>Open contract</em>: Scaling easy, but no Shared Knowledge. Solution???</div><!----></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Court Registry</h1><p> </p><div align="left">"Oracle" for public data availability.</div><p> </p><div align="left">Allows for third-party verification of all transactions.</div><p> </p><div align="left">Solution to "Block Withholding Attack" (see Plasma)</div><p> </p><div align="left">Preimage not enough: Must transitively validate against schema.</div><!--Against data schema--></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Court Registry Issues</h1><p> </p><div align="left">WE HAVE THE SAME ISSUES AS EVERYONE ELSE</div><p> </p><div align="left">50% attack. Consider quorum <em>q</em> of underwriting registrars.</div><div align="left">If <em>q</em> collude: block withholding. If <em>1-q</em> collude, registration denial.</div><p> </p><div align="left">"Oracle" dilemma: Closed (oligopoly), or Open (bribing is legal!)</div><!--Open Oracle == "TCR", Token-Curated Registry.
Our current solution: closed for now, repudiate as soon as fishy.--><p> </p><div align="left">Ideally, register on the main chain — but can it already scale?</div></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Shared Knowledge vs Common Knowledge</h1><p> </p><div align="left">Concepts from <em>Epistemic Logic</em></div><p> </p><div align="left">Shared Knowledge: what <em>everybody knows</em></div><div align="left">Gossip Network. Detects double-spending. Prevents Triple-spending.</div><p> </p><div align="left">Common Knowledge: what <em>everybody knows that everybody knows…</em></div><div align="left">Consensus. Resolves double-spending. Much more expensive.</div><!--Shared Knowledge can serve as a precursor to Common Knowledge.
Obviously it is strictly less powerful than Common Knowledge, and much cheaper to achieve:
it requires no synchronization between the participants and can be reasonably achieved in seconds.
Meanwhile Common Knowledge takes tens of minutes to achieve with current technology.
(Even though Hashgraph claims it can achieve Common Knowledge in a matter of seconds
using gossip-on-gossip, though it's unclear how well this result applies
to an open adversarial network.)
Keeping the trace always beats just doing the thing. Optimal by construction.--><p> </p><!--
--></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Repudiable Facilitators</h1><p> </p><div align="left">Managers for Open Contracts.</div><p> </p><div align="left">Everyone can verify integrity, denounce fraud (Voice)</div><div align="left">Repudiable / Non-custodial (Exit)</div><div align="left">Anyone can open a rival side-chain (Enter)</div><div align="left">Bonded so they can't profitably cheat (Skin in the Game)</div><div align="left">Can only do the Right Thing. At worst: fail to advance.</div><p> </p><div align="left">Double as mutual verifiers. May be part of Court Registry.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Fast Payment via Repudiable Facilitators</h1><p> </p><div align="left">Can Solve Fast Payment at Scale: locally centralized.</div><p> </p><div align="left">Only Floating is unsafe (Limited Damages, Insurable)</div><p> </p><div align="left">Bond >> Floating (Interests Aligned)</div><p> </p><div align="left">Merchant chooses whom to trust. Fallback to slow payment.</div><!----></section><section><p align="right" valign="top"><font size="4"><b>The Court Registry</b></font></p><h1>Beyond Fast Payment</h1><p> </p><div align="left">dApps that extend Fast Payment: non-custodial exchange…</div><p> </p><div align="left">Anonymous rather than fast: Zcash-on-Ethereum…</div><p> </p><div align="left">Future: Develop arbitrary dApps with Computability Logic.</div><p> </p><div align="left">(Computability) Logic is not just for cryptocurrency dApps…</div><!----></section></section><section><section><h1>Conclusion</h1></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>The Take Home Points (redux)</h1><p> </p><div align="left">Make Blockchain dApps secure, scalable, private</div><div align="left">Offer a suitably high-level programming model</div><p> </p><div align="left">A "Blockchain" is a Verifiable Trace of Computation</div><div align="left">Use Game Semantics to prove arbitrary invariants</div><p> </p><div align="left">We're building a "Blockchain Layer 2 Operating System"</div><div align="left">Come join our R&D consortium, BELVEDERE</div></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>The Meta-Story</h1><p> </p><div align="left">Given a problem, seek its essence, stripped from incidentals.</div><p> </p><div align="left">Find the ability to reason logically, for machines and humans.</div><p> </p><div align="left">Match the structure of the computation to that of the logic.</div><p> </p><div align="left">… That's the essence of Functional Programming / Category Theory!</div><!--When you go to the essence, make it explicit, and strip everything else...
You've got the approach of Category Theory,
which is what is good about Functional Programming--></section><section><p align="right" valign="top"><font size="4"><b>Conclusion</b></font></p><h1>Contact</h1><p> </p><div align="left">I NEED MORE INFO! Medium <a href="https://medium.com/alacris"><tt>https://medium.com/alacris</tt></a></div><p> </p><div align="left">TAKE MY MONEY! Our website <a href="https://alacris.io/"><tt>https://alacris.io/</tt></a></div><p> </p><div align="left">I WANT TO HELP! Telegram <a href="https://t.me/alacrisio"><tt>https://t.me/alacrisio</tt></a></div><p> </p><div align="left">SHOW ME THE CODE! <a href="https://j.mp/LegicashCodeReleasePreview"><tt>https://j.mp/LegicashCodeReleasePreview</tt></a></div></section></section></div></div>
<script src="resources/reveal/lib/js/head.min.js"></script>
<script src="resources/reveal/js/reveal.min.js"></script>
<script>
//<![CDATA[
Reveal.initialize({
dependencies: [
{src: "resources/reveal/plugin/highlight/highlight.js",
async: true, callback: () => hljs.initHighlightingOnLoad()}],
controls: false})
//]]>
</script></body></html>