The security property only talks about what the verifier should output in case all honest full nodes agree. However, there is no requirement for the case where the miners disagree. Perhaps in case of disagreement the verifier should output undefined, i.e. the security definition should be amended with "and undefined otherwise."
However, this seems problematic as it may be impossible to achieve: If the honest miners do not agree about the predicate's value and the verifier speaks to a particular honest miner, they may extract a wrong value if the verifier is too eager to extract a value. On the other hand, if the verifier is cautious and waits for k blocks to bury the property, the honest miners may come to agreement before the verifier is satisfied.
The security property only talks about what the verifier should output in case all honest full nodes agree. However, there is no requirement for the case where the miners disagree. Perhaps in case of disagreement the verifier should output
undefined, i.e. the security definition should be amended with "and undefined otherwise."However, this seems problematic as it may be impossible to achieve: If the honest miners do not agree about the predicate's value and the verifier speaks to a particular honest miner, they may extract a wrong value if the verifier is too eager to extract a value. On the other hand, if the verifier is cautious and waits for k blocks to bury the property, the honest miners may come to agreement before the verifier is satisfied.