[andrewcmyers]

Number different versions of principal variables so we can use them all in labels. This is a pretty complicated change and I admit I let Claude go a little wild implementing it. It's needed though so we can get label checking right.

[andrewcmyers]

Versions of mutable principals.

• A non-final variable of contract, interface or address type can now appear in labels and trust tests. Previously only final variables could.
• Each assignment gives the variable a new version, x..vN. Every version is a separate principal in SHErrLoc.
• An assignment records that the new version names the same principal as the assigned value. It does this with an assumption (assumeSamePrincipal), not a checked constraint.
• Where control flow meets (If, EndorseIfStatement, While, For, Try, Atomic), mergeVersions gives a variable a fresh merged version if its branches disagree.
• Loop heads and catch handlers give the variables assigned in the body fresh, unconstrained versions.
• Calls and new do the same for every mutable principal field, because the callee may reenter and change them.
• Trust tests. A trust test (if (a => b)) records its fact about the current version, so the fact lapses once a or b is reassigned.
• One label per variable. All versions of a variable share a single value label. Labels that change with each version are left for later.

How labels use versions.

• PrimitiveLabel has an optional version.
• VisitEnv.toLabel resolves each principal in a label to its current version.
• Expression.principalName returns the principal an expression denotes: for a name, its current version; for a cast to a contract or address type, the principal of its argument.
• Calls, new, and closure creation and binding all use principalName to map the callee's principal parameters. That replaces several hand-written special cases that worked only for final variables.

Final fields.

• Every final field must be assigned exactly once, by a top-level statement of a constructor (or a pasted super-constructor). Contract.markFinalFieldInits enforces this.
• Any other assignment to a final variable, field, local or parameter, is rejected.
• Field labels may name only final variables.
• The old "not initialized" error for fields is gone.

Built-ins.

• sender, value and now are labeled {TOP}. The runtime sets them, so they are trusted data.
• sender is still a sealed address: trusting the value doesn't mean trusting the contract it names.

Tests.

• New IFC tests:
  • TrustFactReassign_W01, TrustFactBranch_W01, TrustFactLoop_W01 and TrustFactFieldCall_W01;
  • TrustFactKept;
  • NonFinalPrincipalLabel_W01;
  • ValueNowTrusted;
  • FinalFieldInit.
• New regular type-checking tests: FinalFieldInitOK and seven Final*/FieldLabelNonFinal negatives.
• TrustQueryNonFinal_W01 is now a positive test, since trust tests on non-final addresses are allowed.