Support for a Native Set Datatype

[Robert-Brune]

Please describe your proposal in a ONE sentence

Add a native abstract key datatype of finite sets.

Underlying problem

Most advanced data structures can be modelled by sum or product of common value types, sequences,
finite maps and finite sets.
There are native types for the first three, but none for finite sets.
There are also SMT-solver, which already support finite sets (cvc5).

Usage Scenario

As soon as one wants to use the common interface Set in Java,
a proper way to represent the state in key would be helpful.

The following interface should give a first idea of such a type:

/*!
Abstract datatype of finite sets.
*/

\sorts {
    Set;
}

\functions {

    // constructors    
    Set setEmpty;
    Set setSingelton(any);
    
    Set setUnion(Set, Set);
    Set setInter(Set, Set);
    Set setMinus(Set, Set);

    Set setAdd(Set, any); // shortcut for setUnion(x, setSingleton(y));
    Set setRemove(Set, any); // shortcut for setMinus(x, setSingleton(y));

    Set seq2Set(Seq);
    
    // Combination with map type
    Set mapKeys(Map);
    Set mapValues(Map);
}

\predicates {
    setMember(Set, any);
    setSubset(Set, Set);
    setDisjunct(Set, Set);
}

Alternatives

At the moment, I think it is possible to use the key type map,
but this seems rather like a nasty workaround.
A native type would make the intension of the specification more clear and easier to understand.

Estimated effort

There might be many rules from locset that also work for this general set.
In the end, it comes down to the rules,
where I lack the expertise to make this new interface usable.

Additional context

This would be nice for Contract-Chameleon, which relies on a theory of sets.

Simplified SMT-Lib specification of finite sets, used by Contract-Chameleon:

:smt-lib-version 2.7
:written-by "Robert Brune"
:date "2025-09-30"
:last-updated "2025-09-30"

:note
"This definition of finite set interface is used by contract-chamelon.
It is highly oriented from the specification of cvc5:
"

:sorts ((Set 1))

:constants  

:funs ((par (A) (seq.union ((Set A) (Set A)) (Set A)))
       (par (A) (seq.inter ((Set A) (Set A)) (Set A)))
       (par (A) (seq.minus ((Set A) (Set A)) (Set A)))

       (par (A) (seq.member ((Set A) A) Bool))
       (par (A) (seq.subset ((Set A) (Set A)) Bool))
       (par (A) (seq.disjunct ((Set A) (Set A)) Bool)) 

       (par (A) (as set.emtpy (Set A)))
       (par (A) (set.singleton (A) (Set A)))

       (par (A) (set.card (Set A) Int))
      )

:note
"
[1] Set definition from:
[cvc5](https://cvc5.github.io/docs/cvc5-1.3.1/theories/sets-and-relations.html)
"
)

[Drodt]

That's definitely something we should add. Except that we should (imo) build on #3652 and make sets polymorphic: Set<[int]> instead of Set with elements of sort any.

[WolframPfeifer]

I implemented something basic for a case study on my fork: https://github.com/WolframPfeifer/key/tree/pfeifer/encPaper2

It is very similar to the above, since I needed it quickly, it does not yet use polymorphic sorts, and only is very minimal in the set of functions and rules. However, it was sufficient for specifying and verifying a basic IntTreeSet implementation.
I will look into making it polymorphic in the near future.