Despite updating loop variable and map in the same manner, Reach tells me that they could be different.

[rithik-raja]

I have a parallelReduce that keeps track of 2 sums—a sum of even numbers evenSum, and a sum of odd numbers oddSum.
At the end of the loop, I update the variables in a return statement by adding a fixed increment. Whenever either evenSum or oddSum is updated, an element of a corresponding Map, either addressEvens or addressOdds, is updated with the same increment.
Obviously, evenSum should be equal to the sum of addressEvens and oddSum the sum of addressOdds, but Reach tells me this is not the case.

  const addressOdds = new Map(Address, UInt)
  const decimalFactor = 1000000

  const [howMany, sumOfHowMany, evenSum, oddSum, deadlineBlock, keepGoing] = parallelReduce([0, 0, 0, 0, thisConsensusTime() + deadlineTime, true])
    .invariant(
      balance() == 0 && 
      balance(tok) == sumOfHowMany * decimalFactor &&
      sumOfHowMany == howMany * (howMany + 1) / 2 &&
      sumOfHowMany == evenSum + oddSum &&
      evenSum == howMany / 2 * (howMany / 2 + 1) &&
      oddSum == ((howMany + 1) / 2) * ((howMany + 1) / 2) &&
      oddSum == addressOdds.sum() &&
      evenSum == addressEvens.sum()
    )
    .while(keepGoing)
    .paySpec([tok])
    .api(Player.buyTickets,
      () => {},
      () => [0, [(howMany + 1) * decimalFactor, tok]],
      (k) => {
        k(null)
        const increment = howMany + 1
        if (increment % 2 == 0) {
          addressEvens[this] = fromSome(addressEvens[this], 0) + increment
          return [increment, sumOfHowMany + increment, evenSum + increment, oddSum, thisConsensusTime() + deadlineTime, true]
        } else {
          addressOdds[this] = fromSome(addressOdds[this], 0) + increment
          return [increment, sumOfHowMany + increment, evenSum, oddSum + increment, thisConsensusTime() + deadlineTime, true]
        }
      }
    )
    .timeout(absoluteTime(deadlineBlock), () => {
      const [[], k__] = call(DeployerAPI.setClaimMode)
      .check(() => {check(this == Deployer)})
      k__(null)
      return [howMany, sumOfHowMany, evenSum, oddSum, deadlineBlock, false]
    })

The last 2 lines of the invariant always fail with values that make no sense to me. I have no problem with the other lines of the invariant. Here are some examples:

const evenSum/330 = <loop variable>;
  //    ^ could = 0
  //      from: ./index.rsh:38:92:while
  const oddSum/333 = <loop variable>;
  //    ^ could = 1
  //      from: ./index.rsh:38:92:while
  const v798 = <function return>;
  //    ^ could = true
  //      from: ./index.rsh:47:50:?:
  const v803 = <map reduction>;
  //    ^ could = 0
  //      from: reach standard library:147:18:application
  const v812 = <map reduction>;
  //    ^ could = 0
  //      from: reach standard library:147:18:application

And

const evenSum/330 = <loop variable>;
  //    ^ could = 6
  //      from: ./index.rsh:38:92:while
  const howMany/331 = <loop variable>;
  //    ^ could = 4
  //      from: ./index.rsh:38:92:while
  const oddSum/333 = <loop variable>;
  //    ^ could = 4
  //      from: ./index.rsh:38:92:while
  const v698 = <function return>;
  //    ^ could = true
  //      from: ./index.rsh:47:50:?:
  const v703 = <map reduction>;
  //    ^ could = 9
  //      from: reach standard library:147:18:application
  const v712 = <map reduction>;
  //    ^ could = 8
  //      from: reach standard library:147:18:application

I could really use some help :'(

[jeapostrophe]

I do not know why the theorem prover is failing, but your invariant is actually false.

You are not guaranteeing (via a check) that addressEvens[this] is not already set. Imagine that evenSum is 10 and addressEvens[jay] is 2, then I send another message, you will update evenSum to something like 22 and addressEvens[jay] to 12, but now the sum of the even addresses is 20, not 22.

BTW, I recommend using the .invariant form multiple times, it will give you cleaner error messages.

[rithik-raja]

Actually, I want it to be such that a single person can participate multiple times.
Also, the invariant should be true even in your example. If evenSum is updated, that value is added to the existing value in the map. So evenSum would be 22 and addressEvens[jay] would be 2+12 which is 14, not 12.
Do you have any idea what's going on? (please help this is driving me insane)

[jeapostrophe]

Ah, I see.

Those <map reduction>s are the results of calling x.sum().

thinking aloud The invariant runs AFTER the loop body, so howMany has already been updated. I wonder if your uses of howMany + 1 in it should really be howMany?

[rithik-raja]

I wonder if your uses of howMany + 1 in it should really be howMany?

What exactly do you mean by this? Each use of howMany + 1 is called each time a person calls the API. So howMany is equal to the number of people who joined (not unique people). Also, evenSum and oddSum are directly related to howMany and should be equal to the respective map reductions.

The invariant runs AFTER the loop body

Does this mean that the invariant is checked, and THEN the loop variables are updated? Which means there's a mismatch between the loop variables and the map reductions?

What I should do? Please tell me what's on your mind.

[jeapostrophe]

Invariants are used in three ways --- https://docs.reach.sh/guide/loop-invs/#guide-loop-invs ---

1. They must be proven true with the initial values of the loop variables
2. If we assume that they are true before the loop body starts, then the loop body must preserve their truth
3. They are assumed to be true after the loop ends

I was referring to how I don't understand

      evenSum == howMany / 2 * (howMany / 2 + 1) &&
      oddSum == ((howMany + 1) / 2) * ((howMany + 1) / 2) &&

given

      sumOfHowMany == howMany * (howMany + 1) / 2 &&
      sumOfHowMany == evenSum + oddSum &&

I think that

• If howMany is even then howMany = 2n, then
• evenSum is \Sigma_{i=0}^{n} 2i = n * (n + 1) (similar to what you have without the even-ness test)
• oddSum is \Sigma_{i=0}^{n-1} 2i+1 = n^2 (not what you have)
• If howMany is odd then howMany = 2n + 1, then
• evenSum is the same and presumably howMany / 2 rounds down to n
• oddSum is \Sigma_{i=0}^{n} 2i+1 = (n+1)^2 (not what you have)

Maybe I'm wrong

[rithik-raja]

The three points you mentioned about the invariants should be true for me.

1. The sum starts as 0 and the map starts as empty
2. The sum is only incremented when the map is incremented by the same value
3. The sums should be equal to the respective map reductions even after the loop

Also, the oddSum formula is correct, and I haven't had any trouble with the loop variables. Plug in 1, 3, and 5 into the formula and we get 1, 4, and 9, which are the expected values.

Once again, this brings us back to the problem of the map reduces behaving unexpectedly.