An interesting question is whether or not we can allow the use of unbound quantifiers if we can provide witnesses behind the scenes.
As a simple example, imagine a function
// All elements in array are unique
property unique<T>(T[] arr)
where all { i in 0..|arr|, j in 0..|arr| | (i != j) ==> (arr[i] != arr[j]) }
// Can map from one array to another
property mapping<T>(T[] lhs, T[] rhs, int[] m)
where all { i in 0 .. |m| | lhs[m[i]] == rhs[i] }
function is_permutation<T>(T[] lhs, T[] rhs) -> (boolean r)
ensures r ==> |lhs| == |rhs| && some { int[] m | unique(m) && mapping(lhs,rhs,m) }
The challenge here is that the some quantifier is unbounded. However, we might have an internal function which actually produced a witness which demonstrates the some holds.
An interesting question is whether or not we can allow the use of unbound quantifiers if we can provide witnesses behind the scenes.
As a simple example, imagine a function
The challenge here is that the
somequantifier is unbounded. However, we might have an internal function which actually produced a witness which demonstrates thesomeholds.