How to update a while loop variable properly

[onyedikachi-david]

I've been trying to update a while loop variable as seen in the below but I dont know where I am getting it wrong...

 const usersPaidSet = new Set();
    const contributorsSet = new Set();

    var [usersPaid, numUsers] = [0, 0];
    invariant(usersPaid <= numUsers);
    while(true) {
        commit();
        PC.publish()
        PP.phase(Phase.Contribution())
        const start = lastConsensusTime() + 2;
        const deadline = start + duration;
        const [ timeRemaining, keepGoing ] = makeDeadline(deadline);
        const [IusersPaid, InumUsers] = 
        parallelReduce([ usersPaid, numUsers ])
          .invariant(usersPaid <= numUsers)
          .while(keepGoing())
          .api(
              C.contribute,
              (() => amt),
              ((returnFunc) => {
                contributorsSet.insert(this);
                returnFunc(null)
                // InumUsers = InumUsers +  1;
                return [IusersPaid, InumUsers + 1]
              })
          )
          .timeRemaining(timeRemaining());;
       
        commit()
        PC.publish()
        PP.phase(Phase.Payment());
        commit();
        const [[], returnPayFunc] =
        call(A.requestPayment)
            .pay(() => 0)
            .assume(() => {
                check(!usersPaidSet.member(this));
            })
            transfer(balance()).to(this)
            usersPaidSet.insert(this);
            returnPayFunc(null);

        commit();
        PC.publish();
        [usersPaid, numUsers] = [usersPaid + 1, InumUsers];
        continue;
    }
    commit();
    PC.publish()
    PP.phase(Phase.Finished());
    commit();
    exit();
})

Verifying knowledge assertions
Verifying for generic connector
  Verifying when ALL participants are honest
Verification failed:
  when ALL participants are honest
  of theorem: while invariant after loop
  at ./oops.rsh:55:5:invariant

  // Violation Witness

  const UInt.max = 2;

  const InumUsers/249 = <loop variable>;
  //    ^ could = 0
  //      from: ./oops.rsh:68:23:while
  const IusersPaid/250 = <loop variable>;
  //    ^ could = 0
  //      from: ./oops.rsh:68:23:while

  // Theorem Formalization

  const v418 = (IusersPaid/250 + 1) <= InumUsers/249;
  //    ^ would be false
  assert(v418);

  Verifying when NO participants are honest
Verification failed:
  when NO participants are honest
  of theorem: while invariant after loop
  at ./oops.rsh:55:5:invariant

  // Violation Witness

  const UInt.max = 2;

  const InumUsers/249 = <loop variable>;
  //    ^ could = 0
  //      from: ./oops.rsh:68:23:while
  const IusersPaid/250 = <loop variable>;
  //    ^ could = 0
  //      from: ./oops.rsh:68:23:while

  // Theorem Formalization

  const v512 = (IusersPaid/250 + 1) <= InumUsers/249;
  //    ^ would be false
  assert(v512)

;

[hmzdot]

Error says code can have usersPaid = 0 and InumUsers = 0 after the parallelReduce and in that case it would break the invariant of the while loop because you update the loop with [usersPaid + 1, InumUsers]

I suggest you to either make sure this scenario doesn't happen, or update you loop variables in such way

[onyedikachi-david]

Thanks for your suggestion, but I'm still tring to wrap my head around how invariants work and what variables I am to keep track along the way. An example or something greatly would help.

[hmzdot]

https://docs.reach.sh/guide/loop-invs/#guide-loop-invs This guide talks about setting invariants.

Invariants are conditions that are true before and after the loop. You generally have to define invariants for

• balances
• indices for any arrays you might have

You don't really need any other invariants but adding more is recommended so that you can make sure your loops work as expected.

It all boils down to "I wrote a program to do X, when my program does X my variables must be Y and I'll check if my variables will be Y in every condition"

[onyedikachi-david]

Thanks.