Enforcing linearity for state transitions and field accesses

Although this wiki entry discusses state transitions, and this entry does as well, the issue addressed here is largely orthogonal to that previous entry, and thus should be separated.

This entry instead addresses the problem of enforcing linearity after state transitions, and also the general problem of how a programmer can access owned/linear fields of a contract. A naive way to imagine state transitions is as follows: a state transition is a statement like any other, and the programmer simply specifies the intended post-transition state, as well as any fields that this state needs that aren't in the current state. For example:

contract MoneyHolder {
  state HasMoney {
    Money m;
    transaction removeMoney() ensures NoMoney {
      ->NoMoney;
    }
  }

  state NoMoney {
    transaction addMoney(Money mNew) ensures HasMoney {
      ->HasMoney(m = mNew);
    }
  }
}

Unfortunately, this doesn't correctly enforce linearity. Indeed, in the above example, the field m is lost forever when the removeMoney transaction is invoked. To make matters worse, there's no immediately obvious mechanism for how the loss of m could be prevented: we can't allow (without additional qualification) the reading of field m to return the actual owned reference to the underlying Money object, because reading a field can be done an arbitrary number of times. We must thus devise a system that enforces linearity, but nevertheless allows the programmer to manipulate owned fields and make state transitions.

Option 1: Simultaneous swap

One immediately obvious option is simply to return all the owned fields of an object from the transition statement: in the above example, ->NoMoney; would become Money m = ->NoMoney;. The below example shows this style:

contract MoneyHolder {
  state HasMoney {
    Money m;
    transaction removeMoney() returns m
                              ensures NoMoney {
      Money m = ->NoMoney;
      return m;
    }
  }

  state NoMoney {
    transaction addMoney(Money mNew) ensures HasMoney {
      ->HasMoney(m = mNew);
    }
  }
}

Unfortunately, this option has two drawbacks:

• it doesn't scale well with the number of linear fields (1, 2, 3 is okay, but 4+ is unwieldy).
• it is inconvenient in the case when we want to transition from S1 to S2, but where we calculate the fields of S2 from the fields of S1 non-trivially. These cases may require the definition of an intermediate state in which the calculations take place. A (admittedly contrived) example is shown below: the Limbo state isn't necessary for the program's logic, but must be defined to circumnavigate the restrictions of the simultaneous swap.

/* Holds two Money */
contract BoxedMoney {
  BoxedMoney(Money m1, Money m2) { this.m1 = m1; this.m2 = m2; }
  Money m1, m2;
  transaction destroy() returns (Money, Money) { ... }
}

contract Boxer {
  state Limbo {}
  state Unboxed {
    Money m1, m2; 
    transaction box() ensures Boxed {
      Money m1, m2 = ->Limbo;
      ->Boxed(m = new BoxedMoney(m1, m2));
    }
  }
  state Boxed {
    BoxedMoney m;
    transaction unbox() ensures Unboxed {
      BoxedMoney m = ->Limbo;
      Money m1, m2 = m.destroy();
      ->Unboxed(m1 = m1, m2 = m2);
    }
  }
}

Option 2: Special local analysis of this

The problem with reading the owned permission from a field is that the type of this doesn't change: since the type of this does not change, and the type determines what can be done to this, there's no way to prevent a field from being read twice (and thus duplicating an owned permission).

One solution to this problem is to change the type of this (at least locally) when an owned field is read. For example, if originally this : C, after reading an owned field f, we have this : C \ {f}, and the field f can be said to be "missing". Since these types talk about the fields of the contract, it doesn't make sense for outside viewers of the contract to see these types: thus, a reasonably restriction is that this must be in a "complete" state after a transaction (i.e. no fields are missing).

In this system, reading from a field that's already missing is an error. To perform a state transition from S1 to S2, all the owned fields of S1 (that are not in S2) must be missing. Calling other transactions while any fields are missing must also result in an error, because this opens up the possibility of some other contract seeing this in an inconsistent state; an alternative is to prevent re-entrant access to this.

The below example shows this style.

contract MoneyHolder {
  state HasMoney {
    Money m;
    transaction removeMoney() returns Money
                              ensures NoMoney {
      Money m = this.m;
      ->NoMoney;
      return m;
    }
  }

  state NoMoney {
    transaction addMoney(Money mNew) ensures HasMoney {
      ->HasMoney(m = mNew);
    }
  }
}

This option may be potentially confusing because linearity is enforced is quite implicitly. On the other hand, it's simple for the programmer in the sense that they can access fields as they normally would expect to (i.e. via reading).

Option 3: Pack/Unpack

Another option is to make the general strategy of Option 2 (i.e. allow this to enter an inconsistent state for some period of time while a transition occurs) more explicit. This can be done with the same sort of pack/unpack construct that appear in the formalism.

In general, we could have the following:

unpack {
  /* If [this] was in state [S1], and [S1] has fields [f_1, ..., f_n], then
   * these fields will be locally in scope for the duration of the block */
  /* statements go here */
} pack as S2(g_1 = x_1, ..., g_n = x_n)

Our example thus becomes:

contract MoneyHolder {
  state HasMoney {
    Money m;
    transaction removeMoney() returns Money
                              ensures NoMoney {
      Money m_ret;
      unpack {
        m_ret = m;
      } pack as NoMoney;
      return m_ret;
    }
  }

  state NoMoney {
    transaction addMoney(Money mNew) ensures HasMoney {
      /* this could perhaps be syntactic sugar for a unpack/pack with no body */
      ->HasMoney(m = mNew);
    }
  }
}

Like in Option 2, we need to prevent other contracts from seeing this in an inconsistent state, so we need to either restrict external calls inside of an unpack, or do dynamic checks for re-entrant calls.

This strategy has the advantage of being more explicit than Option 2 about the fact that this has a special status, but nevertheless being less terse.