CLI tries to verify unmodified methods of refined types

[erniecohen]

Dafny version

4.8.1

Code to produce this issue

module arith {
function abs(x:int):nat { if x < 0 then -x else x }
function max(x:int,y:int):int { if x < y then y else x }
function min(x:int,y:int):int { if x < y then x else y }
function div(x:int,y:int):int requires 0 != y { x/y }
function mod(x:int,y:int):int requires 0 != y ensures x == div(x,y) * y + mod(x,y) { x % y }
function times(x:int,y:int):int { x * y }
}

module bools {
newtype B = bool {
    const b := this as bool
    static function B(b:bool):B { b as B }
    const n:nat := if b then 1 else 0
    static const T:B := true
    static const F:B := false
    const not := !this
    function or(n:B):B { this || n }
    function and(n:B):B { this && n }
    function xor(n:B):B { this != n }
    function plus(b0:B,b1:B):(r:(B,B)) ensures n + b0.n + b1.n == 2 * r.1.n + r.0.n {
        (xor(b0).xor(b1), if b then b0.or(b1) else b0.and(b1)) }  
    predicate imp(v:B) { b ==> v.b }
}
}

module ints {
import opened arith
import opened bools

newtype Int = int {  
    const b := 0 < this             
    const n:int := this as int      
    static const z:Int := 0
    static const m1:Int := -1        
    const z? := this == z 
    const m1? := this == m1
    const emp? := z? || m1?
    function prod(n:Int):Int { arith.times(this.n,n.n) as Int }
    function div(d:Int):Int requires d != z { arith.div(n,d.n) as Int }
    function mod(d:Int):Int requires d != z { arith.mod(n,d.n) as Int }
    const hd:B := mod(2) != 0
    const tl:Int := div(2)
    static function ctor(b:B):Int { if b then -1 else 0 }
    function cons(b:B):(n:Int) ensures n.hd == b && n.tl == this { b.n as Int + 2 * this }
    function len():nat ensures this < exp(len()) decreases abs(n) { if emp? then 0 else 1 + tl.len() }
    // addition with an incoming carry bit
    function plusC(n:Int,b:B):(r:Int) decreases len() + n.len()  ensures r == this + n + (b.n as Int) {
        var (b0,c0) := hd.plus(n.hd,b);        // add the ones digits
        if !emp? || !n.emp? then tl.plusC(n.tl,c0).cons(b0)      
        else if z? == n.z? then ctor(c0).cons(b0)
        else ctor(b.not)
    } 
    function plus(n:Int):(r:Int) ensures r == this + n { plusC(n,B.F)}

    /// shifts
    function lsh():(n:Int) ensures n == prod(2) {cons(B.F) } 
    function lshi(i:nat):(n:Int) ensures (this == 0 <==> n == 0) && (this < 0 <==> n < 0) { if i == 0 then this else lshi(i-1).lsh() }
    static function exp(i:nat):(r:Int) ensures 0 < r { (1 as Int).lshi(i)}
    function timesB(b:B):(r:Int) ensures r == prod(b.n as Int) { if b then this else 0 }
    function times(u:Int):(r:Int) decreases len() ensures r == prod(u) 
    { 
        if z? then z else if m1? then -u else 
        assert prod(u).n == (hd.n + 2 * tl.n) * u.n; 
        var r1 := tl.times(u.lsh()); 
        r1.plus(u.timesB(hd))
    }
}
}

module refints refines ints {
newtype Int ... {}
}

Command to run and resulting output

Dafny.dll verify --progress bug/dfyconfig.toml
where dfyconfig.toml specifies 
general-traits = "datatype"
type-system-refresh = "true"
general-newtypes = "true"

What happened?

This verifies fine in the IDE, but runs forever in the CLI. If you scroll to the bottom of the code, you see that the module refints should generate no verification conditions at all. In fact, it tries to reverify every function from ints, and verification gets stuck trying to verify refints.Int.times. I have no idea why this gets stuck while previous proofs do not in this example; this might indicate additional issues.

What type of operating system are you experiencing the problem on?

Mac

[erniecohen]

The fragility issue (causing the copied function to not verify) might perhaps be related to 5652.