[Feature Request] Set/Map in spec lang

[emmazzz]

🚀 Feature Request

While specifying VASP.move, I noticed that I couldn't reason about something like "number of ChildVASPs who have parent_vasp as their parent". Being able to talk about this is important because we want to prove in VASP that for all parent_vasp, number of ChildVASPs who have parent_vasp as their parent is indeed equal to parent_vasp.num_children.

A few potential ways to solve this issue:

• Implement set and cardinality of set in spec lang so that we can write maybe size({ addr | is_child_vasp(addr) && parent(addr) == parent_vasp }).
• Add support for map to ghost variables so that we can have a map from addresses to u64s tracking number of children for each parent vasp address.
• Implement ghost fields so that we can add a vector field in ParentVASP representing all the children. This issue is already raised in #4221

[shazqadeer]

I looked at VASP.move in a bit more detail yesterday.

• Implement set and cardinality of set in spec lang so that we can write maybe size({ addr | is_child_vasp(addr) && parent(addr) == parent_vasp }).

I would advocate against taking this approach because the native support for cardinality reasoning on arbitrarily-constructed sets is extremely poor. In the past, when I have had to use cardinality reasoning, I added carefully constructed axioms and lemmas. However, I think it is a good idea to add, for specification purposes, variables of type finite set just like we can have variables of type finite vector today.

• Add support for map to ghost variables so that we can have a map from addresses to u64s tracking number of children for each parent vasp address. I think you mean that we need a ghost variable g whose type is a map from addresses to Vec

  and g[x] represents the list of child VASP addresses. Then we can capture the desired specification by comparing len(g[x]) with num_childreen in the parent VAP resource published at x. If we added the finite set type, we could also use a map from addresses to Set

  .

• Implement ghost fields so that we can add a vector field in ParentVASP representing all the children. This issue is already raised in #4221 This is a good alternative to the second approach above.

It looks to me that to verify the specification under question, a new feature is needed. I find the feature of ghost fields a more general and powerful feature that could potentially solve other problems also but it is also likely more difficult to implement than adding more expressiveness to global ghost variables.