Separate free_ips and free_ports

[jihgfee]

Currently, free_ports only arise from using Ht-start, and giving up free_ips. This put unecessary coupling between the free_ips and free_ports resources.

A suggestion is then to separate the two, by specifying the free_ports up front (during adequacy), instead of getting them using Ht-start. Additional motivation can be found at the bottom of this issue.

To change this, I suggest splitting the free ip "coherence" definition in two, as follows:

  (** Free ips coherence *)
  (* Free ips have no bound ports, no heap, and no sockets  *)
  Definition ip_is_free (ip : ip_address) (σ : state) : Prop :=
    state_heaps σ !! ip = None ∧ state_sockets σ !! ip = None.

  Definition free_ips_coh σ : iProp Σ :=
    ∃ free_ips,
      ⌜set_Forall (λ ip, ip_is_free ip σ) free_ips⌝ ∗
      free_ips_auth free_ips.

  (** Free ports coherence *)
  (* Free ports are not in use *)
  Definition free_ports_coh σ : iProp Σ :=
    ∃ free_ports,
      ⌜map_Forall (λ ip ports,
                     (∀ Sn, (state_sockets σ) !! ip = Some Sn →
                            set_Forall (λ p, port_not_in_use p Sn) ports))
                  free_ports⌝ ∗
      free_ports_auth (GSet <$> free_ports).

It is then necessary to lift the existing free ip and free ports lemmas, as well as the adequacy theorem. Finally, this is a breaking chance, so it is necessary to bump all of the examples manually (by specifying free ports during adequacy instead of during starting of new nodes).

The main benefit is that it much better supports a multi-node adequacy theorem (which will be very helpful for applying Trillium to Aneris, as modelling the Start node for every program will be a hassle). In such a case, you would never be able to get FreePorts, as the resource is tied to the specification of Start. It would be possible to get FreePorts for all the nodes that you do not get FreeIp for, but the adequacy theorem starts being very intricate then, as there are a multitude of sets hanging around (e.g. the set of addresses with histories/protocols, the set of free IPs, the set of free ports (that does not overlap with the set of free ips)).

The proposed change would instead allow the adequacy theorem to just require specifying:

What addresses are in your system (to get Unallocated, Message Histories, and FreePorts for them)
What IPs are initially free

In case you do not require allocating new nodes, you can even omit the specification of IPs.

Another benefit is that you would be able to define abstract specifications of specific node start ups in terms of the initial resources, that you then get on start up (with a potential custom adequacy theorem). This is currently not possible, as you only get FreePorts later