search

kenmcmil / ivy

IVy is a research tool intended to allow interactive development of protocols and their proofs of correctness and to provide a platform for developing and experimenting with automated proof techniques. In particular, IVy provides interactive visualization of automated proofs, and supports a use model in which the human protocol designer and the automated tool interact to expose errors and prove correctness.
Other
77 stars 24 forks source link

Error in compiling `total order properties` code in examples with ivy1.7 #29

Open prpr2770 opened 2 years ago

prpr2770 commented 2 years ago

While executing some of the documented examples in Ivy Leader Election[http://microsoft.github.io/ivy/examples/leader.html], with ivy1.7, I found some errors with ivy_check. 

#lang ivy1.7

module total_order_properties(t) = {
    property [transitivity] X:t < Y & Y < Z -> X < Z
    property [antisymmetry] ~(X:t < Y & Y < X)
    property [totality] X:t < Y | X = Y | Y < X
}

isolate id = {
    type this

    specification {
        instantiate total_order_properties(this)
    }
}

Compiling the same with ivy_check generates 3 errors. 

$ ivy_check id.ivy 

Isolate id:

    The following properties are to be checked:
        id.ivy: line 4: id.transitivity ... FAIL
        id.ivy: line 5: id.antisymmetry ... FAIL
        id.ivy: line 6: id.totality ... FAIL

    The following temporal property is being proved:

        id.ivy: line 4: id.transitivity

    The following temporal property is being proved:

        id.ivy: line 5: id.antisymmetry

    The following temporal property is being proved:

        id.ivy: line 6: id.totality

Isolate this:

    The following properties are assumed as axioms:
        id.ivy: line 4: id.transitivity
        id.ivy: line 5: id.antisymmetry
        id.ivy: line 6: id.totality

error: failed checks: 3

Additionally, when generating a trace of the same, we obtain the following: 

$ ivy_check trace=true id.ivy 

Isolate id:

    The following properties are to be checked:
        id.ivy: line 4: id.transitivity ... FAIL
searching for a small model... done
[
    @Y = 0
    1:id < 0 = true
    0:id < 1 = true
    0:id < 0 = true
    1:id < 1 = false
    @Z = 1
    @X = 1
]