Meaning of ? variables

[goodlyrottenapple]

We seem to currently have an inconsistent state of existential variables.

The issue originally arose from this bug: runtimeverification/haskell-backend#3605, where the backend claims #Exists X . #Exists Y . { true #Equals 0 >Int Y } #And { true #Equals 0 <=Int X } is invalid.

Upon investigation, it turned out the backend was stripping the existentials (this change was introduced by runtimeverification/haskell-backend#3193) and essentially checking #Forall X . #Forall Y . { true #Equals 0 >Int Y } #And { true #Equals 0 <=Int X } with Z3, which is of course invalid.

However, when we try to revert the above change to get the correct behaviour for the aforementioned bug, we run into the following error:

https://github.com/runtimeverification/haskell-backend/blob/2e33122cd354045da4e5f40dea9344e02c673a64/kore/src/Kore/Simplify/Exists.hs#L397-L401

This error arises when we get an existential variable appearing both in the configuration and the requires/ensures clause, e.g. when applying this foundry rule:

https://github.com/runtimeverification/evm-semantics/blob/c84e3466aa2ca2f4dea43870369b2ccab012e2f4/include/kframework/foundry.md?plain=1#L565-L570

since the above rule is encoded in kore as:

axiom{} \rewrites{SortGeneratedTopCell{}} (
      ...,
      \exists{SortGeneratedTopCell{}} (Var'Ques'WORD:SortInt{},  ...)
)

or whenever pyk sends over an implies request and explicitly applies an existential quantifier over any unbound variables on the RHS (from runtimeverification/haskell-backend#3620 (comment)):

Quantifying both the term and the predicate probably means that there's
an error somewhere else.
variable=ConfigVarISEVENTEXPECTED'Unds'FINAL:SortBool{}
patt=\and{SortGeneratedTopCell{}}(
    /* term: */
    /* Sfa */
    \exists{SortGeneratedTopCell{}}(
        ConfigVarCHECKEDTOPICS'Unds'CELL'Unds'5d410f2a:SortList{},
        /* Sfa */
        \exists{SortGeneratedTopCell{}}(
            ConfigVarCHECKEDDATA'Unds'CELL'Unds'5d410f2a:SortBool{},
            /* Sfa */
            \exists{SortGeneratedTopCell{}}(
                ConfigVarEXPECTEDEVENTADDRESS'Unds'CELL'Unds'5d410f2a:SortAccount{},
                /* Sfa */
                \exists{SortGeneratedTopCell{}}(
                    ConfigVarISCALLWHITELISTACTIVE'Unds'FINAL:SortBool{},
                    /* Sfa */
                    \exists{SortGeneratedTopCell{}}(
                        ConfigVarISSTORAGEWHITELISTACTIVE'Unds'FINAL:SortBool{},
                        /* Sfa */
                        \exists{SortGeneratedTopCell{}}(
                            ConfigVarADDRESSSET'Unds'FINAL:SortSet{},
                            /* Sfa */
                            \exists{SortGeneratedTopCell{}}(
                                ConfigVarSTORAGESLOTSET'Unds'FINAL:SortSet{},
                                /* Sfa */
                                \exists{SortGeneratedTopCell{}}(
                                    ConfigVarGENERATEDCOUNTER'Unds'CELL'Unds'5d410f2a:SortInt{},
                                   ...
\and{SortGeneratedTopCell{}}(
    /* predicate: */
    /* Sfa */
    \equals{SortBool{}, SortGeneratedTopCell{}}(
        /* T Fn D Sfa Cl */ \dv{SortBool{}}(\"true\"),
        /* Fn Sfa */
        Lblfoundry'Unds'success{}(
            /* T Fn D Sfa */ ConfigVarSTATUSCODE'Unds'FINAL:SortStatusCode{},
            /* T Fn D Sfa */
            Lbl'Hash'lookup'LParUndsCommUndsRParUnds'EVM-TYPES'Unds'Int'Unds'Map'Unds'Int{}(
                /* T Fn D Sfa */
                ConfigVarCHEATCODE'Unds'STORAGE'Unds'FINAL:SortMap{},
                /* T Fn D Sfa Cl */
                \dv{SortInt{}}(\"46308022326495007027972728677917914892729792999299745830475596687180801507328\")
            ),
            /* T Fn D Sfa */ ConfigVarISREVERTEXPECTED'Unds'FINAL:SortBool{},
            /* T Fn D Sfa */ ConfigVarISOPCODEEXPECTED'Unds'FINAL:SortBool{},
            /* T Fn D Sfa */ ConfigVarRECORDEVENT'Unds'FINAL:SortBool{},
            /* T Fn D Sfa */ ConfigVarISEVENTEXPECTED'Unds'FINAL:SortBool{}
        )
    ),
    /* substitution: */
    \top{SortGeneratedTopCell{}}()
))

Since the introduction of runtimeverification/haskell-backend#3193, we have essentially been turning all these existential variables into universal ones, hence the above error never occurred, but this is obviously not sound as evidenced by runtimeverification/haskell-backend#3605. The question is, which of the following options is the correct one?

1. change the encoding of ? vars on the RHS of a rewrite rule to a universally quantified one (this is seemingly the status quo, given [Simplification request] Top-level existential elimination haskell-backend#3193
2. remove the https://github.com/runtimeverification/haskell-backend/blob/2e33122cd354045da4e5f40dea9344e02c673a64/kore/src/Kore/Simplify/Exists.hs#L397-L401 error, allowing existentials in the config and predicates simultaneously (@virgil-serbanuta you mentioned this is usually indicative of a bug?)
3. keep things as they are??

[virgil-serbanuta]

I think that having an existential in the config and predicate is also indicative of an error in this case (or, at least, a confusion).

I think it would be useful to have more clarity about what use-cases we are trying to support, and what ways of encoding them are acceptable to end-users (also see the examples below).

Next, we should decide in which case we actually need to quantify the variables we use (see the end of the paragraph, we don't always need to quantify existential variables).

Let's take a few examples:

1. Generating random numbers with rule rand => ?X ensures Min <= ?X andBool ?X <= Max
2. Producing unspecified, but fixed values, e.g. producing a value that is not in a set: rule pickNotIn(S:Set) => ?X ensures notBool ?X in S.
3. Writing summarization rules, e.g. rule call(stuff) => ?X ensures ....

I'm claiming that:

1. The first example above should be encoded as forall ?X . (rand #And {true #Equals (Min <= ?X andBool ?X <= Max)}) => ?X
2. The second example above might be encoded as exists ?X . pickNotIn(S:Set) => (?X #And {true #Equals notBool ?X in S}), but it may be better to define it as pickNotIn(S:Set) => (f(S) #And {true #Equals notBool f(S) in S}) where f is an unevaluated function that is unique to a (rule, question-mark-variable) pair.
3. The third example above is ambiguous - was "?X" generated by something similar to the first rule above, or something similar to the second rule above, or is it a non-deterministic value, e.g. different values were produced on the various execution branches, and we abstracted that with a variable?

A few comments about the encodings above:

1. forall ?X . (rand #And {true #Equals (Min <= ?X andBool ?X <= Max)}) => ?X means that 'rand' rewrites to all possible ints for which Min <= ?X andBool ?X <= Max.
2. If we encoded the 'rand' rule as forall ?X . rand => (?X #And {true #Equals (Min <= ?X andBool ?X <= Max)}) then this would mean that rand rewrites to all the ints in an unspecified non-empty subset of {Min, Min+1, ... Max} (in particular, rand may or may not be non-deterministic). In practice, it's likely that any proof that works under these constraints, would also work with the forall encoding. However, the point below argues that we may also like to add an uniqueness constraint (i.e. there is a unique value such that ...) - this would make this encoding inappropriate for rand since it would become deterministic.
3. If we encode the second example as exists ?X . pickNotIn(S:Set) => (?X #And {true #Equals notBool ?X in S}) then this is underspecified, since pickNotIn(S:Set) rewrites to a specific value that depends only on S. We may want to rewrite this as exists-and-is-unique ?X . pickNotIn(S:Set) => (?X #And {true #Equals notBool ?X in S}) or something similar.
4. If we encode the second example as pickNotIn(S:Set) => (f(S) #And {true #Equals notBool f(S) in S}) then this would encode exactly what we need.

Depending on what we want to do, we may or may not be able to use the same representation for all examples above. As an example, in all-path proofs, existential variables are transformed in universally quantified variables (e.g. if we want to prove forall X . exists Y . a(X) =ap=> c(Y) and we have a rule that says exists ?Z . a(X) => b(?Z) then we can apply it and quantify ?X universally since the remaining claim to prove is forall ?Z . exists Y . b(?Z) =ap=> c(Y).

[goodlyrottenapple]

also related related: #1046
and this discussion from the above: https://riot.im/app/#/room/!MfVXcmpKuyudZHcqil:matrix.org/$1579293981718150SvIjN:matrix.org

[radumereuta]

@goodlyrottenapple this was opened a while ago. What were the actions needed to be taken here?

[goodlyrottenapple]

Honestly, I'm not sure...probably best to revisit this if/when pertinent to the booster. We don't really have the capacity to try to fix this in the old backend and we seem to have work-arounds in place.