More efficient evaluation of SequencesExt!BoundedSeq when e.g. checking refinement

[lemmy]

The module Foo models a system where -at every step- the log is extended by a subsequence of up to length C from the set S. It is straightforward to see that the module Bar refines Foo. However, TLC fails to verify the refinement because it cannot enumerate the set of all subsequences SeqOf(S, 42).

----- MODULE Foo ------
EXTENDS Naturals, Sequences, SequencesExt

CONSTANT S, C

VARIABLE log

Init ==
    log = <<>>

Next ==
    \E suffix \in SeqOf(S, C) :
        log' = log \o suffix

NextRefine ==
    /\ log' \in Seq(S)
    /\ IsPrefix(log, log')
    /\ Len(log') <= Len(log) + C

Spec == Init /\ [][Next]_log
=====

----- MODULE Bar -----
EXTENDS Sequences

VARIABLE log

Spec == log = <<>> /\ [][log' = log \o <<"a">>]_log

Foo == INSTANCE Foo WITH C <- 42, S <- {"a"}
THEOREM Spec => Foo!Spec

\* .cfg files do not accept the ! in Foo!NextRefine
FooNextRefine == Foo!NextRefine
=====

Clearly, when verifying refinement, it's conceptually unnecessary for TLC to enumerate SeqOf(S, 42). Instead, it would be sufficient to check something like NextRefine, which TLC will check if we redefine Next with NextRefine:

CONSTANT Next <- [Foo]FooNextRefine

However, SeqOf could be enhanced to symbolically check ... \in SeqOf(S, C), similar to how TLC checks Seq(S):

https://github.com/tlaplus/tlaplus/blob/475477653f01447f60603288a2785df1447bdbeb/tlatools/org.lamport.tlatools/src/tlc2/module/Sequences.java#L391-L411

Additionally, this new tlc2.value.impl.Value implementation should properly implement tlc2.value.impl.Enumerable#elements to lazily enumerate the elements of SeqOf when evaluating the existential quantification\E s \in SeqOf(S,C): log' = ....

[lemmy]

Adding the following to SequencesExt.java causes TLC to treat BoundedSeq/SeqOf strictly symbolically. However, there is no infrastructure for a hybrid value. We would have to implement a BoundedSeqValue that extends TLC's Value class.

@TLAPlusOperator(identifier = "SeqOf", module = "SequencesExt", warn = false)
public static Value SeqOf(final Value range, final IntValue size) {
        UserObj obj = new Sequences(range, size.val);
        return new UserValue(obj);
}