Fuel setting on a function used in a constrained type declaration erroneously affects the witness verification

[saltiniroberto]

The following piece of code verifies correctly.

module M {
    predicate method p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

---

However, the verification of the following piece of code,

module M {
    predicate method p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method {:fuel p1,1,2} m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

where the annotation {:fuel p1,1,2} has been added to method m, fails with error

test.dfy(19,35): Error: result of operation might violate subset type constraint for 'T1'
Execution trace:
    (0,0): anon0
    (0,0): anon4_Else

Dafny program verifier finished with 4 verified, 1 error

---

The same happens if the annotation {:fuel 1,2} is added to the function p1 as follows.

module M {
    predicate method {:fuel p1,1,2} p1(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }

    predicate method p2(x:nat)
    {
        if x < 6 then 
            true
        else
            p1(x-1)
    }    

    type T1 = x:nat | p1(x) witness 5
    type T2 = x:T1 | p2(x) witness 5

    method m(x:nat) returns (x':nat)
    {
        x' := 0;
    }
}

[RustanLeino]

Thanks for the bug report. There are various issues with custom fuel settings and encodings (e.g., #670). It's not clear to me if this is a feature we want to continue to support. So, let me ask: What is it you're hoping to do with this fuel setting? Could you live without it just as well (perhaps by inserting some lemma somewhere)?

[saltiniroberto]

I have the need to define constrained types based on inductive datatypes where I want to constrain the constructor used for some of the inductive parameters. Here is a exemplary version of what I am trying to do.

datatype D =    | L1(x:nat)
                | L2(y:real)
                | N0(a:D, b:D)
                | N1(a:D, b:D)
                | R1(a:D, b:D)
                | R2(a:D, b:D)

predicate wT(d:D)
{
    match d 
        case L1(x) => true
        case L2(y) => true
        case N0(a,b) => && a.L1? && wT(a)
                        && b.L2? && wT(b)

        case N1(a,b) => && a.L2? && wT(a)
                        && b.L1? && wT(b)                            

        case R1(a, b) =>    && a.N0? && wT(a)
                            && b.N1? && wT(b)     

        case R2(a, b) =>    && a.L1? && wT(a)
                            && b.N1? && wT(b)          

}

type T1 = x:D | wT(x) witness L1(0)
type R1T = x:T1 | x.R1? witness R1(N0(L1(0),L2(0.0)), N1(L2(0.0),L1(0)))

Now, if I have a method that takes an argument of type R1T for which I define a pre-condition like below,

method mm(t:R1T)
requires t.a.a.x < 8
{ }

it appears to me that I have only two options to get Dafny to verify the well-formedness of the method siganture

1. The first is to use the fuel setting as below, which, however, due to the bug that I have reported, it causes the verification of the witnesses for the types T1 and R1T to fail.

   method {:fuel wT,2,3} mm(t:R1T)
   requires t.a.a.x < 8
   { }

2. The second options is to use an additional requires, which, however, clutters the specification.

   method mm(t:R1T)
   requires wT(t.a)
   requires t.a.a.x < 8
   { }

[parno]

When you add the fuel annotation, Dafny introduces new fuel-related constants, but it looks like there's a bug in the well-formedness check for subset type definitions such that the value of those constants are never defined, which is why your witness suddenly fails to satisfy the check.

In a small experiment, I tried factoring your original example into two files:

s.dfy:

module M {
  predicate method p1(x:nat)
  {
    if x < 6 then 
      true
    else
      p1(x-1)
  }

  predicate method p2(x:nat)
  {
    if x < 6 then 
      true
    else
      p1(x-1)
  }    

  type T1 = x:nat | p1(x) witness 5
  type T2 = x:T1 | p2(x) witness 5
}

t.dfy

include "s.dfy"

module  N {
  import opened M

  method {:fuel p1,1,2} m(x:nat) returns (x':nat)
  {
      x' := 0;
  }
}

Each verifies individually, presumably because the fuel annotation in t.dfy doesn't affect the verification of the subset types in s.dfy. It's a bit cumbersome, but perhaps that will help you as a workaround in your larger example.