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
82 stars 24 forks source link

Should properties and invariants of sub-isolates be hidden by default? #9

Open nano-o opened 3 years ago

nano-o commented 3 years ago

Consider this example: 

#lang ivy1.7
relation r1
isolate a = {
    axiom r1
}
isolate b = {
    invariant true
} with this

and the output of ivy_show isolate=b:

relation r1
axiom [a.axiom1] r1
conjecture [b.invar2] true

Should axiom r1 appear here? Or would it be better to require an explicit with a to bring in this property? Because of the current behavior, it is sometimes awkward to isolate properties and invariants that have quantifier alternations. For invariants, it seems one can use explicit as a workaround, but it does not work for properties.

kenmcmil commented 3 years ago

There are a couple of ways you could hide axiom r1 in 'this'. You could put isolate 'a' in the implementation (or private) section of 'this':

#lang ivy1.7
relation r1
implementation {
    isolate a = {
        axiom r1
    }
}

isolate b = {
    invariant true
} with this

That is, the visibility of sub-isolates is controlled in the same way as the visibility of other objects.

Or, you could could put the axiom in the implementation (or private) section of isolate 'a':

#lang ivy1.7
relation r1
isolate a = {
    implementation {
        axiom r1
    }
}

isolate b = {
    invariant true
} with this