1
Vote

Parametrized Module Instantiation with function argument is wrongly expanded (15-07-17)

description

Please consider the following auxiliary module:
------------------------- MODULE miniAbstractPaxos -------------------------
\* uncomment all extends, to let the theorem Abstraction in minimal go through
\* EXTENDS TLAPS, Integers \* use this and v will unfold to LAMBDA magicBallot, magicValue : TRUE
\* EXTENDS Integers, TLAPS \* use this and v will unfold to LAMBDA magicBallot, magicValue, x1, x2 : x1 + x2
EXTENDS TLAPS \* use this and v will unfold to A!SMT 


VARIABLES maxVal

AbsInit == maxVal  = [a \in {} |-> "null"]

=====
which defines the Operator AbsInit and the variable maxVal. We now define a parametrized instance A(x, magicValue) where we instanciate maxVal with a dummy operator dependent on magicValue:
------------------------------ MODULE minimal ------------------------------
CONSTANTS C,D

absMaxVal(magicValue) == {}

A(x,magicValue) == 
  INSTANCE miniAbstractPaxos WITH
                              maxVal <- absMaxVal(magicValue)

THEOREM Abstraction ==
  ASSUME NEW v
  PROVE  TRUE
<1>1. TRUE
  <2>. SUFFICES ASSUME TRUE PROVE A(v,v)!AbsInit
  <2>4. absMaxVal(v)  = [a \in C |-> "null"]
  <2>. QED  BY <2>4 DEF A!AbsInit
<1>. QED
====
Then the obligation depends on the extends statement in miniAbstractPaxos:
If there is no extends statement, the step <2> can be proven.

If we extend from Integers, TLAPS, we obtain the following obligation for <2>:
ASSUME NEW CONSTANT C,
       NEW CONSTANT D,
       NEW CONSTANT v,
       TRUE ,
       absMaxVal(v) = [a \in C |-> "null"] 
PROVE  absMaxVal(LAMBDA x, magicValue, x1, x2 : x1 + x2)
       = [a \in {} |-> "null"]
If we remove extend TLAPS first and then Integers, we obtain:
ASSUME NEW CONSTANT C,
       NEW CONSTANT D,
       NEW CONSTANT v,
       TRUE ,
       absMaxVal(v) = [a \in C |-> "null"] 
PROVE  absMaxVal(LAMBDA x, magicValue : TRUE) = [a \in {} |-> "null"]
And if we extend only TLAPS, we obtain:
ASSUME NEW CONSTANT C,
       NEW CONSTANT D,
       NEW CONSTANT v,
       TRUE ,
       absMaxVal(v) = [a \in C |-> "null"] 
PROVE  absMaxVal(A!SMT) = [a \in {} |-> "null"]
In all cases, v should not be expanded to anything, since it is a new variable (and even if it were an operator, it needed to be contained in the BY DEF statement).

This behaviour is also quite fragile: changing A(x,magicValue) to A(magicValue) makes the bug disappear. Likewise, if we remove the SUFFICES step and use the same argument for the outer proof(the statement is the same after narrowing the problem down), the bug also disappears.

file attachments

comments