reach-sh / reach-lang

Reach: The Safest and Smartest DApp Programming Language
https://www.reach.sh
Apache License 2.0
584 stars 167 forks source link

Updating an Address array causes compile error #325

Closed AmbroseHill closed 2 years ago

AmbroseHill commented 2 years ago
'reach 0.1';
'use strict';

// Interact Definitions
const UserInteract = {
  ...hasConsoleLogger,
}

export const main = Reach.App(() => {
  // Participant Interfaces
  const User = Participant('User', {
    ...UserInteract
  });

  // Deploy the contract
  deploy();

  User.publish();
  commit();

  const mAddress = Maybe(Address);
  const x = Array.replicate(100,mAddress.None());
  User.only(() => {
    interact.log(x);
    const newX = x.set(0,this);
    interact.log(newX);
  });

  exit();
});

The above code gives the following output when trying to run or compile:

Verifying knowledge assertions
Verifying for generic connector
  Verifying when ALL participants are honest
reachc: The compiler has encountered an internal error:

  Unexpected result from the SMT solver:
  Expected: success
  Result: (error "line 1308 column 525: Sort mismatch at argument #1 for function (declare-fun T1_cons (T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 T2 ) (Array Int T2 ) ) supplied sort is Address" )

This error indicates a problem with the Reach compiler, not your program. Please report this error, along with the pertinent program, to the Reach team as soon as possible so we can fix it.

Open an issue at: https://github.com/reach-sh/reach-lang/issues

CallStack (from HasCallStack):
  error, called at src/Reach/Util.hs:75:3 in reach-0.1.4-2ZKi32JNzIACxBH7cb1Ora:Reach.Util
  impossible, called at src/Reach/Verify/SMT.hs:598:9 in reach-0.1.4-2ZKi32JNzIACxBH7cb1Ora:Reach.Verify.SMT
AmbroseHill commented 2 years ago

Commenting out the lines below fixes the compilation.

    const newX = x.set(0,this);
    interact.log(newX);
jeapostrophe commented 2 years ago

I'm going to pushing a fix shortly, but in this case, the "problem" is that Reach isn't catching an error in your program and it is getting through to a later stage and you get a weird error.

This line const newX = x.set(0,this); is wrong, because x is an array of Maybe(Address) but this is an Address, so it can't be assigned there. You want x.set(0, mAddress.Some(this))