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

Allow casting of range types inside ivy_check #40

Closed benSepanski closed 2 years ago

benSepanski commented 2 years ago

This commit seeks to enable casting of range types to integer types inside isolates.

Running ivyc on this example works. However, running ivy_check produces the error cast is not a supported Z3 function.

#lang ivy1.8

include collections
include numbers

isolate adder = {
    var value : nat
    type one_t = {1}
    export action add = {
        var one : one_t := 1;
        require value >= cast(one);
    }
}
benSepanski commented 2 years ago

I think this is incorrect, based on a piazza post response