-
Notifications
You must be signed in to change notification settings - Fork 55
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Implement call, chain, inspect and inspect-full meta commands
* Fix a bug on the REPL, which was always computing with a nil env * Fix a bug on the REPL test, which made the test not capture the bug above * Port the demo files from clutch
- Loading branch information
1 parent
f5ab086
commit b9d8673
Showing
13 changed files
with
713 additions
and
59 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,242 @@ | ||
;; Let's build a functional bank. | ||
|
||
;; We'll start by defining a tiny database of people and their balances. | ||
|
||
!(def people '((:first-name "Alonzo" :last-name "Church" :balance 123 :id 0) | ||
(:first-name "Alan" :last-name "Turing" :balance 456 :id 1) | ||
(:first-name "Satoshi" :last-name "Nakamoto" :balance 9000 :id 2))) | ||
|
||
;; We need a way to look up keys in the database records, so we define a getter. | ||
|
||
!(defrec get (lambda (key plist) | ||
(if plist | ||
(if (eq key (car plist)) | ||
(car (cdr plist)) | ||
(get key (cdr (cdr plist)))) | ||
nil))) | ||
|
||
;; Let's test it by getting the last name of the first person. | ||
|
||
(get :last-name (car people)) | ||
|
||
;; We also need some functional helpers. Map applies a function to each element of a list. | ||
|
||
!(defrec map (lambda (f list) | ||
(if list | ||
(cons (f (car list)) | ||
(map f (cdr list))) | ||
()))) | ||
|
||
;; Filter removes elements of a list that don't satisfy a predicate function. | ||
|
||
!(defrec filter (lambda (pred list) | ||
(if list | ||
(if (pred (car list)) | ||
(cons (car list) (filter pred (cdr list))) | ||
(filter pred (cdr list))) | ||
()))) | ||
|
||
;; Let's write a predicate that is true when an entry's balance is at least a specified amount. | ||
|
||
!(def balance-at-least? (lambda (x) | ||
(lambda (entry) | ||
(>= (get :balance entry) x)))) | ||
|
||
;; Putting it together, let's query the database for the first name of people with a balance of at least 200. | ||
|
||
(map (get :first-name) (filter (balance-at-least? 200) people)) | ||
|
||
;; And let's get everyone's balance. | ||
|
||
(map (get :balance) people) | ||
|
||
;; We can define a function to sum a list of values recursively. | ||
|
||
!(defrec sum (lambda (vals) | ||
(if vals | ||
(+ (car vals) (sum (cdr vals))) | ||
0))) | ||
|
||
;; Apply this to the balances, and we can calculate the total funds in a database. | ||
|
||
!(def total-funds (lambda (db) (sum (map (get :balance) db)))) | ||
|
||
;; Let's snapshot the initial funds. | ||
|
||
!(def initial-total-funds (emit (total-funds people))) | ||
|
||
;; We can check a database to see if funds were conserved by comparing with the inital total. | ||
|
||
!(def funds-are-conserved? (lambda (db) (= initial-total-funds (total-funds db)))) | ||
|
||
;; Here's a setter. | ||
|
||
!(def set (lambda (key value plist) | ||
(letrec ((aux (lambda (acc plist) | ||
(if plist | ||
(if (eq key (car plist)) | ||
(aux (cons key (cons value acc)) | ||
(cdr (cdr plist))) | ||
(aux (cons (car plist) | ||
(cons (car (cdr plist)) acc)) | ||
(cdr (cdr plist)))) | ||
acc)))) | ||
(aux () plist)))) | ||
|
||
;; We can use it to change a balance. | ||
|
||
(set :balance 666 (car people)) | ||
|
||
;; More useful is an update function that modifes a field based on its current value. | ||
|
||
!(def update (lambda (key update-fn plist) | ||
(letrec ((aux (lambda (acc plist) | ||
(if plist | ||
(if (eq key (car plist)) | ||
(aux (cons key (cons (update-fn (car (cdr plist))) acc)) | ||
(cdr (cdr plist))) | ||
(aux (cons (car plist) | ||
(cons (car (cdr plist)) acc)) | ||
(cdr (cdr plist)))) | ||
acc)))) | ||
(aux () plist)))) | ||
|
||
;; For example, we can double Church's balance. | ||
|
||
(update :balance (lambda (x) (* x 2)) (car people)) | ||
|
||
;; And, here's a function that updates only the rows that satisfy a predicate. | ||
|
||
!(def update-where (lambda (predicate key update-fn db) | ||
(letrec ((aux (lambda (db) | ||
(if db | ||
(if (predicate (car db)) | ||
(cons (update key update-fn (car db)) | ||
(aux (cdr db))) | ||
(cons (car db) | ||
(aux (cdr db)))) | ||
nil)))) | ||
(aux db)))) | ||
|
||
;; Let's write a predicate for selecting rows by ID. | ||
|
||
!(def has-id? (lambda (id x) (eq id (get :id x)))) | ||
|
||
;; That lets us change the first letter of the first name of the person with ID 2. | ||
|
||
(update-where (has-id? 2) :first-name (lambda (x) (strcons 'Z' (cdr x))) people) | ||
|
||
;; Finally, let's put it all together and write a function to send balances from one account to another. | ||
|
||
;; We select the from account by filtering on id, | ||
|
||
;; Check that its balance is at least the transfer amount, | ||
|
||
;; Then update both the sender and receiver's balance by the amount. | ||
|
||
;; If the sender doesn't have enough funds, we display an insufficient funds message, and return the database unchanged. | ||
|
||
!(def send (lambda (amount from-id to-id db) | ||
(let ((from (car (filter (has-id? from-id) db)))) | ||
(if (balance-at-least? amount from) | ||
(let ((debited (update-where (has-id? from-id) :balance (lambda (x) (- x amount)) db)) | ||
(credited (update-where (has-id? to-id) :balance (lambda (x) (+ x amount)) debited))) | ||
credited) | ||
(begin (emit "INSUFFICIENT FUNDS") db))))) | ||
|
||
;; In token of this new function, we'll call our database of people a ledger. | ||
|
||
!(def ledger people) | ||
|
||
;; We can send 200 from account 1 to account 0. | ||
|
||
!(def ledger1 (send 200 1 0 ledger)) | ||
|
||
ledger1 | ||
|
||
;; And assert that funds were conserved. (Nothing was created or destroyed.) | ||
|
||
!(assert (funds-are-conserved? ledger1)) | ||
|
||
;; Or, using the original ledger, we can try sending 200 from account 0 to 1. | ||
|
||
!(def ledger2 (send 200 0 1 ledger)) | ||
|
||
ledger2 | ||
|
||
;; Notice that this transaction fails due to insufficient funds. However, | ||
|
||
!(assert (funds-are-conserved? ledger2)) | ||
|
||
;; funds are still conserved | ||
|
||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; | ||
;; Functional Commitment to a Database Value | ||
|
||
;; Let's define a function that takes a database and returns a transfer function. | ||
|
||
;; Transfer function takes an amount, a source id, and a destination id, then attempts to send the funds. | ||
|
||
!(def fn<-db (lambda (db) | ||
(lambda (transfer) | ||
(let ((amount (car transfer)) | ||
(rest (cdr transfer)) | ||
(from-id (car rest)) | ||
(rest (cdr rest)) | ||
(to-id (car rest))) | ||
(send (emit amount) (emit from-id) (emit to-id) (emit db)))))) | ||
|
||
;; Now let's create a transfer function for our ledger, and commit to it. | ||
|
||
!(commit (fn<-db ledger)) | ||
|
||
;; Now we can open the committed ledger transfer function on a transaction. | ||
|
||
!(call 0x014a94be6a32b6c74be26071f627aff0a06ef3caade04d335958b8a3bb818925 '(1 0 2)) | ||
|
||
;; And the record reflects that Church sent one unit to Satoshi. | ||
|
||
;; Let's prove it. | ||
|
||
!(prove) | ||
|
||
;; We can verify the proof.. | ||
|
||
!(verify "Nova_Pallas_10_3ec93e16c42eb6822e1597d915c0a1f284fea322297786eb506bd814e29e33d3") | ||
|
||
;; Unfortunately, this functional commitment doesn't let us maintain state. | ||
;; Let's turn our single-transaction function into a chained function. | ||
|
||
!(def chain<-db (lambda (db secret) | ||
(letrec ((foo (lambda (state msg) | ||
(let ((new-state ((fn<-db state) msg))) | ||
(cons new-state (hide secret (foo new-state))))))) | ||
(foo db)))) | ||
|
||
;; We'll call this on our ledger, and protect write-access with a secret value (999). | ||
|
||
!(commit (chain<-db ledger 999)) | ||
|
||
;; Now we can transfer one unit from Church to Satoshi like before. | ||
|
||
!(chain 0x0757a47095c97d0a58a8ff66a2146949ee9d60d3f0a82887c203edf1748be711 '(1 0 2)) | ||
|
||
!(prove) | ||
|
||
!(verify "Nova_Pallas_10_118481b08f97e5ea84499dd305d5c2b86089d5d5e5253e6c345119d55020bde3") | ||
|
||
;; Then we can transfer 5 more, proceeding from the new head of the chain. | ||
|
||
!(chain 0x0d0b562063718f3623c1749268da4dd74ed33142edc411f4e74d7a84e64f3f30 '(5 0 2)) | ||
|
||
!(prove) | ||
|
||
!(verify "Nova_Pallas_10_045d2fef5862777cf50a9dc8df50650f1aebfcbfb8135adfea57fb8f45389af4") | ||
|
||
;; And once more, this time we'll transfer 20 from Turing to Church. | ||
|
||
!(chain 0x3e232dc8d44c85697fa4205d0d945014d34b980af498aed9194216c27c489e05 '(20 1 0)) | ||
|
||
!(prove) | ||
|
||
!(verify "Nova_Pallas_10_25c76318cda48570568b9bb766ee9a906790c4dc94c96b1d6549e96c3bff8aa7") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
;; First, we define a stateful function that adds its input to an internal counter, initialized to 0. | ||
|
||
;; The function returns a new counter value and a commitment to a replacement function wrapping the new counter. | ||
|
||
!(commit (letrec ((add (lambda (counter x) | ||
(let ((counter (+ counter x))) | ||
(cons counter (commit (add counter))))))) | ||
(add 0))) | ||
|
||
;; We chain a next commitment by applying the committed function to a value of 9. | ||
|
||
!(chain 0x06042852d90bf409974d1ee3bc153c0f48ea5512c9b4f697561df9ad7b5abbe0 9) | ||
|
||
;; The new counter value is 9, and the function returns a new functional commitment. | ||
|
||
;; This new commitment is now the head of the chain. | ||
|
||
;; Next, we ccreate a proof of this transtion. | ||
|
||
!(prove) | ||
|
||
;; We can verify the proof. | ||
|
||
!(verify "Nova_Pallas_10_241f5c936d5c11e9c99b52017354738f9024c084fdfe49da9ad4a39fb2fe6619") | ||
|
||
;; Now let's chain another call to the new head, adding 12 to the counter. | ||
|
||
!(chain 0x251ccd3ecf6ae912eeb6558733b04b50e0b0c374a2dd1b797fcca84b0d9a8794 12) | ||
|
||
;; Now the counter is 21, and we have a new head commitment. | ||
|
||
;; Prove it. | ||
|
||
!(prove) | ||
|
||
;; And verify. | ||
|
||
!(verify "Nova_Pallas_10_369621a97ad8521369e49e773e0a531b0162d2f193877fbdfb308d3b2a23eea2") | ||
|
||
;; One more time, we'll add 14 to the head commitment's internal state. | ||
|
||
!(chain 0x281605259696cd2529c00806465c9726d81df4ccd2c3500312c991c1fd572592 14) | ||
|
||
;; 21 + 14 = 35, as expected. | ||
|
||
;; Prove. | ||
|
||
!(prove) | ||
|
||
;; Verify. | ||
|
||
!(verify "Nova_Pallas_10_057ebe2b592d6d82c1badc86493f6118a70c81aebb3b53a054d9b2517ad118f2") | ||
|
||
;; Repeat indefinitely. | ||
|
||
;; At every step, we have proof that the head commitment was correctly derived from the previous and some input. | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,29 @@ | ||
;; Let's define a function: f(x) = 3x^2 + 9x + 2 | ||
|
||
!(def f (lambda (x) (+ (* 3 (* x x)) (+ (* 9 x) 2)))) | ||
|
||
!(assert-eq (f 5) 122) | ||
|
||
;; We can create a cryptographic commitment to f. | ||
|
||
!(commit f) | ||
|
||
;; We open the functional commitment on input 5: Evaluate f(5). | ||
|
||
!(call 0x178453ec28175e52c42a6467520df4a1322dd03e06abb3dfc829425ac590e48c 5) | ||
|
||
;; We can prove the functional-commitment opening. | ||
|
||
!(prove) | ||
|
||
;; We can inspect the input/output expressions of the proof. | ||
|
||
!(inspect "Nova_Pallas_10_02058c301605abc546248c543d450e07172690e7fb6be0fa27be6d5a898817e0") | ||
|
||
;; Or the full proof claim | ||
|
||
!(inspect-full "Nova_Pallas_10_02058c301605abc546248c543d450e07172690e7fb6be0fa27be6d5a898817e0") | ||
|
||
;; Finally, and most importantly, we can verify the proof. | ||
|
||
!(verify "Nova_Pallas_10_02058c301605abc546248c543d450e07172690e7fb6be0fa27be6d5a898817e0") |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,17 @@ | ||
123 | ||
|
||
(+ 1 1) | ||
|
||
!(def square (lambda (x) (* x x))) | ||
|
||
(square 8) | ||
|
||
!(def make-adder | ||
(lambda (n) | ||
(lambda (x) | ||
(+ x n)))) | ||
|
||
!(def five-plus | ||
(make-adder 5)) | ||
|
||
(five-plus 3) |
Oops, something went wrong.