Beginner question

Jan 29, 2016 at 1:01 PM
Edited Jan 29, 2016 at 1:02 PM
Hi,

I am trying to learn Dafny by porting some definitions and theorems that I have developed in Coq. Unfortunately, Dafny (Z3?) seems to be stuck trying to prove the very first theorem that I gave to it. It keeps running for a long time without giving any answer. I would like to know how can I proceed in cases like that. Should I wait more (1h, 2h, 1d)? Should I try to point Dafny in the direction of the proof? If so, how do I do this?

Below is the code that I am giving to Dafny. It defines natural numbers, their positional representation and also the sum of representations (the algorithm that we learn in school). The theorem in the ensures clause of the function somaDecimal relates the sum of representations with the sum of naturals.
datatype Natural = Zero | Sucessor(Natural)

function method somaNatural(m: Natural, n: Natural): Natural {
  match n {
    case Zero => m
    case Sucessor(n') => Sucessor(somaNatural(m, n'))
  }
}

function method produtoNatural(m: Natural, n: Natural): Natural {
  match n {
    case Zero => Zero
    case Sucessor(n') => somaNatural(m, produtoNatural(m, n'))
  }
} 

datatype Digito = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9

function method conversaoDigito(d: Digito): Natural {
  match d {
    case D0 => Zero
    case D1 => Sucessor(Zero)
    case D2 => Sucessor(Sucessor(Zero))
    case D3 => Sucessor(Sucessor(Sucessor(Zero)))
    case D4 => Sucessor(Sucessor(Sucessor(Sucessor(Zero))))
    case D5 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))
    case D6 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero))))))
    case D7 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))
    case D8 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero))))))))
    case D9 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))
  }
}

datatype Decimal = Constante(Digito) | Coeficiente(Digito, Decimal)

datatype NaturalNatural = NaturalNatural(Natural, Natural)

function method conversaoDecimalAux(ds: Decimal): NaturalNatural {
  match ds {
    case Constante(d) => NaturalNatural(conversaoDigito(d), Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))))
    case Coeficiente(d, ds') =>
      match conversaoDecimalAux(ds') {
        case NaturalNatural(n', p') =>
          NaturalNatural(somaNatural(conversaoDigito(d), n'), produtoNatural(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))), p'))
      }
  }
}

function method conversaoDecimal(ds: Decimal): Natural {
  match conversaoDecimalAux(ds) {
    case NaturalNatural(n, p) => n
  }
}

function method alinhamentoAux(cs: Decimal, cs': Decimal, ds: Decimal): Decimal {
  match ds {
    case Constante(d) => cs
    case Coeficiente(d, ds') =>
      match cs' {
        case Constante(c') => Coeficiente(D0, alinhamentoAux(cs, cs', ds'))
        case Coeficiente(c', cs'') => alinhamentoAux(cs, cs'', ds') 
      } 
  }
}

function method alinhamento(cs: Decimal, ds: Decimal): Decimal {
  alinhamentoAux(cs, cs, ds)
}

datatype Booleano = Falso | Verdadeiro

datatype BooleanoDecimal = BooleanoDecimal(Booleano, Decimal)

datatype Option<T> = None | Some(T)

datatype BooleanoDigito = BooleanoDigito(Booleano, Digito) 

function method conversaoNatural(n: Natural): BooleanoDigito {
  match n {
    case Zero => BooleanoDigito(Falso, D0)
    case Sucessor(n1) => 
      match n1 {
        case Zero => BooleanoDigito(Falso, D1)
        case Sucessor(n2) =>
          match n2 {
            case Zero => BooleanoDigito(Falso, D2)
            case Sucessor(n3) =>
              match n3 {
                case Zero => BooleanoDigito(Falso, D3)
                case Sucessor(n4) =>
                  match n4 {
                    case Zero => BooleanoDigito(Falso, D4)
                    case Sucessor(n5) =>
                      match n5 {
                        case Zero => BooleanoDigito(Falso, D5)
                        case Sucessor(n6) =>
                          match n6 {
                            case Zero => BooleanoDigito(Falso, D6)
                            case Sucessor(n7) =>
                              match n7 {
                                case Zero => BooleanoDigito(Falso, D7)
                                case Sucessor(n8) =>
                                  match n8 {
                                    case Zero => BooleanoDigito(Falso, D8)
                                    case Sucessor(n9) =>
                                      match n9 {
                                        case Zero => BooleanoDigito(Falso, D9)
                                        case Sucessor(n') =>
                                          match conversaoNatural(n') {
                                            case BooleanoDigito(b, d) => BooleanoDigito(Verdadeiro, d)
                                          }
                                      }
                                  }                                                                                                                                           
                              }                                                                                                          
                          }                                                                             
                      }                                                    
                  }                               
              }              
          } 
      } 
  }
}

function method somaDecimalAux(cs: Decimal, ds: Decimal): Option<BooleanoDecimal> {
  match ds {
    case Constante(d) =>
      match cs {
        case Constante(c) =>
          match conversaoNatural(somaNatural(conversaoDigito(c), conversaoDigito(d))) {
            case BooleanoDigito(vaiUm, b) => Some(BooleanoDecimal(vaiUm, Constante(b))) 
          }
        case Coeficiente(c, cs') => None
      }
    case Coeficiente(d, ds') =>
      match cs {
        case Constante(c) => None
        case Coeficiente(c, cs') => 
          match somaDecimalAux(cs', ds') {
            case None => None
            case Some(BooleanoDecimal(vaiUm', bs')) =>
              match conversaoNatural(somaNatural(somaNatural(match vaiUm' case Falso => Zero case Verdadeiro => Sucessor(Zero), conversaoDigito(c)), conversaoDigito(d)))
                case BooleanoDigito(vaiUm, b) => Some(BooleanoDecimal(vaiUm, Coeficiente(b, bs')))
              }
          }
  }
}

function method somaDecimal(cs: Decimal, ds: Decimal): Option<Decimal>
  ensures 
    forall cs :: 
      forall ds :: 
        exists bs ::
          Some(bs) == somaDecimal(cs, ds) && 
          conversaoDecimal(bs) == somaNatural(conversaoDecimal(cs), conversaoDecimal(ds))  
{
  match somaDecimalAux(alinhamento(cs, ds), ds) {
    case None => None
    case Some(BooleanoDecimal(b, bs)) =>
      match b {
        case Falso => Some(bs)
        case Verdadeiro => Some(Coeficiente(D1, bs))
      }
  }
}  

method Main() {
  print somaDecimal(Coeficiente(D9, Constante(D9)), Coeficiente(D1, Constante(D2)));
}
Any help would be greately appreciated,
Saulo
Jan 29, 2016 at 1:16 PM
My experience is that Dafny usually finds the proof very quickly or not at all.

For correct lemmas:
  • Typical verification times for correct lemmas are less than 1 second.
  • Some lemmas do take longer to verify, perhaps up to 1 minute.
  • It is very rare for a lemma to take longer than 1 minute and still to eventually verify. (I suppose that Z3 has gone into a matching loop and will never make progress)
For incorrect lemmas:
  • Sometimes Dafny gives feedback quite quickly
  • Often it just goes forever (unless you have set a timeout)
  • There are some command line options that can sometimes get you feedback quicker, particularly the "keep going splits" options, which I understand will split the verification condition into parts, and try to verify each of the parts on its own, if the verification time exceeds the setting
Jan 29, 2016 at 1:21 PM
In your situation, what I would do is :
  1. use the annotation {:verify false} to disable verification on all of the functions.
  2. re-enable each function one at a time, until you find the one that has a problem
  3. try to fix that one by providing more detail of the proof
  4. carry on until all the verification is enabled again
Here is a version with verification disabled for each of the functions: http://rise4fun.com/Dafny/L6gu
datatype Natural = Zero | Sucessor(Natural)

function method {:verify false}  somaNatural(m: Natural, n: Natural): Natural {
  match n {
    case Zero => m
    case Sucessor(n') => Sucessor(somaNatural(m, n'))
  }
}

function method {:verify false}  produtoNatural(m: Natural, n: Natural): Natural {
  match n {
    case Zero => Zero
    case Sucessor(n') => somaNatural(m, produtoNatural(m, n'))
  }
} 

datatype Digito = D0 | D1 | D2 | D3 | D4 | D5 | D6 | D7 | D8 | D9

function method {:verify false}  conversaoDigito(d: Digito): Natural {
  match d {
    case D0 => Zero
    case D1 => Sucessor(Zero)
    case D2 => Sucessor(Sucessor(Zero))
    case D3 => Sucessor(Sucessor(Sucessor(Zero)))
    case D4 => Sucessor(Sucessor(Sucessor(Sucessor(Zero))))
    case D5 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))
    case D6 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero))))))
    case D7 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))
    case D8 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero))))))))
    case D9 => Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))
  }
}

datatype Decimal = Constante(Digito) | Coeficiente(Digito, Decimal)

datatype NaturalNatural = NaturalNatural(Natural, Natural)

function method {:verify false}  conversaoDecimalAux(ds: Decimal): NaturalNatural {
  match ds {
    case Constante(d) => NaturalNatural(conversaoDigito(d), Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))))
    case Coeficiente(d, ds') =>
      match conversaoDecimalAux(ds') {
        case NaturalNatural(n', p') =>
          NaturalNatural(somaNatural(conversaoDigito(d), n'), produtoNatural(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Sucessor(Zero)))))))))), p'))
      }
  }
}

function method {:verify false}  conversaoDecimal(ds: Decimal): Natural {
  match conversaoDecimalAux(ds) {
    case NaturalNatural(n, p) => n
  }
}

function method {:verify false}  alinhamentoAux(cs: Decimal, cs': Decimal, ds: Decimal): Decimal {
  match ds {
    case Constante(d) => cs
    case Coeficiente(d, ds') =>
      match cs' {
        case Constante(c') => Coeficiente(D0, alinhamentoAux(cs, cs', ds'))
        case Coeficiente(c', cs'') => alinhamentoAux(cs, cs'', ds') 
      } 
  }
}

function method {:verify false}  alinhamento(cs: Decimal, ds: Decimal): Decimal {
  alinhamentoAux(cs, cs, ds)
}

datatype Booleano = Falso | Verdadeiro

datatype BooleanoDecimal = BooleanoDecimal(Booleano, Decimal)

datatype Option<T> = None | Some(T)

datatype BooleanoDigito = BooleanoDigito(Booleano, Digito) 

function method {:verify false}  conversaoNatural(n: Natural): BooleanoDigito {
  match n {
    case Zero => BooleanoDigito(Falso, D0)
    case Sucessor(n1) => 
      match n1 {
        case Zero => BooleanoDigito(Falso, D1)
        case Sucessor(n2) =>
          match n2 {
            case Zero => BooleanoDigito(Falso, D2)
            case Sucessor(n3) =>
              match n3 {
                case Zero => BooleanoDigito(Falso, D3)
                case Sucessor(n4) =>
                  match n4 {
                    case Zero => BooleanoDigito(Falso, D4)
                    case Sucessor(n5) =>
                      match n5 {
                        case Zero => BooleanoDigito(Falso, D5)
                        case Sucessor(n6) =>
                          match n6 {
                            case Zero => BooleanoDigito(Falso, D6)
                            case Sucessor(n7) =>
                              match n7 {
                                case Zero => BooleanoDigito(Falso, D7)
                                case Sucessor(n8) =>
                                  match n8 {
                                    case Zero => BooleanoDigito(Falso, D8)
                                    case Sucessor(n9) =>
                                      match n9 {
                                        case Zero => BooleanoDigito(Falso, D9)
                                        case Sucessor(n') =>
                                          match conversaoNatural(n') {
                                            case BooleanoDigito(b, d) => BooleanoDigito(Verdadeiro, d)
                                          }
                                      }
                                  }                                                                                                                                           
                              }                                                                                                          
                          }                                                                             
                      }                                                    
                  }                               
              }              
          } 
      } 
  }
}

function method {:verify false}  somaDecimalAux(cs: Decimal, ds: Decimal): Option<BooleanoDecimal> {
  match ds {
    case Constante(d) =>
      match cs {
        case Constante(c) =>
          match conversaoNatural(somaNatural(conversaoDigito(c), conversaoDigito(d))) {
            case BooleanoDigito(vaiUm, b) => Some(BooleanoDecimal(vaiUm, Constante(b))) 
          }
        case Coeficiente(c, cs') => None
      }
    case Coeficiente(d, ds') =>
      match cs {
        case Constante(c) => None
        case Coeficiente(c, cs') => 
          match somaDecimalAux(cs', ds') {
            case None => None
            case Some(BooleanoDecimal(vaiUm', bs')) =>
              match conversaoNatural(somaNatural(somaNatural(match vaiUm' case Falso => Zero case Verdadeiro => Sucessor(Zero), conversaoDigito(c)), conversaoDigito(d)))
                case BooleanoDigito(vaiUm, b) => Some(BooleanoDecimal(vaiUm, Coeficiente(b, bs')))
              }
          }
  }
}

function method {:verify false}  somaDecimal(cs: Decimal, ds: Decimal): Option<Decimal>
  ensures 
    forall cs :: 
      forall ds :: 
        exists bs ::
          Some(bs) == somaDecimal(cs, ds) && 
          conversaoDecimal(bs) == somaNatural(conversaoDecimal(cs), conversaoDecimal(ds))  
{
  match somaDecimalAux(alinhamento(cs, ds), ds) {
    case None => None
    case Some(BooleanoDecimal(b, bs)) =>
      match b {
        case Falso => Some(bs)
        case Verdadeiro => Some(Coeficiente(D1, bs))
      }
  }
}  
 
method {:verify false} Main() {
  print somaDecimal(Coeficiente(D9, Constante(D9)), Coeficiente(D1, Constante(D2)));
}
Jan 29, 2016 at 1:31 PM
Your problem appears to relate to this function:
function method {:verify true}  somaDecimal(cs: Decimal, ds: Decimal): Option<Decimal>
  ensures 
    forall cs :: 
      forall ds :: 
        exists bs ::
          Some(bs) == somaDecimal(cs, ds) && 
          conversaoDecimal(bs) == somaNatural(conversaoDecimal(cs), conversaoDecimal(ds))  
{
  match somaDecimalAux(alinhamento(cs, ds), ds) {
    case None => None
    case Some(BooleanoDecimal(b, bs)) =>
      match b {
        case Falso => Some(bs)
        case Verdadeiro => Some(Coeficiente(D1, bs))
      }
  }
}
I think that the ensures clause does not mean what you intended it to. I'm not quite sure what it should mean, but it should probably be more like
datatype Option<T> = None | Some(val:T)
[...]
ensures somaDecimal(cs, ds).Some? ==> conversaoDecimal(somaDecimal(cs, ds).val) == somaNatural(conversaoDecimal(cs), conversaoDecimal(ds))
You can think of the parameters as being implicity universally quantified, so you don't need to quantify them again, The result of a function can be refered to in the postcondition by simply calling the function - i.e. somaDecimal(cs, ds) stands for the result of the function.
Jan 29, 2016 at 1:37 PM
Thanks a lot for your feedback lexicalscope! I did what you suggested, but since there is just one function with a ensures clause, this one function is exactly the one whose verification makes Dafny run forever. Since I have proved this theorem in Coq before, I think I am able to point Dafny in the right direction. However, I am wondering how one would proceed in the general case. Does Dafny gives us any helpful information of where it is stuck?
Jan 29, 2016 at 1:43 PM
Usually it is neccessary to set a timeout using the command line arguments. If you set a timeout then I think it should report which function it was trying to verify when the timeout occured. A suitable timeout may be 10seconds. You can see the available command line arguments by running dafny with the "/?" argument I think.
Jan 29, 2016 at 1:47 PM
Hi lexicalscope,

After your explanation that the parameters are implicitly universally quantified, I changed the ensures clause to
    exists bs ::
      Some(bs) == somaDecimal(cs, ds) &&
      conversaoDecimal(bs) == somaNatural(conversaoDecimal(cs), conversaoDecimal(ds))
Thanks to this change, dafny now ends running and says
/home/saulo/Desktop/decimal.dfy(148,16): Error BP5003: A postcondition might not hold on this return path.
/home/saulo/Desktop/decimal.dfy(150,4): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
    (0,0): anon13_Else
    (0,0): anon14_Then
    (0,0): anon12

Dafny program verifier finished with 11 verified, 1 error
It looks like Dafny does not agree that the postcondition is always true. Does Dafny explain why? Can it give an example of an input that makes the post condition false?
Jan 29, 2016 at 1:59 PM
If you are running Dafny in Visual Studio then it shows a red dot next to each of the verification failures. If you click the verification failure it shows you a trace that causes the verification failure.

If you are running it from the command line I am not sure how to acheive this. The basis of the process must be to ask Z3 to falsify the condition and then provide a model. Perhaps there are Dafny command line options that will cause Danfy to output such a model. Hopefully someone else will reply to the thread and tell us.

p.s. for your post condition to be valid you would have to know that somaDecimalAux(alinhamento(cs, ds), ds) never gives None. So I might try to prove a lemma like:
lemma somaDecimalAuxNotNone(cs: Decimal, ds: Decimal)
   ensures somaDecimalAux(alinhamento(cs, ds), ds).Some?
{
   // proof goes here
}
Jan 29, 2016 at 2:05 PM
Lexicalscope, I am really grateful for your help so far. Thanks a lot! Since I am running Dafny on Ubuntu, I am going to look for command line options that give the information that is readly available on VS. Also, I am going to review my code. Probably I introduced one or more bugs when porting it from Coq to Dafny.
Jan 29, 2016 at 2:13 PM
It could also be that Dafny is not able to prove the code without some extra lemmas provided by you. Just because the code is correct does not mean that Dafny can automatically prove that it is correct.

If you want to look at some examples of proofs in Dafny then there are many in the "test" directory in the source code https://dafny.codeplex.com/SourceControl/latest#Test/

I also have a few articles on my blog documenting some features and approaches I found useful:
http://www.lexicalscope.com/blog/category/dafny/