Account / network precondition RFC

[mitschabaude]

Precondition RFC

If users want to add preconditions on the account or protocol state, these will most often relate to the current on-chain state of these fields. A very intuitive model is to let users just "use" the current state -- for example, let them access the "current account balance". The mental model is that this balance is a variable (not a constant!) that depends on the current chain. It can be implemented by fetching the current balance from the chain, using it in the prover as the value for the variable, and adding a precondition which fixes the balance to exactly this value. If we wouldn't add the precondition, then the balance would be unconstrained, which would be against the intuition that we prove a computation which uses the current balance as input.

Therefore, I think a good default is to just let users access the balance (and other fields) as the property of some object, and behind the scenes add the necessary precondition. We propose the following API to achieve that:

// inside method
let balance = this.currentAccount.balance; // automagically adds a precondition
balance.assertLte(100e9); // this method can only be called if current balance <= 100 MINA

Note that to use this API intuitively, one doesn't need to understand the concept of a precondition at all. It's enough to be aware of the this.currentAccount property. The returned balance is a plain UInt64 variable; the added precondition stays completely hidden. Similarly, we propose to have a this.currentProtocolState property which exposes protocol state preconditions. On other parties, we would have corresponding party.currentX properties.

However, advanced users may want to declare arbitrary preconditions. For example, in the above example, it makes sense to actually not use the current balance, but just to add a precondition directly. We propose the following API:

Party.assertBetween(this.accountPrecondition.balance, 0, 100e9);

This works for any party, not just the this party. It mutates this.accountPrecondition.balance, which is the precondition (represented as an object {lower: UInt64, upper: UInt64}.

The last example achieves the same as the first one -- it constrains the balance to be less than 100 MINA -- but without the fragility that the current balance needs to stay unchanged until the transaction is accepted. However, to use an API like this, you do have to understand the concept of a precondition. That's why it's OK to use more jargon ("precondition"), and make this a bit less discoverable (have to use Party), and let it not do any magic. Similar to this.accountPrecondition, we propose to expose this.protocolStatePrecondition, which would just be shortcuts to access party.body.accountPrecondition and party.body.protocolStatePrecondition.

In addition to Party.assertBetween, there is also Party.assertEquals (already implemented), and we could likewise add Party.assertBelow and Party.assertAbove.

Finally, you may want to reference the current state when declaring an arbitrary precondition. For example, possibly you want to restrict the nonce to an interval of the form [currentNonce, currentNonce + tolerance]. Or you may want to restrict it to be exactly currentNonce + 2, because you already know that there'll be 2 earlier transactions which increment the same nonce. For this final use case, we propose the following API:

Party.assertEquals(this.accountPrecondition.nonce, this.currentAccount.nonce.add(2));

This is the precisely same API as before, just making use of this.currentAccount. The logic would be that any explicitly set precondition would override any magically inserted precondition. So, in this case, nonce == currentNonce would be overriden to nonce == currentNonce + 2.

TODO list

• Implement the this.current* API and, for other parties, party.current*.
• Implement this.*Precondition and party.*Precondition.
• Implement Party.assertBetween, Party.assertEquals
• Fetch all account preconditions from chain
• Fetch all protocol state preconditions from chain
• Create unit-tests which confirm that
  • setting/fetching all preconditions is possible
  • set preconditions show up in the JSON transaction

[jasongitmail]

Thanks Gregor.

1. On the naming:

this.accountPrecondition
this.protocolStatePrecondition

Given they're both state, how about this?

this.accountPrecondition
this.protocolPrecondition

And we landed on network precondition during the earlier naming project, so maybe this?:

this.accountPrecondition
this.networkPrecondition

2. The logic would be that any explicitly set precondition would override any magically inserted precondition. This makes sense, to allow overriding the magic if it exists. +1

3. Party.assertBetween(this.accountPrecondition.balance, 0, 100e9); This feels unusual to me.

Alternatively for naming, would it be possible to do something like this.preconditions.account.balance.assertBetween(0, 100e9) b/c it provides hierarchy in the naming or this.accountPrecondition.balance.assertBetween(0, 100e9)?

Preference for the first one b/c, although it feels long, it provides hierarchy and intellisense code suggestions would guide them to know what options are available at each depth of the hierarchy as they type out this.preconditions.account.balance.

[mitschabaude]

Thanks for the feedback @jasongitmail!

My argument for accountPrecondition and protocolStatePrecondition is that these are the same names used in the OCaml code, the graphql API, the JSON structure, the written spec here, and probably a number of other places. I feel that naming consistency is more important than choosing the "ideal" names (which is rather subjective). For example, a user exploring the graphql API at https://proxy.berkeley.minaexplorer.com/graphql should find the exact same field names as a user autocompleting the JS type. If protocolStatePrecondition in one place is suddenly called networkPrecondition in another place, it's confusing.

Currently, this consistency is achieved by autogenerating the TS types from OCaml code. Here is the autogenerated Party type: https://github.com/o1-labs/snarkyjs/blob/cba3f5b5e4ac6f1fdca894d97ceb11d15e875608/src/snarky/gen/parties.ts#L356
Any special cases would require overriding this and make the implementation dirtier, which is another reason for me to not want it.

That doesn't mean that we can never add any shortcuts / alternate ways to access things in snarkyjs. But I'm against naming tweaks like preconditions.account or protocolPrecondition that break consistency without meaningfully adding to the API.

[bkase]

This is great!

I agree with both @mitschabaude and @jasongitmail . Specifically, we should use the a preconditions namespace with account and network subfields and change the json, graphql, the spec, and the ocaml structure to match it! While choosing names is subjective, I think there are good arguments for using the precondition namespace and referring to the protocol ones as network (I’ll happily enumerate them if necessary). This was an oversight when reviewing the transaction structure 😓 and highlights why it’s good to be doing these sorts of tasks before the hardfork and these structures can no longer change (so we can keep the consistency).

I can try and knock out these name changes today so it hopefully won’t slow any work down.

[bkase]

Additionally, I think we need to be careful with the automatic constraint; for example, this one is would make contract interaction trivially Denial-of-service-able via MEV (front-run the transaction by sending dust to the account). A safer constraint to insert would be a >= on the balance (then only an owner of the account can break the contract). However, inserting this constraint may be unintuitive. Off the top of my head, I don’t have a great suggestion for what to do here, but I’ll think more about it today.

[mitschabaude]

Nice @bkase, yeah I'm perfectly fine with name changes when they happen across the project! 👌🏻

Regarding the other discussion -- should we have this.accountPrecondition.balance.assertBetween(0, 100e9)? This feels much better to me bc the name is consistent, there is just a method assertBetween that's added to the original (autogenerated) type.

Personally, I'm a huge fan of separating data and functions and using plain JS objects for data.. so that an accountPrecondition would just always be a plain object conforming to the autogenerated type:
https://github.com/o1-labs/snarkyjs/blob/cba3f5b5e4ac6f1fdca894d97ceb11d15e875608/src/snarky/gen/parties.ts#L486

The benefit IMHO is that this makes creating these objects much nicer:

let balance = { lower: UInt64.from(0), upper: UInt64.from(100e9) };
let accountPrecondition: AccountPrecondition = {
  balance,
  nonce,
  receiptChainHash, // we have autocomplete for the property names!
  delegate,  // order of properties doesn't matter!
  state,
  sequenceState,
  provedState
};

Typescript feedback is wonderful when passing objects like these around.

If, on the other hand, accountPrecondition and balance have to be a custom classes with some methods on it, we are faced with less purity / more boilerplate when creating them, and it gets more error-prone, and all the classes have to be imported:

let balance = new Interval(UInt64.from(0), UInt64.from(100e9)); // have to import `Interval`to do this :(
let accountPrecondition = new AccountPrecondition(  // have to import `AccountPrecondition` to do this :(
  balance,
  nonce, // no nice autocomplete for the names here :(
  delegate, // wait.. which came first again? delegate or receiptChainHash? :(
  receiptChainHash, 
  state,
  sequenceState,
  provedState
);

Ok, so that's my argument for the Party.assertBetween thing, but I know that just having to type . to find methods is a very nice thing about classes :D So I'm open to the discussion here!

[bkase]

Finally, I think even advanced APIs should be discoverable via intellisense . I agree with you that it’s not ideal from a code organizational standpoint, but it’s one of those things where we should always to optimize for dev usability.

In this case, discoverability trumps the new boilerplate imo. But the constructor should definitely take a JavaScript object as a parameter so we get autocompletion of fields (and anytime a constructor or any function takes more than a handful of arguments this is a good practice)

[mrmr1993]

Generally I'm in favour of the original proposal, with the proposed tweaks. One note:

Or you may want to restrict it to be exactly currentNonce + 2, because you already know that there'll be 2 earlier transactions which increment the same nonce. For this final use case, we propose the following API:

Ideally we should be tracking the new state of the accounts part-way through transactions, so that updates from prior parties will be successful. I would expect that we should construct e.g.

before: app_state[0] = 4
construct party 1: {precondition: {app_state: [new Field(4)]}, update: {app_state: [new Field(5)]}}
construct party 2: {precondition: {app_state: [new Field(5)]}, update: {app_state: [new Field(6)]}}

if both party 1 and party 2 were to call this.currentAccount.app_state = this.currentAccount.app_state.add(1)

[mitschabaude]

Agreed @mrmr1993, we should do that! It's tracked here: #114
I think it's just going to be part of a later PR, to keep scope small

[mrmr1993]

I guess one other thing worth calling out: it would be nice if balance was 'special', so that it only gets constrained if you care about its actual value or some concrete bounds. For example,

let balance = this.currentAccount.balance; /* has type WeakBalance */;
let balance_value = balance.value(); /* has type Balance, adds equality precondition */
balance.assertLt(foo); /* adds/refines upper bound */
balance.assertGt(bat); /* adds/refines lower bound */
this.currentAccount.balance = this.currentAccount.balance.add(1); /* doesn't add precondition, only sets delta */

(assuming this is practical to implement). This removes a potential foot-gun where users are likely to add preconditions where none were necessary or intended.

Bonus points if anything that would accept a Balance also accepts and detects a WeakBalance, calling value() to get the actual Balance, but I'm not familiar enough with the API to know how feasible this is.

[mitschabaude]

That's very interesting @mrmr1993! I guess this is only possible for balance, right - because that's the only field where we send the delta in the transaction and not the full new value? I agree it would be cool, but it's a bit involved and the impact not huge because it's only for balance -- so I'll save it for later as an enhancement: #205

I do think all of what you wrote is feasible

[45930]

Note that to use this API intuitively, one doesn't need to understand the concept of a precondition at all

The last example achieves the same as the first one -- it constrains the balance to be less than 100 MINA -- but without the fragility that the current balance needs to stay unchanged until the transaction is accepted

This sounds like giving the developer a false sense of security. An invisible precondition that will cause a transaction to fail if balance has changed (or network block height, epoch, account nonce, etc..) when all the developer means to have asserted is that the balance was less than 100 is way more confusing imo than figuring out that you need to call assertBetween. Being aware of this.currentAccount and Field.assertLte sounds very similar to being aware of this.accountPrecondition.balance and Party.assertBetween. I'll grant that the words "precondition" and "party" hit a little different. I think I'm something like the type of dev you're targeting with this, and for me, I find 2 different ways to do the same thing, one objectively worse but "easier", to be more confusing than one proper way to do it, well-documented.

Finally, you may want to reference the current state when declaring an arbitrary precondition.

This is more compelling to me. The ergonomics of making a trade at the current price +- slippage, or submitting a transaction only valid in the current epoch are way nicer than getting explicit user input.

[mitschabaude]

@qcomps That's an interesting take. But maybe the example was not ideal to make the case for an invisible precondition (I chose it to make the case for also having explicit preconditions).

Let's imagine that we would expose the current balance, but not add a precondition automatically, so we would just give the user an unconstrained variable which happens to have the correct value in it. This feels like a footgun as well - how many users would understand that this variable can be anything and still make the proof succeed?

If users don't do the right thing to add a precondition themselves, their smart contract could become open to attack. To me this seems worse than having a few transactions fail.

So, to me the only alternative to having an easy way to access current state, and adding strict preconditions by default, is to make a less ergonomic API that makes it very obvious that you get something that's unconstrained.

An example for such a less ergonomic API that actually already exists would be the following: we just have a method fetchAccount(publicKey), which returns an account, which has a balance on it that is a constant UInt64. Then, we could have documentation that shows that you can do this fetch outside the method and pass the balance to the method as a parameter. Here, it would be very clear for everyone that anything can be passed in! And then the example could go on to show how to explicitly add a precondition.

Would you prefer this latter way of doing it?

[jasongitmail]

Great discsussion!

I find 2 different ways to do the same thing, one objectively worse but "easier", to be more confusing than one proper way to do it, well-documented.

This is more compelling to me. The ergonomics of making a trade at the current price +- slippage, or submitting a transaction only valid in the current epoch are way nicer than getting explicit user input.

@qcomps +1 from a dev experience perspective

If users don't do the right thing to add a precondition themselves, their smart contract could become open to attack. To me this seems worse than having a few transactions fail.

@mitschabaude Also really important.

Let's keep discussing this. Maybe the compromise position to use the magic precondition only for asserting an exact balance, to prevent any foot guns and default to safety. Then others are manual and we document this as an exception. Are there any other footguns where a default precondition could be useful for safety @mitschabaude ?

[45930]

Let's imagine that we would expose the current balance, but not add a precondition automatically, so we would just give the user an unconstrained variable which happens to have the correct value in it. This feels like a footgun as well - how many users would understand that this variable can be anything and still make the proof succeed?

I definitely agree that malicious behavior succeeding is worse than unintentionally wrong behavior failing. What is an example of worst case though? If I write const balance = this.account.balance; transfer(balance, caller), I pretty clearly want to transfer my whole balance. Would your example balance.assertLte(100e9)successfully (and wrongly) prove that 200e9 is less than 100e9 without setting the precondition? Or is the issue that you can prove it, and then at verification time it might not be true, but it will still pass?

Regardless, the same people who would shoot themselves in the foot with this will also not read through this thread and will just see transactions failing. If possible it would be preferable to fail this before deploy. Maybe allowUnconstrainedValues: false could be a config value in the deploy pipeline or something like that (not mutually exclusive of this proposal).

we just have a method fetchAccount(publicKey), which returns an account, which has a balance on it... you can do this fetch outside the method and pass the balance to the method as a parameter.

Would this actually constrain account balance or just some input UInt that ought to be account balance? I definitely prefer being able to "use" account.balance... I guess the main thing I'd prefer is to fail a lot earlier if used improperly, rather than secretly adding something the dev didn't write.

[mitschabaude]

Would this actually constrain account balance or just some input UInt that ought to be account balance?

It wouldn't constrain the account balance. It's the behavior you were arguing for, that we shouldn't constrain the balance automatically, it just makes it more obvious that it's not doing so.

Would your example balance.assertLte(100e9)successfully (and wrongly) prove that 200e9 is less than 100e9 without setting the precondition?

The issue is that balance would not be not linked to the actual balance. You could set it to 0 by changing one line of code. Then you would successfully prove that 0 is lower than 100e9, while the account balance could still happily be 200e9.

If I write const balance = this.account.balance; transfer(balance, caller), I pretty clearly want to transfer my whole balance.

Ok, say you write

const tenPercentOfMyBalance = this.account.balance.div(10);
transfer(tenPercentOfMyBalance, caller);

Then you clearly want to transfer 10% of your balance. However, if this.account.balance can be anything, a malicious actor could set it to 10x your balance, and successfully pull out all your money.

IMO, if we give users a field that says "this.account.balance", we owe them that it's actually constrained to their balance.

By the way, just to make this explicit, balance is just an example in this whole thread. The same discussion applies to other account fields like state, nonce, sequenceState, provedState etc, and protocol state fields like blockchainLength, timestamp, totalCurrency etc.

We already have a magical API for on-chain state. We allow users to write

let x = this.x.get();
this.x.set(x.add(1));

This should mean the following: It sets your new state to +1 the old state. If x can be anything, it would allow users to set the new state to anything. The snark would be worthless. We have to fix x to the current state, IMO -- or force users to explicitly add a precondition for x themselves.

I definitely prefer being able to "use" account.balance... I guess the main thing I'd prefer is to fail a lot earlier if used improperly, rather than secretly adding something the dev didn't write.

This is great feedback - errors instead of magic. I've been thinking about a new proposal which moves in that direction. Will write more soon

[mitschabaude]

Precondition RFC, version 2

In light of the discussion so far, I propose an alternate API, which forces users to add preconditions themselves instead of doing it secretly. The new proposal also does away with magic property access which secretly runs logic, and instead strives to be boring and explicit, while being also fairly simple and discoverable.

We consolidate account / network preconditions under a single field, this.account and this.network. Using account / network fields looks like this:

let myBalance = this.account.balance.get();
// should be equal to my actual balance
this.account.balance.assertEquals(myBalance);
// ... doing arbitrary computations with the balance

let chainLength = this.network.blockchainLength.get();
// should be not more than the current length + 5
this.network.blockchainLength.assertBetween(chainLength, chainLength.add(5));

this.account.balance.get() does the following: It fetches the balance from chain and creates a variable with that value in it. It does NOT link it to the current balance in the snark circuit. Instead, explicit assertEquals or assertBetween is necessary to create that link.

To make this not a footgun, we throw an error if the user doesn't add any explicit precondition on the field. The error is thrown when compiling, proving, or running the smart contract method in any other way. Example:

@method payout(caller: PublicKey) {
  let balance = this.account.balance.get();
  this.transfer(balance.div(10), caller); // tentative API to send money from the zkapp account
}
// ...

MyContract.compile(zkappAddress); // throws an error!

Running this would throw:

Error: You used `this.account.balance.get()` without adding a precondition that links it to the actual balance.
Consider adding this line to your code:
this.account.balance.assertEquals(this.account.balance.get());
You can also add more flexible preconditions with `this.account.balance.assertBetween`.
    at /home/gregor/my-zkapp/node_modules/snarkyjs/dist/server/index.js:5039:145
    ...

The developer would hopefully read the error message and modify their code like this .. which would fix the error, and teach them about preconditions at the same time.

@method payout(caller: PublicKey) {
  let balance = this.account.balance.get();
  this.account.balance.assertEquals(balance);
  this.transfer(balance.div(10), caller); // tentative API to send money from the zkapp account
}

Closing thoughts

Doing away with the magic property access on account.balance, and using explicit account.balance.get() instead, enables us to add even more methods to the same property. Thus, we can have the preconditions like assertEquals() right next to get(). I find this somewhat preferable than to have an additional this.preconditions.account + the magic accessors on this.account.

Note that I also changed this.currentAccount to this.account, which for me also makes more sense than before, if everything is consolidated on this one field.

I think now that @mrmr1993's concern, about not constraining the balance when it doesn't have to be, is sufficiently addressed by having very visible methods like transfer or send / receive, which you would typically just use by putting in some amount that doesn't refer to the current balance. Only in cases like above (where delta is really computed from the current balance) would you even stumble over the error and use a precondition. To make it harder to hit those cases, we probably should NOT have a balance.set() method, just balance.addInPlace() and balance.subInPlace() which we already have.

[45930]

As for me, I quite like version 2!

[jasongitmail]

Love it. Intuitive API, errors catch footguns, and no unexpected magic. This is great.

Note that I also changed this.currentAccount to this.account,

+1

[bkase]

This is great, I love this!

[imeckler]

This is nice -- thanks for writing this up Gregor!