Names for wires

[spitters]

@cmester0 suggested to have (nominal) names for "wires" e.g. names of functions. This would be helpful in Bert13 TLS where wires can be indexed by e.g. the round.

@MarkusKL responded: The main challenge is the interaction with the invariant. It can no longer be statically defined (from fixed locations), but by some mechanism the local names of the locations must be passed. The equality invariant on heaps would also be less useful, since there is no canonical relation between the two heaps (that may have been renamed). However, I think that it can still work.

Definition Loc (T : choice_type) := nat.
Definition to_Location {T} : Loc T → Location := λ n, (T; n).
Coercion to_Location : Loc >-> Location.

Definition LL {T : nomType} (A : choice_type) (k : Loc A → T) : T :=
  k (natize (neu (supp (k 0%N)))).

Definition pack : raw_module :=
  @LL raw_module 'unit (fun l1 =>
  @LL raw_module 'nat (fun l2 =>
    ([module fset [:: l1 : Location ; l2 : Location ] ;
      [ 0%N ] : { 'unit ~> 'unit } (x) {
        v ← get l2 ;;
        #assert (v > 5)%N ;;
        v ← get l1 ;;
        ret v
      }
    ]) : game _
  )).