Adds defaults to access requests using join-like semantics.

[klizhentas]

Consider this problem. Users can request policies, and for each policy, there has to be at least one approver.

To express this in Z3, we introduce "for_each" expression:

(RequestPolicy.names == ("access-stage",))
 & (
 RequestPolicy.names.for_each(
   lambda x: RequestPolicy.approvals[x].len() > 1))

This will get converted into anonymous recursive Z3 function that will iterate over list and apply the lambda expression.

[flyinghermit]

Can we abstract the lamda function so that users only need to write:

(RequestPolicy.names == ("access-stage",))
 & (RequestPolicy.names.minApproval(1))

instead of:

(RequestPolicy.names == ("access-stage",))
 & (
 RequestPolicy.names.for_each(
   lambda x: RequestPolicy.approvals[x].len() > 1))

?

[klizhentas]

Can we abstract the lamda function so that users only need to write:

(RequestPolicy.names == ("access-stage",))
 & (RequestPolicy.names.minApproval(1))

instead of:

(RequestPolicy.names == ("access-stage",))
 & (
 RequestPolicy.names.for_each(
   lambda x: RequestPolicy.approvals[x].len() > 1))

?

We can do that in the future, as a syntactic sugar I will create a ticket. For now I wanted to keep the underlying syntax mostly for visibility for you folks.

[klizhentas]

@xacrimon I have applied some changes, can you take another look