Constraints in SnarkyJS built in methods

[unborn meadow]

I'm looking at this bit of code in here. https://docs.minaprotocol.com/zkapps/snarkyjs/smart-contracts

class HelloWorld extends SmartContract {
  @state(Field) x = State<Field>();

  @method increment() {
    // read state
    const x = this.x.get();
    this.x.assertEquals(x);

    // write state
    this.x.set(x.add(1));
  }
}

so in here x is fetched on the client side. x is sent as public input to a Mina node. there's a constraint that checks whether public input x equals to onchain x.
so someone can't modify snarkyJS and fake the x.

My question is this.
this.x.set(x.add(1));
Does this line generate a proof that says , onchain x is indeed set to the public input x + 1?
Or should I add another constraint after the state update?

[ripe salmon]

Calling of increment will create a proof thats tied to a single account update (in this case).

This account update contains the following information:

• preconditions, created using this.x.assertEquals(x), which tells the L1 protocol that your proof is valid, given that the current on-chain state at the time when the account update is applied, is x. This is imporant because your proof is valid given the data it was computed with, so the chain needs to check if the data is still the same as when you computed your proof.
• state (updates), created using this.x.set(...), telling the L1 protocol that the result of your computation is an account update that wants to set the state x for your account. The L1 protocol doesnt know where does the new x value come from, all of that is abstracted away by your proof - which is computed on the client side

[unborn meadow]

so as I understand someone running this code on client side can modify snarkyJS and change the last line's effect to sth like this.x.set(100 or this.x.set(x.add(5).
And to prevent that there should be sth like this after the update? this.x.assertEquals(x+1);

[ripe salmon]

if you change the code of your smart contract, you change the circuit use to compute the proof that authorizes the account update, therefore the L1 protocol wont accept that proof anymore, since it wont be valid under the rules (verification key) that was deployed as your smart contract

[unborn meadow]

maybe not change the code directly llike this.x.set(100). but modifying SnarkyJS.
In docs it says, if not for the precondition in above code, " a malicious user could modify SnarkyJS and make it just use any other value than the current on-chain state – breaking our zkApp."
So my concern is just like that what prevents someone from setting the this.x to sth else other than current x + 1.

[ripe salmon]

the proof itself, if you modify the contract code, or snarkyjs, you wont be able to create a valid proof for your smart contract anymore

proof is a proof of computation, if the computation changes, you proof & verification key changes as well

[unborn meadow]

if that's the case why is this precondition/assertion needed?

    const x = this.x.get();
    this.x.assertEquals(x);

if modifying the initial smart contract code or snarky js messes up the proof, there's no need to add this check. right?

as i said above I'm confused because docs says if not for this line someone could modify snarkyJS and mess up with the value of x.
sorry if i'm mistaken somehow.

[ripe salmon]

preconditions, created using this.x.assertEquals(x), which tells the L1 protocol that your proof is valid, given that the current on-chain state at the time when the account update is applied, is x. This is imporant because your proof is valid given the data it was computed with, so the chain needs to check if the data is still the same as when you computed your proof.

^^ i've explained this in the original response, the L1 protocol needs additional verification for your proof. Since there could have been multiple transactions in the same block, and while the proofs will still be valid, the preconditions won't be after the first transaction has been included. (if both TX have the same preconditions)

[unborn meadow]

ok I understand this precondition causes a tx revert if there are multiple txs that trying to update this.x.
but what about this part?

[ripe salmon]

thats the same concept in different words, still describing preconditions

[unborn meadow]

this is bit confusing.
in here it says the precondition is added in order to prevent a malicious user modifying snarkyJS. As I understand that statement means if there's no precondition , and if someone has modified snarkyJS, the proof won't fail.
you said if someone modified snarkyJS the proof will fail.

[ripe salmon]

Sorry for the mix up, i was talking about the precondition itself being part of the proof. Therefore it means noone can remove the precondition which anchors the proof to the on-chain state.

Another thing is that if you dont use the precondition, then you can't trust the values used to compute the proof, because you dont know how the client provided the values. This is what docs mean by modifying snarkyjs, but its a bit more complex than that.

[unborn meadow]

aa ok. so should there be a precondition/assertion at the end of the function to check if the state is incremented correctly?
I mean if this precondition ( this.x.assertEquals(x);wasn't part of the proof someone can use a different value for x.
just like that can someone set this.x to some other value?

[ripe salmon]

no, the value you set to x is computed in the proof itself, the proof proofs that you increment some input by some value, and then you have that in a variable and you set it as a new state

the proof is the glue in between the input (existing on chain state) and the output (state you want to set)

you proof the computation 🙂

[unborn meadow]

aa ok I see, every computation that been done via a snarkyJS built in method get included in the proof.

Thanks @ripe salmon