search

informalsystems / quint

An executable specification language with delightful tooling based on the temporal logic of actions (TLA)
Apache License 2.0
782 stars 31 forks source link

Quint allows let-bindings where operators are expected, breaking integration with Apalache #1403

Open p-offtermatt opened 6 months ago

p-offtermatt commented 6 months ago

Apalache is version 0.44.7 Quint version 0.18.3 Spec: https://github.com/cosmos/interchain-security/blob/8184c49ab6f6edb3e53cd7b6a70c127d5b65eb24/tests/mbt/model/ccv_model.qnt#L178

% quint verify ccv_model.qnt --verbosity 5
error: internal error: while parsing in Apalache:
'Input was not a valid representation of the QuintIR: Operator forall is a binding operator requiring an operator as it's second argument,
but it was given QuintLet(1938,QuintOpDef(1918,providerState_1938,val,QuintApp(1917,field,List(QuintName(1915,currentState), QuintStr(1916,providerState)))),QuintLambda(1937,List(QuintLambdaParameter(1919,consumer_1937)),def,QuintApp(1936,exists,List(QuintApp(1925,toSet,List(QuintApp(1924,get,List(QuintApp(1922,field,List(QuintName(1920,providerState_1938), QuintStr(1921,sentVscPacketsToConsumer))), QuintName(1923,consumer_1937))))), QuintLambda(1935,List(QuintLambdaParameter(1926,packet_1935)),def,QuintApp(1934,eq,List(QuintApp(1929,field,List(QuintName(1927,packet_1935), QuintStr(1928,validatorSet))), QuintApp(1933,applyKeyAssignmentToValSet,List(QuintName(1930,providerState_1938), QuintName(1931,consumer_1937), QuintName(1932,providerValSetInCurBlock_1940))))))))))'
bugarela commented 6 months ago

Discussed in slack, I'll add the important context here. The error happens because of a let-binding as the second arg to forall:

runningConsumers.forall(
            // ...the validator set under key assignment is in a sent packet...
            val providerState = currentState.providerState
            consumer => providerState.sentVscPacketsToConsumer.get(consumer).toSet().exists(
                packet => 
                    packet.validatorSet == 
                    applyKeyAssignmentToValSet(providerState, consumer, providerValSetInCurBlock)
            )
        )

Moving the val providerState = currentState.providerState up or down in scope fixes it.

Follow-up: we should detect cases like this in quint during static analysis and report an error. It's a weird place to have a let binding.

bugarela commented 6 months ago

More context from @shonfeder: It’s because the “binding operators” like forall and exists need to locate the variable to be bound from the operator given as its first argument, and the logic here is not generalized to handle let bindings that happen to evaluate to operators.

This S.forall(x => P) is translated into \A x \in S: P.