ZK HACK III - Zero to One: Developing on Aleo

Transcript

foreign cool yeah let's get started uh thanks for coming everyone my name is pranav I'm an engineer here at ilio and today I'm super excited to talk to you guys about Elio uh the Leo programming language and just you know walk through how we can build private applications on our stack let's see cool uh so Elio is an L1 with a novel architecture that really enables um private applications but also really um a unique point is that we also enable

stateful applications as well and we're in this talk we're going to figure out how Elio achieves that and we're going to start with some preliminaries so we'll do a little bit of a review of snarks um look at decentralized ledgers a little bit abstractly uh look at the account model which is uh primitive upon which or a primitive a concept on which most decentralized ledgers are built and then look at a new model called the record model um New or Old depending on your perspective but uh the record model which Elio uses to really enable these applications uh once we do all these preliminaries we'll actually write some code so we'll

look at Leo look at you know data types familiar paradigms and then introduce some advanced concepts that Leo has including uh how to program records and how to use on-chain state in conjunction with the record model and then finally we'll look at some upcoming things uh that you know that are happening in the ecosystem some new tools that we have on the horizon that'll help developers and then we'll wrap it all up with uh an announcement on zprize uh so before we get started just jumping into things um here's a link to uh some resources to get your Dev environment set up uh depending on your internet connection

this may take a little bit of time so I recommend anyone you know especially if you have a little bit of a slower internet uh hop here uh go to this link you know maybe start getting things set up while we talk about you know the high level overview I'll just leave it up for a couple more seconds for anyone who needs it and yeah let's get to it so snarks so we'll I think it goes without saying especially uh now that we're here at ZK hack is that zero knowledge proofs are a powerful tool for building secure systems typically zero knowledge proofs are privacy preserving cryptographic proofs of computational integrity and if we sort of double click into that

a zero knowledge proof is effectively some proof Pi which proves that uh given some public output y some publicly known function f that I know some output some private input X such that Y is equal to f of x so the core idea here is that with these zero knowledge proofs I can kind of prove to you that I know something without actually showing you that's something um in real in reality this is all way more complex and there's way more depth to this and I recommend checking out resources that are associated with the zero knowledge podcast ZK hack um the Whiteboard sessions uh for you know deeper introduction but we're just

going to keep things at a high level for today um so the first zero knowledge proof um uh was invented in 1989 and uh the protocol is kind of constructed at a high level as follows uh you have a proverb with uh some function f some claimed output Y and the prover has some private input X that it does not want to reveal you also have a verifier with uh the access to that same function and public knowledge of the output so the prover claims that they know uh some private input X such that the statement holds the verifier asks the prover okay prove it to me and uh the way they go about doing this is with a

sort of Challenge and response protocol um and eventually you know after a couple of rounds of this the verifier can be convinced that the prover in fact does know X now this is a remarkable achievement but there's still some problems with this construction and they're essentially kind of line of these three spaces here um first of all this protocol is interactive so it requires for the prover and verifier to be online in order for the verifier to be convinced and this is not really a desirable property in most cases in some cases at least um also this protocol isn't succinct so the the proof that the actual verif that the

prover sends isn't isn't short um which you know this is something that can be improved on and is a desire another desirable property and then finally uh the this protocol also doesn't have uh concrete efficiency it takes approver uh a long actually a very long time usually to generate uh this computation and also um requires a verifier another you know a significant amount of time to verify this as well so uh if we fast forward a couple more years uh into uh 1994 we actually get uh the first succinct non-interactive zero knowledge proof and in this protocol this makes some improvements on these uh problems that

we saw before so in the same way you have your approver and then you have your verifier except your verifier here is um much more uh much smaller in the sense it doesn't require as much compute to do verification which we have which is why we have it uh in a smaller box here um and when the prover makes the claim and the verifier asks approver uh first you know they they agree on some um uh you know they agree on some random Oracle basically some common uh transcript uh which the prover will use when they're generating the proof and the verify will be used will use when they're when they are verifying and this common transcript basically says tells

the approver that okay these are the inputs that the verifier is going to challenge me on and um tell us a verifier these are the inputs that you want to check um check on effectively and in using this construction um the prover can then just submit a short proof to the verifier and the verifier can check it quickly and this gets us the first ZK snark again this is super high level but we can kind of operate with this definition for uh most of today's talk here and just so that we all kind of have our get on the same page uh what is a z case narc uh zika snark is a zero knowledge to sing to non-interactive argument of knowledge

and essentially a ZK snark proof is um the proof is zero knowledge meaning that it doesn't reveal the witness uh the private inputs used to construct the proof the proof is succinct meaning that it's small in size and verifying it is fast the proof is not interactive like we discussed uh the prover and verifier don't need to be online and exchange messages back and forth to uh perform verification and uh the proof is sound and this is a technical requirement but at a high level it means that any statement that can be proven True by the proof system is actually in fact true so now that we have a high level idea of

zero zero knowledge privacy case snarks uh let's switch gears a bit and talk about decentralized ledgers at least abstractly so that we can kind of frame the problem that Elio tackles today so again I think it goes without saying uh decentralized ledgers uh are desirable they they enable a huge number of applications that we really uh didn't have before but uh they still run into some fundamental limitations and uh to really understand what why you know we run into these limitations uh we need to take a closer look at how these work so uh on the left here we have a we have a ledger uh with you know some accounts their Associated code and some data

and essentially decentralized ledgers ensure correctness by re-executing transactions and so what do I mean by this so essentially when a user submits a transaction with some application data some an input and a signature authenticating the transaction it's uh broadcast to the network and each node on the network re-executes this computation and if the computation is correct the nodes agree and the signature is valid the state for the application is updated now the problem is in this model is that ledger re-execution really hurts scalability so for because every node needs to re-execute on this network um this just leads to a lot of wasted

computation to do some napkin math here if you had 3000 nodes on each Style Network with five second computations a block this leads to like about 15 000 seconds or four hours of re-execution which can be avoided and because of this I think this is a familiar motivation for most of us here which is why like we uh have uh constructions like Roll-Ups so we we know that like you know we can use zero knowledge proofs in a way to achieve succinctness and this is uh sort of the primary motivation for that but on another dimension uh Ledger re-execution also hurts uh privacy because every node needs to re-execute

uh you know every transaction they need to be able to see all program State all user data um input data output data basically everything at every you know piece of State on that Network and they'll need to see this and use this till basically till the end of time so fundamentally in this construction uh you can't have privacy and uh it really breaks a lot of applications uh that you know KET allow this much leakage so clearly we do need to improve on this uh on this Construction but first uh we need to see where this problem is coming from there's a there's a sort of like higher level concept of why uh decentralized ledgers especially

organized in a certain way uh have this problem of scalability and privacy and that problem really is associated with the account model so the account model at a high level is a model for organizing uh account and application state and you know sorry I'm gonna take a pause before we go into the account model um I see I see a question on the side the first question was uh will ZK Roll-Ups need minors and really like it depends on your construction but really what you need for a roll-up like fundamentally is sort of um uh in in some constructions you'll need

something like an operator or a miner to make it happen um either that can be done sort of in a lightweight construction or you'll probably do it for a whole network but it's it's really dependent and you'll still need it um but then these things can be succinctly verified on your target chain uh the next question was well I post will we post this uh this uh session after and where I believe this will be uploaded to YouTube um I think within a day or so and then the next question is uh where would I find information about which curves are used uh with the account to generate a private key um I believe like the source of Truth is on our GitHub I think I don't know if uh

um Colin might be able to link or you know anyone here might be able to link the exact curves and their exact parameters but um yes uh hopefully that answers your question hopefully that will be answered a little bit down the line okay great um so back to the account model uh so the count models is high level way of organizing uh application user and account state and in this model you basically have a decentralized ledger here on the left that tracks each account's data um with some like global data structure some piece of global state and for each account you have its address its balance it's code and it's

storage and storage is essentially it's like you can think of as it's a persistent memory on the left here you have a user on the network and and the user's address so when a user creates a transaction the transaction itself contains the address of the account they want to interact with the value they're sending in their transaction uh the data of their transaction a fee and then a signature authenticating that transaction and when that transaction hits the network all the nodes in the network see this authenticate the signature and um execute this transaction and if the nodes agree the account state is updated so the balance of the account will be

updated and it's storage we'll be up will be updated this is a very simplified model but it still highlights what we'll what we'll get to which is the problem um with the account model and it's that well first of all uh this account is simple uh this model is simple um it's really easy to program it's really easy to use nice to work with and it's the one that we've worked with like pretty much so far especially in like um ethereum style like you know like more programmable decentralized ledgers so we do like this model but there is some problems like we've just discussed before on scalability and on privacy so

while this model is easy to work with again to reiterate um you know it's not fundamentally scalable and it's not fundamentally private so let's see what we can do to improve on this construction and see if we can gain some privacy so what we're going to do in this sort of exercise is we're going to try to attempt to extend the account model with some cryptographic you know Primitives and see if we can arrive at something like private smart contracts the idea being is that we want to hide uh smart contract data it's usage patterns while also making creating a performance system so yeah let's let's have at our first attempt so in the um in the previous section we defined a

transaction as this you know like data structure here uh we're going to make some modifications so first uh let's uh commit to the value that is being set in a transaction instead of sending it in the clear uh we're going to encrypt the data under some secret key and then instead of sending a signature we're going to send a proof and that proof is going to attest to the transactions execution the state transition performed by that transaction it's going to attest to that attest to the fact that it is that it has been performed correctly um and then on the right here where you have your original model of your account uh with its balance code and storage instead we are going to again commit to

the balance um at the bottom we're going to encrypted storage under some secret key and the key thing here is that we are going to transform the code into a representation that can be reasoned about uh in a snark in a ZK Stark this representation is what we call a predicate but you can essentially think of it as a mathematical formula that represents uh the specification of the code so now that we have all this together um let's see let's see like how it all kind of works when you when a user submits a transaction so uh you have again your now modified Global state where in your account

you're only tracking a commitment of the balance a mathematical formula or predicate representing the code and then encrypted storage and when a user submits a transaction oops uh when a user submits a transaction uh which contains its address the commitment to the value the new encrypted data the fee and the proofs the network will then just simply check the proofs and if the proofs are verified uh the account state is updated and now if we kind of rewind a bit we've mentioned how ZK snarks give us something uh give us succinctness uh which allows for fast verification and essentially what's nice here is that in

the what the main Improvement in this construction here is that instead of each node having to re-execute computation they can quickly check that it has been done correctly and hopefully this this should all still be like you know familiar mostly review if you've been keeping up with uh the previous workshops as well as uh the content on you know YouTube and so on now the so let's actually kind of double click here and and see what we're actually verifying in these proofs so what we're given is our input what we're taking as input is the code um the old state of the account so it's old balance it's all uh commitment to its old balance and it's old encrypted

State and then we want to make a new claim that the we want to make a claim that the new state is correct so like the the new state is actually in fact uh this new uh commitment to the balance and this new encrypted value encrypted values and in the proof we're first going to check that the value is conserved so you're not minting money out of thin air this would be not great to have so you're going to check that um the sum of the uh you're going to check that the sum of the commitments of the balances Are all uh equal to the the sum of the new uh commitments to the balances and then you're also going to check that the program predicate is satisfied so given the old encrypted State as public inputs uh some other you know public

data that's given in your transaction as well as some private inputs being the unencrypted state and the in the actual uh value of the accounts and the actual data that you're sending in your transaction you're going to check that the the program sort of executed correctly and when you do so um you're effectively checking that state transition now this model is actually like you know it's it's fine uh it seems pretty interesting uh what we do get here is some uh privacy in our in terms of our data so like whatever's stored in the account isn't um isn't available to see because we're encrypting them and we're not storing the balances in the clear but there's

still some problems in this model um uh the main problem one of the main problems being that there's no concurrent access to program state so in order for you to do any of these proofs to you know or any of these proofs or any of these uh predicates essentially uh consume the entire program's Old State uh before you know updating it and producing a new one which is then uh sent chain uh and um add it if it's uh if the proofs are verified the problem with this model here where you're consuming the whole state and then putting the new one and they're all encrypted is that if you have two parties trying to uh transact with the same program

but there's a sort of like a a difference in timing it could get to the point where one party uh successfully updates a program a but a second party has read Old State so whenever they try to uh actually submit their transaction and get it updated um it is invalid and therefore their transactions rejected the only way you can sort of have multi-tenancy in this model is where you uh where party a you know reads the state creates a transaction submits it to the network the network verifies it verifies the update and then and then in the second the second party can then read the new updated State

create a transaction and then update that to the network so it's a very serialized model and it's not performance and yeah this is a problem and then there's no privacy in this in this account model so so right now in in this big Ledger in this big global data structure each account even though its state itself is encrypted its data is encrypted uh it's still indexed by address so although you don't reveal the contents of your application you reveal access patterns so every time if I'm if I'm user one and I'm interacting with program a the entire network can knows that it is me that is interacting with them

with that with that program uh and so in this case yeah you do have some privacy but this isn't really the Privacy uh uh that we that we need so let's kind of review the properties of this construction so we have no more Ledger executions we're using CK snarks to succinctly verify uh that our program is run correctly we have data privacy because we're committing and encrypting um the balance and the uh data itself respectively but we don't have account privacy as we discussed because you can see uh access patterns and because a program needs to consume the old encrypted State and produce you know the new encrypted State

and then send that uh to chain basically uh you don't have efficient State updates and you don't have concurrency so can we improve upon this model to make this better right like what's what's the really core of the problem here and how can we improve it to you know get you know some more of these properties that we want and the issue is that basically in this account model every transaction needs to consume the entire program state in order to uh um yeah basically yeah it needs to consume the entire program State and then also addresses are public you still indexing the entire Ledger the entire program state by its address so

there's still just one single place you're looking at when you're actually storing and updating your program state so the idea here is that instead of like this model that we have before the key intuition is that can we Shard application State such that each user owns their own piece and if we apply this intuition we arrive at something called the record model uh before we go to the record model I see a new question um when can we start doing transfers on ilio uh so people are building wallet applications at the moment and um once there you have some a better UI for doing these um

these transfers but fundamentally they are possible on our Network um the Yeah the code is all there and it's just um yeah the really like to make this more feasible we just are looking for um we're just improving upon the user experience here uh and then just to also call out uh once we also start adding support for General uh deployment and execution of programs uh this also becomes much more smooth uh the next question is uh so what makes Elio that different than other privacy focused projects like XMR um sorry I'm not completely familiar with the core properties of that construction

so or like you know the other protocol I think um maybe someone can cover it in the chat if not feel free to ask it on our Discord or Telegram and you know we can kind of like discuss that offline uh and the final question and this is my final one before I switch the record model is does Ali offer internship programs or Junior positions for beginners who are willing to jump to full-time uh jump full time into the space and learn to contribute uh Elio is actively hiring we don't have an official internship program um and I think that's as much as I can say on that um we do have our jobs listing on our website and

um but we're also always happy to like interact with people new space and get them up to speed with our grants program and have a couple other avenues for doing so so you're not like fully out of luck um but we don't have an official internship program great uh so I'm going to keep I'm going to keep uh had a knob so the record model just to recap a bit so that we're all in the same uh page account model has some core problems no uh actual privacy because of access patterns and no concurrency no efficient State updates so we're going to solve that with this new model or old model called Rec called uh the record model and essentially in this model um the decentralized a decentralized

ledger tracks each record via Global state so instead of tracking uh accounts it's indexing that by address it tracks The Ledger tracks effectively a set of Records and let's see here so what happens is in the construction here is that you have some Global state for each program you have its program ID it's code in predicate form and then you have also a subset of records that are associated with that program in that record itself the record owner the person who owns that piece of data is encrypted the record balance the value is uh is a commitment instead of it being in the clear

and uh the record data itself is also encrypted so there's not no information being revealed here and uh the user you have a user here on the left and um and a user effectively owns certain records on the network but that's all encrypted unless a user you know queries it and um uses you know uses or spends a record so here you have um a user actually submitting a transaction and a transaction is essentially broken down into a number of transitions each of those transitions refers to a program that is being invoked

um the old records that are being consumed so the old pieces of programs state that are being consumed the new records that are produced so the new pieces of program State and then a fee and some proofs and when the proofs are checked if they are verified the network updates the set of Records associated with that program by effectively you know um you know adding in the new balance and uh updating the new encrypted data for each of those records so essentially in this model users consume and use records only associated with their context for a specific execution of the program so by starting this application State this way you can

now have multiple people uh hitting that application at once without taking it into an inconsistent state while still also maintaining privacy as well which is the core the core intuition here and then finally because the decentralized Ledger can enforce stuff like no double uh like that no record record is consumed twice uh you but you don't have double spends of application State and this is important for ensuring uh consistency of your application so what is actually checked in these proofs again just so that we you know complete this idea uh you're given you're taking in as input into this uh sort of in this proof uh proof statement that uh the old the code predicate the

old records and you're producing that you're making the claim that this uh computation is produced these new records and what you're checking is that the balances of the old records and the new records are uh the sum of the balances is conserved and then you're checking that the program predicate is satisfied for uh all input records and output records and in doing so you have this construction that uh not only has you know the the properties of the previous construction but also allows to count privacy see in this case in this case uh there's no um there's no actual like data being

revealed in the clear like even your owner whoever owns a record is encrypted so no one on the network can see record owners you have efficient State updates because we've sharded application state and then you have concurrency because different applications can um because different users can hit that application at the same time and uh without like you know going into an inconsistent State and we really get that fundamentally because we've taken stuff from an account model and sharded it into a number of Records um like an entire application state is sharded into a number of Records Each of which is owned only by the user of that application

and yeah that's that's sort of all the Primitives upon which we uh we sort of we we've constructed ilio and the fundamental thing here to to call out is that really so why do we care about accounts and Records um the reason is is the account model in you know traditional constructions and older constructions is how we manage Global State uh program state right um in ethereum all your state is on the network on on an account and that's that's used to drive the program execution in the record the record model is essentially a different way of organizing things organizing program State such that

we can we can do we can do things privately so for example like if you didn't really care too much about having um you know program State and all you want to do is just run programs and check proofs um you don't fundamentally need this record model but this record model is is key in ensuring that uh you can you can start creating applications that have some notion of state that state can live on chain it can persist and be executed over you know the course of their Ledger's execution great uh let me take a quick look at some questions here see

okay answered answered okay uh so when when would we be able to deploy a Leo program and execute it on chain uh so there we'll we'll talk a little bit about doing something like that on uh later in the workshop uh the short answer though is that we're working on it um this is the next Milestone that our team is uh going to be tackling in the in the phase of our test net so more to come soon um but this is the next sort of big thing uh that uh we're excited to update people on when we get there um just a quick thing for the question though is can you brief us uh us about nodes if you could just shoot a reply you know elaborate on your question uh that would be great

uh difference between a Leo and ZK sync um I think I'll leave that to the chat to actually you know correctly answer I don't want to speak out a turn and misrepresent the properties of uh of of ZK sync um the exact difference between provers miners prover and miners validators from stakers um this this is essentially so uh the short answer is that provers effectively run programs uh validators uh produce blocks and stakers um stake on the network uh there's much more information about this in detail I think in our blog posts and there might

be a couple more resources out there but for this talk um uh we're not going to you know dive into that and then uh the next question oh sorry there's another one is that the record model similar to the utxo model it is similar that's sort of the key intuition um you can essentially take the utxo model and kind of extend it into the record model um see anymore okay cool uh what happens so the next question was what happens when an application needs to perform some actions for the user since the user is only one in control of

keys so I think if I'm understanding your question correctly and you're asking that how does an application sort of you know execute on the behalf of a user um I think the if I'm understanding your question correctly uh we'll get to this later in the workshop but we can also augment the um the record model with some notion of the account model so some notion of global State and uh re-execution by the network to get a hybrid model where you do all your stuff in private that you want to do with records and then whatever you need um an application to perform some actions on behalf of a user you kind of switch over into uh the account model

ish or into some Global Ledger re-execution and then do some stuff there more to come later in the workshop it's a pretty cool construction um and yeah let's see uh so the next question I see is yeah I'll leave this rest I'll leave this up for the rest of the chat and um we'll just keep on we'll keep heading on so now that we have a idea of all these like high level Concepts and you've got some intuitions for things uh let's look at how what Leo is and how we can use it to actually develop private applications so this is the uh this will be the coding component of the workshop um

for those of you who haven't gotten a chance to install uh and set up uh both the Leo um the the Leo CLI the ALU SDK and optionally uh some vs code plugins please go to this link and um you know follow the instructions there's a specific setup instruction which um you know essentially pulls a script and runs it and will do all of your setup for you if you opt to manually build and uh and do things you might find that you'll have to like install some stuff when you first run a Leo program don't worry we'll give some time for that as well but I'm just going to pause for maybe like two minutes uh let two three

minutes let people you know set things up and then we'll keep going and then in the meantime I'll answer questions okay great so um next question so is running a client node equivalent to running a full node on another blockchain like Bitcoin another word what is uh so let me answer that first piece of the question um sometimes to run a client you may need to like you can opt to run a full node like with any other construction if you don't want to do something as heavyweight there are um we are exploring some ideas for like clients uh those just more to come later

uh yeah it's it's more of a it's not it's we just kind of need to design that construction uh there I think the question though what that question is getting at though because each client needs to manage its records um it might require more work than a light client in other contexts and it makes the makes the light client look a little bit more like a full node but this can be done quite easily um not quite easily but at least like your initial scan of Records is probably the most computentially intensive task you'll ever do as a client but after that all you're doing is just you know getting records that are relevant to you so that's pretty easy it's pretty

lightweight and doesn't require that much compute so that was the first part of the question there second uh question part is what's the difference between a client note and approver so a client node can be approver um but we also have a scheme where a client node can delegate proving to another node with more computational resources and then that node can execute for you or create the proof for you and submit that to the network so for example if you're like on like a lightweight mobile device you can delegate to approver it'll get the job done send it to the network and do it on your behalf um and then yeah the second part of that question was I uh or second comment

there was I understand the prover is kind of like a minor with coinbase rewards as incentive and yeah that's effectively true so right now in our test net approvers are essentially grinding um certain puzzles for uh coinbase rewards but uh the distribution scheme is more unique and I think interesting I'll leave that for um to look at you know at some resources on the on the alien blog um one quick thing before I answer one more question is um is the noise in the background still a problem um feel free to chime in if or received okay great okay I see no it works

can't hear anything okay great awesome uh the final question is uh that we'll do before I move on is how could I do data analysis if all the data were encrypted um so this is where you could actually uh construct some cool construct some cool schemes um first of all one thing that I I'm pretty excited about if you know people can kind of make this happen is you really can do enforce a data Marketplace by like first you know by first principles because every user sort of owns their own records right like a user can decrypt all of their records but no one else can see them users can

um submit their data on a data Marketplace for um uh you know for for you know just for people to buy and use and you can probably construct some cool schemes out of that um that will require probably a little bit more cryptography you have to use to sort of allow like um I guess like tiered record decryption but um I I'll kind of like leave that for uh leave that as an exercise um but yeah you're right that you won't be able to do just data analysis um just outright just by looking at the chain and I think this is an important thing to have um it's actually a feature not a bug because really like uh the whole if the whole core idea is privacy

um this is sort of like fundamentally at odds with it um cool and I will leave the rest of the questions for um to be answered in you know in in the threat in their threats so I'm assuming everyone's gotten some time to set things up let me see if I can get rid of this I cannot cool cool um yeah okay we'll just we'll just keep moving on let's see all right so now that we have some intuition for the record model uh let's take a look at Leo and see how we can use it to develop private applications so Leo is a high level programming

language that is compiled into alien instructions which is more of like an assembly language which is then serialized into AVM byte code which is the actual you know format in which uh programs live on chain and is actual format you know it's it's used on the network um the compiled bytecode is the effectively the format that's uh that's deployed on chain and then is visible to all participants on the network and then finally the Elio virtual machine or the AVM is a virtual machine which will like read AVM bytecode and execute it and produce uh a proof so in this Workshop though we're only going to focus on Leo code

um there are a bunch of additional resources on uh Elio instructions in the AVM in our developer docs and you can get to our developer developer Docs via the bitly link but it's also developer.alio.org and there's a ton more resources out there and it's a pretty cool construction definitely encourage people to to check that out so with that uh Let's do let's get started with Leo Let's uh let's create our first Leo program and um yeah and then we'll kind of go through the the parts of a Leo program so for those of you that are following along um like you know open up a terminal window open up vs code um and you know type in the following

command so we're going to create a directory called projects we're going to CD into the directory uh invoke the command Leo new hello world CD into that and then we're gonna call Leo build and then Leah run Maine with these inputs and you can just use them directly as is so I'll give people uh two minutes to do something with that and then I'm going to walk through it uh with you guys and show you uh uh parts of this stuff on my on my machine cool um let's see answered answered okay great I think most of the questions are taken care of for the person who asked

about nodes a little bit a while ago if you can add some more clarifying information in your in your um thread that would be great we can get to that question uh once you do great I'll give people just another 30 seconds foreign we have another question does Elio Pro uh support private State consensus on layer one how efficient is it in terms of transactions per second slash speed um

so I guess to maybe unpack your question a bit more did the question sort of disappear uh uh let me just answer it out right like if we're talking about just how does the network uh like arrive at consensus and how does it relate to State well because all your state is private by records your consensus your networks don't need to re-execute they're just checking proofs overstate transitions those proofs um are zero knowledge so they don't reveal any information about um your application State and in doing so is um you know preserves privacy so during consensus you just check proofs

effectively maybe that answers your question if not feel free to ask another uh ask another one um oh I see it again um how efficient in terms of transactions per second um I don't have the current numbers right now uh I think maybe someone might be able to post it up but um yeah that that that's off the top of my head uh and then the final question is what programming language does Elio use the programming language is called Leo and that's what we're doing right now so um yeah if you get a chance to install Leo uh we can walk through the demos all together so let me let me do just that um we're gonna do we're gonna create a Leo

program and go through uh you know the parts of Leah program so I have the directory called projects I'm gonna do Leo new hello world and we're going to CD into this uh uh cool so this is sort of the structure of a Leo project you have a readme um the first important piece is you have this thing called the program.json and this is like your config file for your program um here the two main important pieces I want to call out is uh you have uh some development accounts and essentially you have a private key and you have an address associated with each account

um whatever you execute uh Leo programs in this directory it's going to use these private keys and addresses and now you can always swap these out with new values and you can do that using the alio CLI so if you look at the terminal here you can do Elio account new and that generates a new private key A View key and address and you can swap these out and effectively execute transactions under different identities um the next main important thing is you have your Source directory with your main.leo um here is the hello worldly program so you have a programmed scope the scope which defines the body of a program and you have the program's identifier

this identifier is uh will correspond to a unique identifier for the program on chain so it's um it's it's a unique identifier such that any other you know developer or any other application will be able to find a program by its program ID then you have a transition called Main and a transition essentially forms a public interface about of a of a of your program more on transitions later there's actually some deeper Concepts here but for the purpose of this intro like this is fine so your transition is called main it takes a public input which is a u32 takes an uh another input B which is u32 and in Leo inputs are private by default

if you don't put a public visibility on it uh it is assumed to be private and then uh it produces a u32 as an output so because there's no again no modifier here this is going to be a private output then on line four you have a declaration of a variable C A type declaration and because Leo is strictly typed we we currently require all variables to be uh to be typed explicitly typed we are working on type inference so more com more to come later but on line four we add the we take the sum of A and B and then return C um one question I think seems relevant

to answer right now um I think it came up I saw it a little bit earlier is our input files being deprecated uh this is a great question uh we've been going through some back and forth on design here so for the purpose of this Workshop we don't need to touch inputs um everything that we we will run can be done by the can be done by the command line so you're all good to go there um so more to come on inputs you can track it like uh on the Leo GitHub repository but we don't need that for today and then you have a directory called build um let's actually build the program so we'll do we'll call wheelbill and that's going to populate the build directory uh it's gonna go do some stuff

uh invoke the AVM and build the program and in the program you'll have like your main Alia files this is like Elio instructions and you have the associated program.json um uh that's essentially a clone of the one that you saw before so this is the high level overview of the high level anatomy of a of a Leo project we're not going to go too much into alien instructions today but um you know you can always find some more information there but just so that we're all on the same page here you can run Leo run main one you uh to either one u32 to u32 and

um you can build and run this program okay cool great um awesome so with that uh let's actually go and do a deeper dive the Leo language um before we do that I see that uh okay we got some answered questions here uh one question is there a difference in computation costs between a public and private input all else being equal um yes there is because in your snark you're going to have to encrypt uh that value uh you said input but you're gonna have to decrypt that input um same thing for outputs

uh great so let's talk data types uh we're gonna just do a quick like flying tour of Leo and um hopefully build a some an interesting program and but we'll first get started with primitive types here uh Leo has some primitive types uh integers uh booleans uh that are probably familiar to most of you um uh it also has uh some algebraic data types fields scalers and groups and these data types relate to like the underlying uh snark construction and also relate to some of the underlying cryptographic Primitives that we have available also to be used in Leo so like for example in Leo you can um uh hash commit do all that stuff and these are data types sort of related to

that um you also have some specialized data types address you should be fairly intuitive it's uh relates to addresses on the network so Leo also has um custom data types user-defined data types that you can declare in a program the two user-defined data types are structs and records for now we're only going to look at struts records actually have some deeper underlying meanings so we'll take we'll talk with them later so structs are probably declared in a in a sort of familiar syntax if you're coming from yeah C ish uh maybe rust um you declare struct its name uh a timestamp or you know a member variable

in this case a timestamp and then you declare its type now member variables can either be primitive data types or they can also be other structs themselves so fairly uh natural interface here so now let's actually start looking at some programs uh actually we have we have a cool question here um uh why do we call Leo a language and not a rust DSL so I wouldn't call it a rust DSL you're probably right in calling it a rust-like DSL uh rust-like domain-specific language um and maybe you can call it a rest DSL because it is implemented in Rust but it's it's more rust-like it's not exactly rust-like

um uh because there are certain Concepts in Rust that you that um are as natural to express in circuit-based languages so um for that it's where you know I think I think for the purposes of answering your question language and DSL can almost be used interchangeably um great so let's uh let's look at uh a Leo program here um here's a program it's called hello.aleo and uh the first thing to call out is we see a function and a transition now in Leo especially a function is a piece of code that takes some values as input

and produces some values as output and it can be called by other transitions but transitions actually are something special here and they're really to do with our programming model um a transition is a function that can interact with on-chain objects so it can uh consume and produce records which are then uh posted up to the chain uh it can also interact with on-chain State uh which we'll get to later in the workshop but there's some cool stuff that you can do in transitions that you can't do in uh in functions and really transitions are a new paradigm that are needed to power uh stateful applications on on ilio so next up we have

um we see like we addressed before we have a variable declaration uh it has to be statically typed um here we have a subtraction operation and one thing I'd like to call out here is that all default integer arithmetic on uh in Leo is uh checks for overflow so the way we've implemented under the hood is that if you just use the you know straightforward like standard operations uh your overflow checks are built in and it's built to be safe if you'd like to use wrapping operations which can be sometimes more efficient but also unsafe you can explicitly declare them and use them in or not explicitly declare them you can explicitly use them in Leo but you can

find more resources on that in our developer dots um so transitions also have this notion of visibility so functions just taking inputs produce outputs but transitions themselves actually uh you know will be will be the public interface of your programmer and will form the actual um predicate that you define so here you're also for transitions you can define public and private uh inputs um and public and private outputs now there's also conditional uh statements conditional structures in Leo so you have conditional statements here uh one thing about Leo is that you can also return early from conditional

statements so um if you're kind of going through a branch you can exit the branch and exit the program early and this is just there to kind of provide a familiar um familiar ergonomic interface you also have for Loops for Loops here need to have their Loop variable statically uh typed so you do need to declare the the type of the loop variable and uh the loop Expressions must be um must be uh integer literals for now and we're working on extending support there but here um you know you they must be explicitly declared integer literals and the reason why is that when the compiler takes this high level Leo program and turns it into

um a circuit it needs to all the computation needs to be sort of statically defined and unrolled into a sequence of computations or a circuit basically a circuit always has a fixed size so for that like Loop literals need to be um statically need to be stat um static integer literals but they can also be constant Expressions uh more to come on that later uh Leo also has some search statements that uh can be used to check um check certain values certain properties when we're producing proofs and if any of these assertions are triggered uh the execution halts and the uh the AVM the alio virtual machine

fails to create a proof uh they should just just feel feel familiar to asserts in um other languages uh something like self.collar this is a special uh sort of thing we have where you can get the address of the uh person or the entity uh invoking this transition or trans or invoking this transition and it lets you you know do some create some checks it's it can be useful and we'll see that later great so we're gonna get into our first uh sort of programming challenge uh coding challenge uh we're gonna budget some time for this and

essentially the coding challenge is this um we're going to compute interest it's going to be simple but just give you enough to see like you know just get comfortable with writing Leo um so we create a new first like the first challenge here is to create a new project titled interest we saw a couple steps ago how to create a new project via the Leo new command second part of the challenge is in that uh new program that new scaffolded structure that you've defined um I you will replace the main transition with a new transition called calculate calculate will take in a private variable principle and a public

variable rate and then calculates the resulting balance after compounding interest for exactly 10 periods and assume that rate will be a u32 um and you know just for Simplicity we can assume principle to also be a u32 so I'll give everyone some time to like you know work on that feel free to ask some questions um I'm going to go through answer a couple more and we also have some test cases for you to just you know check send you check your implementation uh the funny thing here is that you're doing integer division uh which will have some you know weird Corner cases and won't get like the decimal values that you might

be expecting so feel free to check your work with some test cases foreign great um just going through the list here um so first one is there a way to view the 35 constraints generated for hello.aleo one thing I'd like to maybe just call out about constraints in general um so maybe first I'll answer your question directly there is no way to do it like with a tool at the moment we are working on we have a tool internally that we use and we're going to work on you know we are open to releasing it once um we've uh you know once we kind of get into shape uh for that so that's

to directly answer your question um and then another thing just to kind of like just if they're out there for constraints in general um every proving system sort of has their own stuff with constraints um at least with ours you should um constraints it is a useful metric to use when you're trying to optimize your own program locally so like if you've made you know your MVP one of a Leo program it's producing some number of constraints well a great way to see that you've actually made an improvement is try another implementation and see if you have fewer constraints um more about like comparing constraints across languages is very I'd say uh it's sort of a poor metric of

comparison I think you find that like um numbers are represented differently and there's certain like internals to like making um stuff work with uh program State like so work with the record model that requires a certain overhead with constraints so just for what it's worth just throwing that out there um just to help you use constraints as a useful way of optimizing your programs um it looks like most of the questions have been answered I'm just going to take a chat yeah it looks like a thank you Haruka actually for for mentioning this it

looks like the IntelliJ plugin might not be updated to support the latest grammar um yeah I I think I I see that return Then finalize might not be there um yeah thank you for calling that out actually we'll uh we will uh push out an update for that um seems straightforward to do yeah I'm going to give people like another two three minutes and then Twist of time um instead of the full 10. um if you do need more time just though just drop it in the chat um it'll at least let me know [Music]

foreign [Music] cool I think we'll in interest time we'll we'll keep we'll keep pushing forward so here's our solution um just to go over pretty quickly it's a transition called calculate takes into principle it takes in a rate as specified we declare a variable called the mount for the principle and then simply just construct a for Loop um be sure to do the multiplication

first and then the division and then return the value um this should be fairly straightforward um but let's sort of extend that a bit um one thing that kind of sucks about this design is that you can only do for 10 iterations and that seems very restricted and um not useful so uh the next extension on this challenge is okay can we vary the number of periods over which we Inc accrue interest so here's the challenge uh modify calculate so that it takes an additional private parameter called periods check that periods doesn't exceed exceed 50 and then calculate um in the interest for those number of

periods so one thing that just a hint for people is that we have asserts which are great for checking um and yeah this one I'll give a couple minutes just for people to play with and then here's some test cases um for these test cases I guess it's worth mentioning the first element is a principle the second element is the rate um and then the third element is the number of periods that rate because we're sort of assuming like a division by hundred and it'll change if you depending on your like division Factor but if you're doing like divide by a hundred it's five percent thank you

why this should be straightforward as well no tricks in this um but just want to get people familiar with the language so we'll give it another 30 seconds uh given that there's no questions in the chat so uh there's a question out there

um oh I see okay it looks like our ID plugin might be having some issues so first question was uh why does my vs code theme when I open a Leo file that's the plugin that we have um it kind of does the same like uh color scheme as um as Leah like you know that we have for our for our language so I believe you could be able to change that in your uh plug-in settings I'm not sure that I've never tried it um so that answered the first one uh the second one uh Loop bound must be okay so first one um unknown function assert if it's

coming in the IDE this is where I mentioned the ID plugin might be broke might be out of date um it uh if you go through and run Leo build and you're using the most recent version of Leo uh you should be able to um it should be able to run no problem uh assert like uh like let me let me go maybe I'll leave this up here but uh assert and then just a predicate is supported uh I see another one Loop bound must be a literal so if you have your Loop bound as an expression of something um it won't work and the reason why is

especially if that if that expression is an input your um it's not statically defined right so like if you uh decide to pass some five or ten you'll be doing a different number of loop iterations so for that um you need to do it you need to do a different sort of trick to get around it and the maybe the hint I'll give is maybe Define a bounded number of iterations can you define an upper bound and then go from there and I guess since there's some questions and stuff I think we can give some more time but one thing I'll call out here is that with circuit languages in general

this is uh this is an interesting like sort of like programming Paradigm that people like you'd need to adopt um because your computation needs to be fully sort of specified and needs to be sort of fixed size in in some in some sense um you need to sometimes employ like a clever trick or something to uh get around uh you know variable inputs that might change the size of your program so I'll give it another 30 seconds cool uh we'll keep moving on

so here we have a solution here's our solution um just just to call out the different points here is that we've added in a third parameter called periods and then we assert the first line is we check that periods is less than or equal to 50. and the main modification here is that we just add a condition inside of our Loop that returns if um the number of periods uh is equal to 50 or uh sorry if the if the loop counter is equal to the number of periods are greater it's greater than or equal to the number of periods and um yeah that's sort of The Simple Solution here uh the main idea we want to call out though is like for Loops at least right like we need to still

sort of create an upper bound on the number of iterations that we can do and then inside the body of the loop or inside the program logic we can encode uh ways to get the results for the variable amount that we wanted and this is sort of like the high level concept that we want to the high level takeaway that we want to uh point out for this uh for this exercise here all right um let's go on and now let's uh let's actually start doing some cool stuff so we talked a lot about records uh how why you need records and like you know like how they support private applications so we're gonna get to actually program with them and uh play around with them for a bit so first uh let's kind of walk

through how we can actually use records and you know declare and use records so here we have a record declaration and you'll see that it's very similar to the Declaration of a of a struct but um records have two required Fields uh the owner and Gates owner is the the address that owns that record and it's the address to which that record is encrypted encrypted to when it's on chain so only that address whatever you produce a record and it's put to chain or whatever you um if you're trying to or if you're trying to consume a record only if you own the private key corresponding to that address can you decrypt and use that record and it's really important for you know getting

this privacy property that we care about and then we have gates gates is a denomination of eliocredits um which is the native uh Native unit of currency on the network effectively um Gates is effectively to it so Gates is to alio credits as G way is to eat as senses to dollars is the analogy there and great so with records we can essentially use them to encode application State uh because we have this sort of owners field and because of the way the protocol Works users exclusively own their own records and Records like we've discussed before enable concurrency in

privacy so let's see how this works we'll walk through a couple examples and then build an application that uses records on our own uh one thing to call out here though is um so records you can Define also user data so here on the left you see uh we have a uh we have some struct called payload which is structs as we discussed earlier and we have a record here on the right state which takes in the field uh which is also which is in itself is struck called payload and Records can take multiple number of data fields uh you can this one only has one but then you can you know if someone wanted to they can Define another data field under it Foo that takes in a u8 and so on and so

on um we do have some static bounds uh right now while we're kind of going through early phases of testnet figuring out what programs can be deployed you know ironing out the The Kinks but um there's a static bound um it's I believe it's 32 if you're interested but um if if it does start to hinder your application we'd love for you to file a file a an issue and it'll let us know that like you know people are hitting into this limit and we are open extending it cool so this is how you declare records it should just be fairly the tldr is ADD owners and Gates and it's like structs so how did records work on ilio so we

talked about transitions transitions are the the public interface of your contract transitions are the pieces of code that can interact with on-chain objects so transition can take in some number of records and produce some number of Records so let's see how this works how you can do this with an actual program and with you know every project right uh we'll talk about tokens and how do we instantiate a token on a Leo using records uh this token will be private by default so like essentially you can think of uh a short blurb here is how do you instantiate uh zcash um within

um with an alien with an alien program something zcash like um before I go into this example I'll take a pause I see some questions uh there are use cases for having a record within a record this uh sort of unexplored territory um see records are explicitly on chain objects right or obviously live on chain um if you're if you'd like to store the data of another record in a record you can totally do that by like pulling it out of one and putting it in another but right now because like we're kind of like thinking conceptually thinking of them as like blobs or encrypted blobs on chain

it's a question of what does it mean for a record to be in a record is it a reference to another record and then a question we'd have to kind of ponder is what's what's the use case so really the the the short answer there is uh we don't know um and we we're curious to find out if you have some thoughts on this we'd love the feedback because it'll really help improve and to think about what an alternate construction looks like uh is the code from this session shared in the GitHub repo or anywhere else uh in Elio HQ which is our main GitHub repo um there's a workshop repo for it um I'll let uh I think maybe someone link it up in the chat but

uh yeah uh final question before we go on is does Leo provide some sort of random number generator or a suggested approach there's nothing right now for an RNG uh natively right now so um but there's something that uh we're interested in so if you if you have a proposal or you'd like to see this please feel free to file an issue or file a proposal and you know get it'll help us track track this issue all right so on to records um so we have some record uh token here and uh token will have an owner and Gates as required and then Define a balance

token will also have a function called transfer so transfer what it's going to do is take in a token record as input an address that you want to send to and an amount and then you're going to on start starting on line two compute the difference the amount that you're going to send and the amount left over you're going to create a new record called remaining with the difference the stuff that's left over and one thing to call out here is because Leo is um has safe math by default checks for overflow uh the the chat we don't need to check for overflow explicitly online too and then on line eight we create the token that we're going to send to the other party and that will be encrypted

under their address which is the receiver and then send those tokens out um you know return them and how does it look like with some like on-chain interaction um let's see oh yeah just to call out that's how you that's how you instantiate a record in uh in code so let's say you have some Ledger with some record n on it the owner of that record is Alice and only Alice can see that record it's encrypted to her address so if Alice wants to send some number of tokens to Bob let's say she wants to send it by a transfer she puts in his input her record and she can do so because she can decrypt her record um she puts in Bob's address and the amount of tokens she wants to send

the transition transfer will produce a new record Being the remaining amount for Alice and um the uh the amount for Bob that's record number two notice that record number N1 is new let's it's a new record it doesn't use the same one record n and you know both these records are encrypted under their owner's address the transition transfer also creates a proof that the network can check to make sure that this transition is valid and if the network checks and the proof goes through uh these uh Records are appended to The Ledger now one thing to call out here is that we see that record n is grayed out and this is something fundamental about

the record model when you use a record inside a transition it's used and cannot be used again this is where the Ledger prevents double spending if you did allow this you actually get into some pretty interesting attacks I think it's uh pretty uh straightforward to also construct one so essentially what you're doing here is that um yeah so you can um when you spend that record it's sort of it still stays on chain this chain keeps track of it but it tracksuit with a serial number that tells you that that record's been spent and cannot be used anymore uh one question I see is uh for records are you only able to encrypt with your private key or can you choose to encrypt with other owners public key so that

they can only just decrypt it and that's exactly what we did in this in this uh program uh uh transfer right so like essentially in this transition transfer this is something that Alice is going to call but she's going to provide Bob's address as input right so she essentially that that in line eight when you create that token transferred you're creating a new record that is encrypted to Bob's address now Alice because she called this function she knows how much she sent to Bob there's no way to get around that but um Bob like when when this record's put on chain only Bob will be able to decrypt it and if Bob does like has been like scanning the chain for records that are now created to him he'll sort of like be

notified when uh this record's included cool sweet so that's how records work uh and now we're going to do uh another programming challenge here um for purposes of time I'm going to maybe keep this one pretty short um so try to follow along if you can but there is our Workshop repo which we'll we'll do this exact example so if it's a little too fast don't worry you can go back um and do it yourself and then as always if you have any questions please feel free to like hop on our telegram or Discord and we're always there happy to answer so here what we're going to do is

Implement a private auction using Leo and in our design the where we care about privacy is that we don't want bidders to learn any information about each other but we're okay with the auctioneer the person running uh um transactions or sorry running the auction uh to see that information and we're assuming that the auctioneer in the in the sense is uh semi-on or isn't it's just trusted the auctioneer isn't colluding with any players it's not revealing some information on the side so uh that's just how our trust model is going to work for simplicity's purpose someplace simplicity's sake um and yeah um let's kind of walk through this model like how we want this

to work effectively um so the first step we want to create some sort of transition Place bid which Alice can invoke and it creates a new record which is encrypted to the auctioneer's address and that contains some information about Alice's bid then we want Bob to be able to call that same function place a bid which also creates a new record that's encrypted to the auctioneer's address foreign once the auctioneer decides to like finalize the whole thing or you know like start resolving the auction they can take in the two records that are created from Alice and Bob top and bottom respectively and push it through a transition called resolve resolve will select the winning bid the bid with the

greatest amount and produce a new record which is essentially the same it's just the new record is whichever record was the max bid so it's going to still keep the owner as the auctioneer gonna keep the same amount of gates going to keep the same metadata associated with that record but it's just going to select the the maximum one or and in the sense selection actually produces a new record but that's just a technical detail underneath then the auctioneer is going to finalize the winning bid or finish the auction and what they do in in this transition finish is it takes in the the winning record and

um outputs a new record which contains the same payload as the old record but encrypts the new one under the Winner's address and in doing so that winner now owns this record that they can show and attest to that they are in fact the winner and uh then can use it you know maybe when they're resolving the auction on the side or you know out of bed so let's see how that works um so let's kind of go through the challenge we're going to go through this a little quickly so uh don't worry if it's a little too fast to follow for now so um we're going to create a new project auction we're going to define a record called bid which has a following user-defined Fields bitter amount and is

winner and yeah I think I'll give just a little bit here let's see if there's any outstanding questions but foreign we don't have any functionality baked in the core for now we're interested in doing something like this so feel free to file an issue or if you have some proposals uh we're willing to kind of work and workshop that uh and make that part of our language um uh are the source code of transitions

necessarily public so if you use the protocol as is uh you publish a program and everyone else can use it and you know do and so in in doing so you do make your source code public um this is because like in the start construction your predicate is also public but what you can do and this is something we're also interested in doing is um eventually like if you want to keep your source code private and just check proofs on chain um that's a totally feasible and reasonable thing to do uh how can the function transform or change manipulate Bob's record since it has not been decrypted with his private key

does this means you can only send a uh tokens to an address so like uh the function transform I think you're maybe referring the function transfer so the function transfer is not manipulating anything to do with Bob's records it's just producing a record to Bob um it doesn't take in any of Bob's old records so because it's doing so it's just kind of like it doesn't need Bob's key to like run effectively um next question is there an is there a way for an Auctioneer to commit to its program or give the participants any guarantee yes it totally can when

the auctioneer publishes their program on chain there that is effectively the source code of the program that's run so whether you're doing Place bid that's the the program that you will be running and then finally perhaps a naive question in this setup the auctioneer can see all the bids and um agree yeah this is correct uh to find the winning uh yeah the auctioneer can see all the bids is there a mechanism to minimize the number of bids that the auctioneer uh can see but still find the winning bid uh just wondering how much privacy it can be in the situation so let me think here um so one interesting way you could probably extend this scheme to increase privacy is maybe construct like an MPC

uh or just add some notion of multi-party computation to it so instead of like giving the auctioneer all the responsibility to resolve and do things uh you just have um uh you can sort of do the compute together and hide some information from the auctioneer um I'm going to kind of leave it at that high level uh because FPC constructions are really bespoke um so yeah uh we'll we'll keep it at that I think great um awesome I'm Gonna Keep moving and actually I'm gonna sort of jump ahead because we'll be coming up on time zoom and we want to make sure we have time for everything else

um so here you know we Define a record um the main things to call out here is that there's a bidder there's an amount and there's a winner all of which are primitive data types so the next thing we're going to do is create a transition called Place bid which takes in the bidder that is the bitter and the amount bid it checks that um checks that the caller is the address of the bidder and then constructs a new bid which is uh owned by the auctioneer and the specifications here I'll post all these slides up but for the purposes of this Workshop or just for the interest of time I'm just going to push through show the solution and we'll talk about some more stuff uh some more interesting stuff so here's a function Place bit line two we do an insertion check and simply just

construct a new record on line three um that the next part challenge the next function that we're going to Define is a function transition resolve the one that the auctioneer is going to call to resolve the bids this will take us input two bids and then check that the invoker of this function is only the auctioneer and select it selects a bid with the highest amount so this is actually very straightforward to do in Leo um you just have a check on line two it's an assertion check checking that the auctioneer's address the the caller's address is as follows which is auctioneers and then you know just as does a simple conditional statement and Returns the the greater bid and then finally finishing the auction

so we're gonna Define a transition called finish which is going to take a bit as input and then just produce a new record that has the same payload that's encrypted to the new owner and the way it does that is you know same thing line two there's a check and line four um there's uh the results of the bid so with that um I'm going to see if we can quickly run through some uh One More Concept which is on chain state which is a new exciting thing that we have on ilio where we combine some of these Notions with the account model with the record model to get like this hybrid model where you can do all your private stuff

in private land in record land and use on chain State when it's needed and it's useful uh and on-chain state and sort of like Ledger re-execution can be useful in certain situations where you want the network to be executing on your behalf and um you know maybe for certain applications like escrow this is very naturally motivated so Leo has this thing called mappings and for those coming from solidity uh this should be a very familiar interface mappings are essentially on chain uh pieces of State uh that you know a map from a key to a value uh should be very straightforward if especially if you just look if you are referring from you

know solidity the evm and whatnot um so with mappings we can do something like a transfer of a token but maybe we can start with a token that's in a record an amount and a record and transfer it publicly so I have a private token that I don't want anyone to know how much balance it has but I want to publicly send some coins to someone other party and I don't care if people know how much I send to that other party by the end of the day they don't know how many tokens I have in total and we can do this with by combining the record model and mappings here we've defined an augmented version of our transition transfer where instead of receiver and

amount being private they're actually public values so everyone's going to know who I'm sending it to how much I'm sending line two we calculated the difference is as we've done before but then the the important thing to call out is line eight um we first so in line three we create a new record with the remaining balance send it to ourselves and then in line eight we return that record but then invoke a finalized block which is what you see with the syntax then finalize with the arguments receiver and amount a finalized block is essentially a piece of code that defines that tells the network what to do when execute when you when executing this transaction on chain

so once you do the off chain component get a proof submit the transaction the network checks the proof and then executes the finalized block and we'll go through an example of this how it does this but what we're doing here is then in lines 10 to 12 we're incrementing an on-chain mapping called balances with the receiver's address and the amount that we sent them so in this way the whole network knows uh what the uh what that new person has and is able to see that that that you know the receiver got some money and we'll kind of walk through this in a quick flow so here we have a network there's some validators checking the network and you have a ledger which contains a record with Alice's balance and you also

have an on-chain mapping this is public State uh with keys corresponding to the addresses both Alice and Bob's and the values that they have so step one Alice will query the network for her encrypted record so she's going to get a record pull it you know pull it from the network it'll still be encrypted she will then uh decrypt her record and execute the transition transfer locally so she's going to put in Bob's address the amount she wants to send these will be public and then the transition transfer the one that we just discussed the modified one will produce a new record containing Alice's remaining balance a proof that you see at the bottom proof pi and then also send um

like also produce or just you know pass through the public inputs that to the finalized Block in this case Bob's address and um the amount she wants to send this all will get packaged into a transaction that you see here uh the transaction will contain the record it'll be encrypted under Alice's address the proof the proof is the proof is also included but the Bob and the address are um are set in the clear so what the network does is it checks the proof and then if the proof verifies uh then or so if the proof doesn't verify network doesn't do anything no state is

updated uh just dump right dump the transaction um if the proof does verify though the network can add the record to The Ledger you know say that the old record was spent and also update Bob's balance up here in the corner um with its uh with the new value and so the network executes the finalized block and stores the new record and this is essentially a powerful model which really um sort of like allows you to as a developer choose how much privacy you want in your application so it's really like a nice fine sliding scale that you can use and Define what you need privately but then use public stuff when it's useful and

necessary um and this can be a powerful primitive we're really excited to see what people can do with them I will give one big like asterisk mappings are an extremely experimental feature there's a lot of improvements that we as a team are really focused on doing uh but more to come over the next couple months so um we have a little bit more time to touch on a couple things um first we'll talk about some tools that are available in the Leo ecosystem that can help you run check your programs just you know improve the developer experience and then uh we'll finally wrap things up with an announcement on zprize so first deploying applications uh

what's the state of it right now so right now you we're working on adding support to test net three to like actually send your transactions uh actually deploy your programs execute them on the network but in the meantime we have a little uh little tool it's an experimental Tool uh called slingshot which you can through which you can create a node and a local development node and run it and you know uh you know play around like deploy execute your programs I see there are a couple questions I'm going to pause here for a second and just answer some things um let's see uh do mappings conflict with

concurrency properties yes they do so like if because you have to do things so you don't conflict with concurrency properties but they're subject to the same concurrency and consistency properties as ethereum state effectively so the order that is determined by you know the block is sort of the order in which uh finalized blocks are executed if you don't design your data structures in an item coded way or um maybe design them as operational transforms um you'll have a problem with on-chain consistency and then is there a way to achieve in the finalized action uh yes so this is uh what this question is asking is can

you do General loads or stores in finalize State and finalize blocks so right now it is not possible but this is the improvements to the mappings that we're really actively working on so um with so more to come stay tuned but uh yeah we're really excited to see what we can do there and um we'll we'll post an update to the community when that's ready um so in this presentation just switching things back I wanted to show a demo a slingshot we're a little bit tight on time but you can go to this GitHub repo uh where you can look at the slingshot tool um and after this workshop I'll post some better instructions and some resources in running this tool and kind

of using it locally if for those that are interested we're going to skip ahead and uh talk a little bit about formal verification which is an exciting like component that we're adding in to our an exciting direction that we're exploring and to do that I will have um Alessandro another one of our Engineers come up and present on it yeah hello so okay I'm going to tell you very briefly about the work we're doing

informal verification applying it to the area blockchain video programming language Etc so um first of all the motivation for this is that the zero knowledge proof that we've been talking about uh concerns the com that the fact that the computation was performed correctly so but what is the computation described as it's described as a zero knowledge circuit it's essentially an arithmetic circuit where gates are algebraic operations and so on and so forth you can read all about that in the literature but the point is that that that's what the zero knowledge proof refers to you know however

the user does not write directly does your knowledge circuit the user writes some Leo code and according to our tool chain the real code gets compiled to any structures which are these Intermediate Language that we use also to store problems on chain and then in instructions are compared to the zero knowledge circuit so there are two major steps and within each of these steps there are a lot of sub steps as is typically in compilers you know you first pass the code you try track it you do some Transformations optimizations and so on so you can imagine each of these two arrows really consisting of a lot of smaller arrows or sequence together um

so how do we know whether the the zero knowledge circuit is computationally equivalent to the Leo cone so how do we know whether it was combined correctly so that's a general concern obviously you know you always want your compiler to be correct but for this particular application area the point is that if the compression is not correct then the zero knowledge proof does not necessarily apply to the to the audio code it still applies to the zero knowledge circuit but that may differ from the computation as intended by the user who writes Leo code and so in order to address this problem we we use formal verification so what that is is that we

were building tours to generate theorems mathematical theorems that assert the correctness of the combination process since there are these two major computational steps we generate one theorem for each of them those are fairly independent but of course they get combined together to give an end-to-end assertion and of correctness and to do that obviously we we need a former semantics of all the these languages and formalisms involved so we are developing a formal semantics of the Leo programming language from a semantics of alien structures from a semantics of zero knowledge circuits those that

actually we already have and we are using and so we when we generate this this theorems and then we have them checked mechanically by a theorem prover so we don't do that by hand we don't just write them in password and paper we use tools to do that specifically we use the acl2 tour improver which is one of a hands full of the main general purpose theorem provers in the world it's uh used its industrial strength it's used a lot in Hardware verification in commercial companies also increasingly in software verification and and so we are building the theorems that are expressed in the

language and logic of the acl2 theorem prover and what wants to generate the theorem so we ask the theorem prover to check that the theorem is correct of course we need to spell out the proof in sufficient detail so that the the the theorem prover can check it and when I say proof I don't mean zero knowledge proof I mean a proof or mathematical theorem so it's at a different level here so this is very much work in progress we have already some of the pieces done and working right now we are focusing mainly on the verification of the zero knowledge gadgets which are essentially components that get composed together to generate several knowledge

circuit uh for for for given Leo products we also have other parts done and in process in the front end for both Leo code and instructions so yeah we will publish more updates on these uh as soon as we have them available we're actively working on that having said that our astronauts to come back [Music] great and with that um just a quick blurb on our project and how to get involved so Elio is proudly written in Rust uh we're open source on GitHub

uh we have our Workshop you know repo with all these code examples posted up here and uh we have different ways which through which we engage with our community Twitter Discord we also have a telegram um uh that's not here but uh we can put that up somewhere uh for you guys to get access um we'd love for people to contribute to our projects so whether that means uh filing issues filing bugs uh writing their own features those are all welcome if you'd like to contribute in a more formal way um we have a grants program where we'll work with workshop and come up with the grants proposal uh or you could come up with a grant proposal and we'll fund it and um you know have a more collaborative uh

engagement we're also hiring um so feel free to go to Elio uh and we have our jobs postings on there [Music]