In the following code, Dafny fails to see the calc equality relationship holds, even though it follows directly from the statement of the lemma:

type uint32 = i:int | 0 <= i < 0x1_0000_0000

function last(s:seq):T
requires |s| > 0;
{
s[|s|-1]
}

function all_but_last(s:seq):seq
requires |s| > 0;
ensures |all_but_last(s)| == |s| - 1;
{
s[..|s|-1]
}

function ConcatenateSeqs(ss:seq<seq>) : seq
{
if |ss| == 0 then [] else ss[0] + ConcatenateSeqs(ss[1..])
}

lemma {:axiom} lemma_ReverseConcatenateSeqs(ss:seq<seq>)
requires |ss| > 0;
ensures ConcatenateSeqs(ss) == ConcatenateSeqs(all_but_last(ss)) + last(ss);

lemma Test(word_seqs:seq<seq>, words:seq)
{
var word_seqs' := word_seqs + [words];

calc {
    ConcatenateSeqs(word_seqs');
        { lemma_ReverseConcatenateSeqs(word_seqs'); }
    ConcatenateSeqs(all_but_last(word_seqs')) + last(word_seqs');
}

}

It's an error to export a function from a module if that function uses a type internal to the module. But doing this shouldn't cause Dafny to crash. Nevertheless, Dafny does crash when given this buggy code:

module m1 {
export reveals f
type T = int
function f(x:T) : T { x }
}

The program

class System { }

verifies fine, but it compiles into C# code that doesn't compile. The problem seems to be related to the fact that the class is called System.

Through a combination of trigger selection and predicate expansion for error reporting, the following 77-line Dafny file produces a 1.6 million-line Boogie file. The good thing is that it still verifies, but this still seems like a place where we might eventually want to do something more efficient.

type sp_state
type operand = int

function sp_op_const(c:int) : int { c }

predicate {:opaque} InBounds(s:sp_state, o:operand, v:int)
{
    0 <= o < 0x1_0000_0000
}

lemma lemma_K_InBounds()
    ensures forall s:sp_state :: 
                InBounds(s, sp_op_const(0x428a2f98), 0x428a2f98) &&
                InBounds(s, sp_op_const(0x71374491), 0x71374491) &&
                InBounds(s, sp_op_const(0xb5c0fbcf), 0xb5c0fbcf) &&
                InBounds(s, sp_op_const(0xe9b5dba5), 0xe9b5dba5) &&
                InBounds(s, sp_op_const(0x3956c25b), 0x3956c25b) &&
                InBounds(s, sp_op_const(0x59f111f1), 0x59f111f1) &&
                InBounds(s, sp_op_const(0x923f82a4), 0x923f82a4) &&
                InBounds(s, sp_op_const(0xab1c5ed5), 0xab1c5ed5) &&
                InBounds(s, sp_op_const(0xd807aa98), 0xd807aa98) &&
                InBounds(s, sp_op_const(0x12835b01), 0x12835b01) &&
                InBounds(s, sp_op_const(0x243185be), 0x243185be) &&
                InBounds(s, sp_op_const(0x550c7dc3), 0x550c7dc3) &&
                InBounds(s, sp_op_const(0x72be5d74), 0x72be5d74) &&
                InBounds(s, sp_op_const(0x80deb1fe), 0x80deb1fe) &&
                InBounds(s, sp_op_const(0x9bdc06a7), 0x9bdc06a7) &&
                InBounds(s, sp_op_const(0xc19bf174), 0xc19bf174) &&
                InBounds(s, sp_op_const(0xe49b69c1), 0xe49b69c1) &&
                InBounds(s, sp_op_const(0xefbe4786), 0xefbe4786) &&
                InBounds(s, sp_op_const(0x0fc19dc6), 0x0fc19dc6) &&
                InBounds(s, sp_op_const(0x240ca1cc), 0x240ca1cc) &&
                InBounds(s, sp_op_const(0x2de92c6f), 0x2de92c6f) &&
                InBounds(s, sp_op_const(0x4a7484aa), 0x4a7484aa) &&
                InBounds(s, sp_op_const(0x5cb0a9dc), 0x5cb0a9dc) &&
                InBounds(s, sp_op_const(0x76f988da), 0x76f988da) &&
                InBounds(s, sp_op_const(0x983e5152), 0x983e5152) &&
                InBounds(s, sp_op_const(0xa831c66d), 0xa831c66d) &&
                InBounds(s, sp_op_const(0xb00327c8), 0xb00327c8) &&
                InBounds(s, sp_op_const(0xbf597fc7), 0xbf597fc7) &&
                InBounds(s, sp_op_const(0xc6e00bf3), 0xc6e00bf3) &&
                InBounds(s, sp_op_const(0xd5a79147), 0xd5a79147) &&
                InBounds(s, sp_op_const(0x06ca6351), 0x06ca6351) &&
                InBounds(s, sp_op_const(0x14292967), 0x14292967) &&
                InBounds(s, sp_op_const(0x27b70a85), 0x27b70a85) &&
                InBounds(s, sp_op_const(0x2e1b2138), 0x2e1b2138) &&
                InBounds(s, sp_op_const(0x4d2c6dfc), 0x4d2c6dfc) &&
                InBounds(s, sp_op_const(0x53380d13), 0x53380d13) &&
                InBounds(s, sp_op_const(0x650a7354), 0x650a7354) &&
                InBounds(s, sp_op_const(0x766a0abb), 0x766a0abb) &&
                InBounds(s, sp_op_const(0x81c2c92e), 0x81c2c92e) &&
                InBounds(s, sp_op_const(0x92722c85), 0x92722c85) &&
                InBounds(s, sp_op_const(0xa2bfe8a1), 0xa2bfe8a1) &&
                InBounds(s, sp_op_const(0xa81a664b), 0xa81a664b) &&
                InBounds(s, sp_op_const(0xc24b8b70), 0xc24b8b70) &&
                InBounds(s, sp_op_const(0xc76c51a3), 0xc76c51a3) &&
                InBounds(s, sp_op_const(0xd192e819), 0xd192e819) &&
                InBounds(s, sp_op_const(0xd6990624), 0xd6990624) &&
                InBounds(s, sp_op_const(0xf40e3585), 0xf40e3585) &&
                InBounds(s, sp_op_const(0x106aa070), 0x106aa070) &&
                InBounds(s, sp_op_const(0x19a4c116), 0x19a4c116) &&
                InBounds(s, sp_op_const(0x1e376c08), 0x1e376c08) &&
                InBounds(s, sp_op_const(0x2748774c), 0x2748774c) &&
                InBounds(s, sp_op_const(0x34b0bcb5), 0x34b0bcb5) &&
                InBounds(s, sp_op_const(0x391c0cb3), 0x391c0cb3) &&
                InBounds(s, sp_op_const(0x4ed8aa4a), 0x4ed8aa4a) &&
                InBounds(s, sp_op_const(0x5b9cca4f), 0x5b9cca4f) &&
                InBounds(s, sp_op_const(0x682e6ff3), 0x682e6ff3) &&
                InBounds(s, sp_op_const(0x748f82ee), 0x748f82ee) &&
                InBounds(s, sp_op_const(0x78a5636f), 0x78a5636f) &&
                InBounds(s, sp_op_const(0x84c87814), 0x84c87814) &&
                InBounds(s, sp_op_const(0x8cc70208), 0x8cc70208) &&
                InBounds(s, sp_op_const(0x90befffa), 0x90befffa) &&
                InBounds(s, sp_op_const(0xa4506ceb), 0xa4506ceb) &&
                InBounds(s, sp_op_const(0xbef9a3f7), 0xbef9a3f7) &&
                InBounds(s, sp_op_const(0xc67178f2), 0xc67178f2) 
{ reveal_InBounds(); }

Dafny crashes in Translator.FuelSetting.GetFunctionFuel when verifying the code below:

datatype T = T(n:int)

function ToInt(t:T) : int
    ensures ToInt(t) == int(t.n);
{
    int(t.n)
}

method Test()
{
    assert exists p:int :: exists t:T :: ToInt(t) > 0;
}

The following dafny program produces a compiler error.

module A {
  export E {G}
  method G(x: int) returns (y : int) { y := 0; }
}

module B {
  import A.E

  method Main() {
    var two := A.G(2);
  }
}

Produces the error error CS0103: The name '_1_A' does not exist in the current context

I believe this is a result of an issue with the Cloner where the module is cloned before compiling, but does not clone the signatures of its imports, resulting in stale references to modules that have not been compiled (i.e. we're looking for _1_A here when we have actually compiled _1_A_Compile).

The following program:

predicate bad()
{
    forall i :: i in {1}
}

Fails in Dafny 1.9.7 with the following errors:

Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
(0,-1): Error: equality is not allowed in triggers
10 name resolution errors detected in C:\cygwin64\tmp\test.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

C:\cygwin64\tmp\test.bpl(1719,37): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1721,40): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1729,37): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1731,40): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1738,37): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1740,40): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1747,37): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1749,40): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1780,32): Error: equality is not allowed in triggers
C:\cygwin64\tmp\test.bpl(1781,41): Error: equality is not allowed in triggers
10 name resolution errors detected in C:\cygwin64\tmp\test.bpl

I use the Visual Studio extension a lot, and I was excited to have the ability to start and stop verification using F5. However, it's not as useful as I'd hoped it would be, because every time I use it it seems to throw away the cache of verification results! I'd find it useful if this weren't the case.

The common scenario I find myself in is:

1. I make some changes to a lemma, and the plugin starts verifying them.
2. While it's in the middle of verification, I realize I have a bug in the changes I just made and I make some more changes to fix that bug.
3. I hit F5 to say, "Stop verifying now, because I know you're going to fail."
4. I hit F5 to say, "Start verifying again, because I've made changes that will help you succeed."

But, all the savings I was hoping to get by stopping its futile attempt at verification are moot, because it threw away cache results for the entire file. So instead of saving a few seconds of futile verification time, I actually lose minutes of time by having to re-verify the entire file.

Dafny fails to determine that set s in this code segment is finite.

datatype OUTER = b(x:INNER)

lemma l()
{
    var s := set r : OUTER | true;
}

Boogie supports both const declarations and function declarations:

const c:int; axiom c == 3;
function f(i:int):int { i + 1 }

Dafny doesn't have const declarations, which means you have to write c as a zero-argument function:

function c():int { 3 }
function f(i:int):int { i + 1 }

It would be nice to be able to write something like:

const c:int { 3 }
const c:int := 3
const c:int = 3

and then refer to c in the rest of the program as "c", not "c()".

The third lemma doesn't verify:

lemma lemma_Subset_Cardinalities<I>(a : set<I>, b : set<I>)
    ensures a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
{
    if (a <= b) {
        if x :| x in a {
            assert x in b;
            lemma_Subset_Cardinalities(a - {x}, b - {x});
        }
        else {
            assert a == {};
            assert |b - a| == |b| == |b| - |a|;
        }
    }
}

predicate pred_lemma_Subset_Cardinalities<I>(a : set<I>, b : set<I>) 
    ensures a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
    ensures pred_lemma_Subset_Cardinalities(a, b) 
{
    lemma_Subset_Cardinalities(a, b);
    true
}

lemma lemma_Subset_Cardinalities_Universal<I>()
    ensures forall a : set<I>, b : set<I> :: a <= b ==> pred_lemma_Subset_Cardinalities(a, b) && |a| <= |b| && |b - a| == |b| - |a|
{
}

while function lemma in body is still working in 1.9.8:

lemma lemma_Subset_Cardinalities_Universal<I>()
    ensures forall a : set<I>, b : set<I> :: a <= b ==> |a| <= |b| && |b - a| == |b| - |a|
{
    if a : set<I>, b : set<I> :| a <= b && !(|a| <= |b| && |b - a| == |b| - |a|) {
        assert pred_lemma_Subset_Cardinalities(a, b);
    }
}

In the attached example, where test1.dfy declares a module and test2.dfy includes test1.dfy, Dafny crashes due to an unhandled exception. The output is below.

test1.dfy.txt
test2.dfy.txt

Unhandled Exception: System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.Resolver.CheckTypeInference_Visitor.CheckTypeIsDetermined(IToken tok, Type t, String what) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 4503
at Microsoft.Dafny.Resolver.CheckTypeInference_Visitor.VisitOneExpr(Expression expr) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 4465
at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9602
at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable1 coll, Action1 fn) in f:\Apps\codeplex\boogie\Source\Core\Util.cs:line 62
at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9596
at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable1 coll, Action1 fn) in f:\Apps\codeplex\boogie\Source\Core\Util.cs:line 62
at Microsoft.Dafny.BottomUpVisitor.Visit(Statement stmt) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9607
at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable1 coll, Action1 fn) in f:\Apps\codeplex\boogie\Source\Core\Util.cs:line 62
at Microsoft.Dafny.BottomUpVisitor.Visit(Statement stmt) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9608
at Microsoft.Dafny.Resolver.CheckTypeInference(Statement stmt, ICodeContext codeContext) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 4309
at Microsoft.Dafny.Resolver.CheckTypeInference_Member(MemberDecl member) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 4254
at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List1 declarations, Graph1 datatypeDependencies, Graph1 codatatypeDependencies) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 2101 at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 822 at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 361 at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in f:\Apps\dafny.git\Source\Dafny\DafnyMain.cs:line 147 at Microsoft.Dafny.Main.ParseCheck(IList1 files, String programName, ErrorReporter reporter, Program& program) in f:\Apps\dafny.git\Source\Dafny\DafnyMain.cs:line 96
at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in f:\Apps\dafny.git\Source\DafnyDriver\DafnyDriver.cs:line 174
at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in f:\Apps\dafny.git\Source\DafnyDriver\DafnyDriver.cs:line 59
at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1.

The {:prependAssertToken} attribute is only used internally in Dafny, so its name should start with a leading underscore (so as not to conflict with user-defined attributes).

If you include a file that's longer than the including file, the Dafny extension will often crash. Here's a small example. Create two files:

includer.dfy:

include "includee.dfy"

method test()

and includee.dfy:

function TestFunc(x:int) : int
{
    x + 2
}

lemma SomeProperties(y:int)
    ensures TestFunc(y) > y;
{

}

This will crash the extension. The problem is that the code that tries to add "Go to definition" functionality doesn't check whether the expression it's trying to tag is in the current buffer/file. In this case, it sees TestFunc in the ensures to SomeProperties, and tries to add a tag to the current snapshot, which fails with an out of range error.

The current master branch of Dafny crashes in an assertion failure when verifying the program below:

predicate {:opaque} ValidRegs(regs:map<int,int>)
{
    forall r:int :: 0 <= r < 10 ==> r in regs
}

predicate mypredicate(regs:map<int,int>)
    requires ValidRegs(regs)

lemma mylemma()
{
    var regs:map<int,int>;
    assume mypredicate(regs);
}

Dafny will correctly rule out the following bad type synonyms; they're equi-recursive, and should not be permitted:

type Bad = set<Bad>
type Bad = (Bad, Bad)
type Bad = map<Bad, Bad>

However, Dafny seems not to detect cycles deeper than one level of nesting; the following type synonyms are all accepted:

type Bad = set<set<Bad>>
type Bad = seq<(Bad, Bad)>
type Bad = map<int, set<Bad>>

...and so on.

Any of these will cause a fatal crash in the Dafny verification process whenever Bad is mentioned. For instance, any of the above type synonyms, when paired with the below definition, crash Dafny:

predicate UhOh(bad: Bad)

It seems that the syntactic occurs check only looks one level deep; it should recursively descend the structure of the type.

The following function:

function BitsAsInt(b:bv32): int
    ensures 0 <= BitsAsInt(b) < 0x1_0000_0000
{
    b as int
}

Causes an assertion failure in the latest Dafny:

(Very similar to issue #26.)

Dafny verifies the following program, but generates invalid code.

datatype bar = Bar
datatype obj = Obj(fooBar:map<foo,bar>)
datatype foo = Foo

method test_case() returns (o:obj)
{
    if true {
        o:= o.(fooBar := o.fooBar[Foo := Bar]);
    }
}

The compilation error generated is:

error CS0136: A local variable named '_pat_let_tv1' cannot be declared in this scope because it would give a different meaning to '_pat_let_tv1', which is already used in a 'parent or current' scope to denote something else

The segment of the generated code causing this error is:

public static void @test__case(out @obj @o)
  {
    @o = new @obj();
  TAIL_CALL_START: ;
    var @_pat_let_tv1= @o;
    if (true)
    {
      var @_pat_let_tv1= @o;
      @o = Dafny.Helpers.Let<@obj,@obj>(@o, _pat_let0_0 => Dafny.Helpers.Let<@obj,@obj>(_pat_let0_0, @_2_dt__update__tmp_h0 => new @obj(new obj_Obj(((@_pat_let_tv1).@dtor_fooBar).Update(new @foo(new foo_Foo()), new @bar(new bar_Bar()))))));
    }
  }

If the if statement is removed, code generation is correct.

Dafny generally gets the exit status correct for verification, but some invocations that emit an error message incorrectly return an exit status of zero. This is a minor bug, but still isn't good for a parent build system.

For example, in both of these cases Dafny has clearly failed (at a different stage) and printed an error message, but it returned a zero exit status:

% Dafny.exe /noNLarith /timeLimit:60 /trace /compile:0 main.i.dfy
[TRACE] Using prover: C:\Users\baumann\src\spartan\tools\Mindy\Binaries\z3.exe
Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
Parsing main.i.dfy
smc_handler.gen.dfy(1499,7): Error: more than one declaration of function/procedure name: CheckWellformed$$_.Main
smc_handler.gen.dfy(1499,7): Error: more than one declaration of function/procedure name: IntraModuleCall$$_.Main
2 name resolution errors detected in C:\cygwin64\tmp\main.i.bpl

*** Encountered internal translation error - re-running Boogie to get better debug information

C:\cygwin64\tmp\main.i.bpl(6013,10): Error: more than one declaration of function/procedure name: CheckWellformed$$_.Main
C:\cygwin64\tmp\main.i.bpl(6018,10): Error: more than one declaration of function/procedure name: IntraModuleCall$$_.Main
2 name resolution errors detected in C:\cygwin64\tmp\main.i.bpl

% Dafny.exe /trace /noVerify /compile:2 /out:main.exe main.i.dfy
[TRACE] Using prover: C:\Users\baumann\src\spartan\tools\Mindy\Dafny\z3.exe
Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.
Parsing main.i.dfy
Coalescing blocks...
Inlining...

Running abstract interpretation...
  [0.0624617 s]

Dafny program verifier finished with 0 verified, 0 errors
Compilation error: an assume statement cannot be compiled (line 188)
Compilation error: an assume statement cannot be compiled (line 235)

As reported in boogie-org/boogie-friends#8, the Emacs mode for Dafny does not report errors when they appear in an included file, which leads to the appearance of correct verification for all type-correct files which import type-incorrect files.

One solution to this is to enable the Dafny compiler to report errors in included files when typechecking/verifying/compiling the including files. We could localize this reported error to the line of the pertinent include statement to indicate to the user what has gone wrong.

This issue does not exist in Visual Studio; however, it does not seem like such a bad thing to produce an error annotation on the include statement saying "errors exist in this included file," even if those errors are reported from within their own file. Indeed, this would clarify for the user why it is that this file is refusing to verify, should they forget that they had included the file whose errors are being reported.

I suggest the following format for the error message: If there are errors in an included file A.dfy, and we have B.dfy with a line include "A.dfy", let Dafny say: B.dfy(<line>,<col>): Error: the included file "A.dfy" contains error(s)." I don't think we wish to report all of A.dfy's potentially many errors here; it is best, I would guess, to merely point the user toward A.dfy so that they can investigate these errors within the context of that file.

What do you think about this solution, @RustanLeino and @cpitclaudel?

It was decided that ExistentialGuards should be named BindingGuards. That change has been made in the Dafny reference manual but has not yet been made in the Dafny source code.

The following program:

datatype Maybe = Nothing | Just
predicate bad(e:Maybe)
{
    forall i :: 0 <= i < 1 ==>
        0 == match e
            case Nothing => 0
            case Just => 0
}

Crashes Dafny for Windows v1.9.7 with the following backtrace:

Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft.

Unhandled Exception: System.NullReferenceException: Object reference not set to
an instance of an object.
   at Microsoft.Dafny.Resolver.FreeVariables(Expression expr) in c:\dafny-public\Source\Dafny\Resolver.cs:line 10376
   at Microsoft.Dafny.Resolver.SanitizeForBoundDiscovery[VT](List`1 boundVars, Int32 bvi, ResolvedOpcode op, List`1 knownBounds, Expression& e0, Expression& e1) in c:\dafny-public\Source\Dafny\Resolver.cs:line 10130
   at Microsoft.Dafny.Resolver.DiscoverAllBounds_Aux_SingleVar[VT](List`1 bvars, Int32 j, Expression expr, Boolean polarity, List`1 knownBounds) in c:\dafny-public\Source\Dafny\Resolver.cs:line 10019
   at Microsoft.Dafny.Resolver.DiscoverAllBounds_Aux_MultipleVars[VT](List`1 bvars, Expression expr, Boolean polarity, List`1 knownBounds) in c:\dafny-public\Source\Dafny\Resolver.cs:line 9981
   at Microsoft.Dafny.Resolver.DiscoverBestBounds_MultipleVars[VT](List`1 bvars, Expression expr, Boolean polarity, Boolean onlyFiniteBounds, List`1& missingBounds) in c:\dafny-public\Source\Dafny\Resolver.cs:line 9944
   at Microsoft.Dafny.Resolver.CheckTypeInference_Visitor.VisitOneExpr(Expression expr) in c:\dafny-public\Source\Dafny\Resolver.cs:line 2444
   at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) in c:\dafny-public\Source\Dafny\DafnyAst.cs:line 8221
   at Microsoft.Dafny.Resolver.CheckTypeInference(Expression expr, ICodeContext
codeContext) in c:\dafny-public\Source\Dafny\Resolver.cs:line 2356
   at Microsoft.Dafny.Resolver.CheckTypeInference_Member(MemberDecl member) in c:\dafny-public\Source\Dafny\Resolver.cs:line 2318
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies) in c:\dafny-public\Source\Dafny\Resolver.cs:line 1685
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig) in c:\dafny-public\Source\Dafny\Resolver.cs:line 725
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in c:\dafny-public\Source\Dafny\Resolver.cs:line 326
   at Microsoft.Dafny.Main.ParseCheck(IList`1 fileNames, String programName, ErrorReporter reporter, Program& program) in c:\dafny-public\Source\Dafny\DafnyMain.cs:line 70
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFileNames, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in c:\dafny-public\Source\DafnyDriver\DafnyDriver.cs:line 174
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in c:\dafny-public\Source\DafnyDriver\DafnyDriver.cs:line 106
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1.<Main>b__0() in c:\dafny-public\Source\DafnyDriver\DafnyDriver.cs:line 34
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state, Boolean preserveSyncCtx)
   at System.Threading.ExecutionContext.Run(ExecutionContext executionContext, ContextCallback callback, Object state, Boolean preserveSyncCtx)
   at System.Threading.ExecutionContext.Run(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.ThreadHelper.ThreadStart()

Export sets are a convenient way to hide internal types from users of a module. However, they don't seem to hide it from whatever part of Dafny is checking for type resolution ambiguity. In the example below, Dafny complains, when T is used by function g, that T is ambiguous: it can't tell if it's cm1.T or cm2.T. However, due to the restrictive export set on cm1 that excludes T, it should be clear that T refers only to cm2.T.

As a demonstration that cm1.T should be hidden from those importing cm1, I have in my example code another module m that imports cm1 the same way. There, Dafny correctly complains when the function h tries to refer to the (locally non-existent) type T.

This is the incorrect error message generated by Dafny:

test1.dfy(19,17): Error: The name T ambiguously refers to a type in one of the modules _4_cm2_Compile, _0_cm1_Compile (try qualifying the type name with the module name)

This is the correct error message generated by Dafny:

test1.dfy(25,17): Error: Undeclared top-level type or type parameter: T (did you forget to qualify a name or declare a module import 'opened?')

This is the code that caused the above two error messages to be generated:

module am {
type T
}

module cm1 refines am {
export reveals f

type T = int

function f(i:int) : int { i }

}

module cm2 refines am {

import opened cm1

type T = bool

function g(b:T) : T { !b } // Error incorrectly reported here

}

module m {

import opened cm1
function h(t:T) : int { t + 1 } // Error correctly reported here

}

The following Lemma fails to prove in Dafny 1.9.8:

lemma mylemma()
{
    var shift:int := 1;
    assume (1 as bv32 << shift) as int == 2;
    assert (1 as bv32 << 1) as int == 2;
}

The proximate cause appears to be a missing LitInt() call in the version with the literal, as seen in the translated Boogie code:

    var shift#0: int;
    shift#0 := LitInt(1);
    assume nat_from_bv32(LeftShift_bv32(nat_to_bv32(LitInt(1)), nat_to_bv32(shift#0)))
   == LitInt(2);
    assert nat_from_bv32(LeftShift_bv32(nat_to_bv32(LitInt(1)), nat_to_bv32(1)))
   == LitInt(2);

I suspect, but haven't confirmed, that this issue isn't unique to <<.

Opening a file with a deep nested function in Visual Studio causes the Dafny extension to hang. Here's an example:

datatype List = Cons(hd:int, tl:List) | Nil

function DeepFunction() : List
{
Cons(32,Cons(31,Cons(30,Cons(29,Cons(28,Cons(27,Cons(26,Cons(25,Cons(24,Cons(23,Cons(22,Cons(21,Cons(20,Cons(19,Cons(18,Cons(17,Cons(16,Cons(15,Cons(14,Cons(13,Cons(12,Cons(11,Cons(10,Cons(9,Cons(8,Cons(7,Cons(6,Cons(5,Cons(4,Cons(3,Cons(2,Cons(1, Nil))))))))))))))))))))))))))))))))
}

Breaking into the debugger while this is happening reveals the cause to be a call to ExprRegions that happens in ComputeIdentifierRegions. It appears that because the expression corresponding to each Cons is an ApplySuffix, ExprRegions is called both on its Lhs and on each of its subexpressions. But, since the Lhs is itself a subexpression, each call to ExprRegions causes two invocations of ExprRegions. Thus, in a 32-deep function, we get 2^32 calls to ExprRegions.

I believe the fix is just to comment out the following lines in ExprRegions:

  } else if (expr is ApplySuffix) {

/* I propose cutting these because the Lhs will be visited by the for loop below
var e = (ApplySuffix)expr;
if (e.Lhs != null) {
ExprRegions(e.Lhs, regions, prog, module);
}
*/
} else if (expr is LetExpr) {

Dafny methods have named return values, while Dafny function return values are anonymous:

method m(x:int, y:int) returns(z:int)
function f(x:int, y:int):int

This is nice and concise when you never have to refer to the return value by name. But sometimes you need to refer to the return value in an ensures clause. Currently, this is done by referring to the whole function call applied to its arguments:

method m(x:int, y:int) returns(z:int)
  ensures z >= 10
  ensures isEven(z)

function f(x:int, y:int):int
  ensures f(x, y) >= 10
  ensures isEven(f(x, y))

There are two issues with writing a call like "f(x, y)" in ensures clauses. First, the call is often very long to write -- not just "f(x, y)", but "myverylongfunctionname(myverylongargument1, myverylongargument2, myverylongargument3)". This can be mitigated somewhat by binding the return value to a shorter name using a "var" (let) expression, but this doesn't work across multiple ensures clauses. Second, when Dafny sees the function call "f(x, y)" in an ensures clause, it tags the function as recursive, which brings in extra machinery for layers and fuel.

These two issues could be solved independently. But both issues could be solved together with an optional named return value, something like:

function f(x:int, y:int):(z:int)
function f(x:int, y:int) returns(z:int)
function f(x:int, y:int)->z:int

Boogie, for example, already supports optional named return values from functions.

The following code defines an opaque predicate p and never reveals p, but it still manages to prove something that should only be provable if p is revealed:

predicate {:opaque} p(i:int)
{
  i == 3
}

predicate {:opaque} q(x:int)
  requires p(x)
  ensures  p(x)
{
  true
}

lemma L(x:int)
  requires p(x)
{
  reveal_q();
  assert q(x);
  assert x == 3; // succeeds; should fail
}

I think the consequence axiom for q unintentionally reveals p by using q's fuel ($ly) instead of the start fuel for p:

// consequence axiom for _module.__default.q
axiom 0 < $ModuleContextHeight
     || (0 == $ModuleContextHeight && 1 <= $FunctionContextHeight)
   ==> (forall $ly: LayerType, $Heap: Heap, x#0: int :: 
    { _module.__default.q($ly, $Heap, x#0) } 
    _module.__default.q#canCall($Heap, x#0)
         || ((0 != $ModuleContextHeight || 1 != $FunctionContextHeight)
           && $IsGoodHeap($Heap)
           && _module.__default.p($ly, $Heap, x#0))
       ==> _module.__default.p($ly, $Heap, x#0));

Dafny checks that every pointer that is dereferenced, or is passed to a routine that may dereference it, is allocated. This usually holds, except possibly inside old expressions. Dafny lays down such checks inside old expressions, but apparently it's missing the checks for lemmas that are called inside expressions.

The code below gives test cases. Lines marked with "error" should report an error, and Dafny does this correctly. Lines with no markings should report no error, and Dafny does this correctly. Lines marked with "BUG" should report an error for the value passed to a lemma, but Dafny currently does not report any error -- this is the bug.

class C {
  var next: C
  var x: int
}

function F(c: C): int
  requires c != null
  reads c
{
  c.x
}

twostate function G(a: C, new b: C): int
  requires a != null && b != null
  reads b
{
  old(a.x) + b.x
}

lemma L(c: C)
{ }

twostate lemma K(a: C, new B: C)
{ }

method M0(p: C)
  requires p != null
{
  var c, d := new C, new C;
  ghost var x;
  if
  case true =>
    x := F(c);
  case true =>
    x := old(F(c));  // error
  case true =>
    x := old(L(  // BUG: should check L's parameter to be allocated in the old state
               if F(d) == 10 then c else c  // error
             ); 5);
  case true =>
    x := old(L(  // BUG: should check L's parameter to be allocated in the old state
               if F(p) == 10 then c else c
             ); 5);
  case true =>
    x := old(L(c); 5);  // BUG: should check L's parameter to be allocated in the old state
  }
method M1(p: C)
  requires p != null
{
  var c := new C;
  ghost var x;
  if
  case true =>
    x := old(assert F(c) == 5; 5);  // error
  case true =>
    x := old(calc {
               5;
               { L(c); }  // BUG: should check L's parameter to be allocated in the old state
               5;
               F(c);  // error
             }
             10);
}
method M2(p: C)
  requires p != null
{
  var c := new C;
  ghost var x;
  if
  case true =>
    x := (K(c, c); 5);  // error
  case true =>
    x := (K(p, c); 5);
  case true =>
    x := c.x;
  case true =>
    x := old(c.x);  // error
  case true =>
    x := G(p, c);
  case true =>
    x := G(c, c);  // error
}

In the example below, I get "Error: value does not satisfy the subset constraints of 'array'" when I try to pass an array of uint32s (a subset type) to a function (ArrayIdentity) that is generic over array types. Oddly, it works when I do the same test with sequences or if the entire array is treated as the generic type (e.g., when calling Identity).

function Identity<T>(a:T) : T
{
  a
}

function SeqIdentity<T>(s:seq<T>) : seq<T>
{
    s
}

function ArrayIdentity<T>(a:array<T>) : array<T>
{
    a
}

type uint32 = i : int | 0 <= i < 0x1_0000_0000

lemma test()
{
    var x:uint32;
    var g := Identity(x);     // Works

    var s:seq<uint32>;
    var s' := Identity(s);      // Works
    var s'' := SeqIdentity(s);  // Works

    var a:array<uint32>;
    var a' := Identity(a);    // Works
    var a'' := ArrayIdentity(a);  // Error    
}

In this example:
`method M() {
ghost var h := var ta := F(); 5;
var j := ghost var tb := F(); 5;
assert h == j;
}

function F(): int { 5 }
`
The printer omits both "ghost" keywords, which throws an error when re-parsing.
Added relevant test in 021226d

Dafny's char type predates the newtype facility and is very limited compared to newtypes. It would be useful if char behaved more like a newtype. For example, this would allow programmers to convert between char types and other integral types, which would help when writing parsers and printers that convert between strings and integers. For example, with newtypes, you can write:

newtype mychar = x:int | 0 <= x < 0x10000

function method digitAsChar(i:int):mychar
  requires 0 <= i < 10
{
  mychar(48 + i)
}

This is difficult to do with the current char type.

The latest Dafny fails to prove:

function SeqRepeat<T>(count:nat, elt:T) : seq<T>
    ensures |SeqRepeat<T>(count, elt)| == count
    ensures forall i :: 0 <= i < count ==> SeqRepeat<T>(count, elt)[i] == elt

datatype Maybe<T> = Nothing | Just(v: T)
type Num = x | 0 <= x < 10
datatype D = C(seq<Maybe<Num>>)

lemma test()
{
    ghost var s := SeqRepeat(1, Nothing);
    ghost var e := C(s);
    assert e == C(SeqRepeat(1, Nothing));
}

This also fails with the older Z3.

The following program causes Dafny to crash:

module Library {
}

module Outer {
  import Library

  module Inner {
    import Library
  }
}

Here's the output:

> dafny SigCrash.dfy
Dafny program verifier version 1.9.8.30829, Copyright (c) 2003-2016, Microsoft.

Unhandled Exception: System.Diagnostics.Contracts.__ContractsRuntime+ContractException: Precondition failed: Signature != null
   at System.Diagnostics.Contracts.__ContractsRuntime.TriggerFailure(ContractFailureKind kind, String msg, String userMessage, String conditionTxt, Exception inner) in c:\dafny\Source\Dafny\DafnyAst.cs:line 0
   at System.Diagnostics.Contracts.__ContractsRuntime.ReportFailure(ContractFailureKind kind, String msg, String conditionTxt, Exception inner) in c:\dafny\Source\Dafny\DafnyAst.cs:line 0
   at System.Diagnostics.Contracts.__ContractsRuntime.Requires(Boolean condition, String msg, String conditionTxt) in c:\dafny\Source\Dafny\DafnyAst.cs:line 0
   at Microsoft.Dafny.ModuleDecl.AccessibleSignature() in c:\dafny\Source\Dafny\DafnyAst.cs:line 2574
   at Microsoft.Dafny.Resolver.ResolveExport(ModuleDecl root, ModuleDefinition parent, List`1 Path, List`1 Exports, ModuleSignature& p, ErrorReporter reporter) in c:\dafny\Source\Dafny\Resolver.cs:line 1809
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in c:\dafny\Source\Dafny\Resolver.cs:line 423
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in c:\dafny\Source\Dafny\DafnyMain.cs:line 147
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in c:\dafny\Source\Dafny\DafnyMain.cs:line 96
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in c:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 174
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in c:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 59
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1.<Main>b__0() in c:\dafny\Source\DafnyDriver\DafnyDriver.cs:line 36
   at System.Threading.ExecutionContext.RunInternal(ExecutionContext executionContext, ContextCallback callback, Object state, Boolean preserveSyncCtx)
   at System.Threading.ExecutionContext.Run(ExecutionContext executionContext, ContextCallback callback, Object state, Boolean preserveSyncCtx)
   at System.Threading.ExecutionContext.Run(ExecutionContext executionContext, ContextCallback callback, Object state)
   at System.Threading.ThreadHelper.ThreadStart()

Curiously, if one or both of the imports is renamed, even if both are renamed in the same way, the crash does not occur. For example, the program

module Library {
}

module Outer {
  import L = Library

  module Inner {
    import L = Library
  }
}

does not cause any crash.

Rustan

The CaseStatement and CaseExpression grammar currently has the following
(in Dafny.atg):

  "case"                      (. x = t; .)
  ( ...
  | "("
      CasePattern<out pat>        (. arguments.Add(pat); .)
      { "," CasePattern<out pat>  (. arguments.Add(pat); .)   }
    ")"

This does not allow to match an empty tuple. It should be:

  "case"                      (. x = t; .)
  ( ...
  | "("
      [ 
         CasePattern<out pat>        (. arguments.Add(pat); .)
         { "," CasePattern<out pat>  (. arguments.Add(pat); .)  }
      ]
    ")"

If C is a heap-related type (such as a class), then there are restrictions on expressions "forall x:C :: ..." to prohibit quantifying over objects x that aren't yet allocated. However, these restrictions aren't always enforced for type variables T that might later be instantiated with C. In the example below, the function AllP quantifies over all x of type T, even though T is later instantiated with C. Then AllP's frame axiom is used (in M3) to prove something that is not provable directly (as seen in M2). Rustan and I discussed this and tentatively proposed that the rules for quantifying over type variables T should be tightened, unless the programmer annotates T to indicate that T can never be instantiated with a heap-related type.

predicate P<T>(x:T)

predicate AllP<T>() { forall x :: P<T>(x) }

class C {}

method M1()

method M2()
{
  assume (forall x :: P<C>(x));
  M1();
  assert (forall x :: P<C>(x)); // FAILS (perhaps correctly)
}

method M3()
{
  assume (forall x :: P<C>(x));
  M1();
  assert AllP<C>();             // SUCCEEDS (perhaps incorrectly)
  assert (forall x :: P<C>(x)); // SUCCEEDS (perhaps incorrectly)
}

Commit 4957da6 introduced the {:warnShadowing false} attribute to locally suppress shadowing warnings. This works for functions, but it doesn't appear to work for lemmas/methods. Here's a small example:

lemma {:warnShadowing false} L(x:int)
{
    var x := 2;
}

Induction can be applied in two contexts:

• A method, in which case the potential induction variables are all the in-parameters
• A quantifier expression, in which case the potential induction variables are the bound variables
  of the quantifier expression.

The {:inductive} attribute is used to specify that only a subset of the potential
inductive variables be used. The current implementation requires that the given subset
be listed in the same order as they appear in the potential induction variables list.
But there does not seem to be a good reason for this restriction.

We propose that this restriction be removed and that induction be applied in the order
specified in the {:induction} attribute.

Are there any technological or ideological reasons for not supporting for loops in Dafny?

Verifying the following:

type word = x | 0 <= x < 0x1_0000_0000

function extract(src:map<int, word>): map<int, word>
    requires forall i :: 0 <= i < 0x10 ==> i in src
{
    (map i | 0 <= i < 0x10 :: src[i])
}

with Dafny 1.9.8 yields:

verified/test2.dfy(6,5): Error: value does not satisfy the subset constraints of 'map<int, word>'

Curiously, I have been able to work around this in a larger project by adding various assertions in the map expression (e.g. asserting that src[i] is in bounds, and then expressing it as src[i] as word), but that workaround is unstable and breaks when seemingly unrelated definitions in the environment change.

In the Dafny code below, the latest version of Dafny times out. It will succeed if you put the fuel for Looper one notch higher (as in the commented code below). Eliminating the call to reveal_Looper() also allows verification to succeed.

function Transform(x:int) : int

lemma TransformProperties()
    ensures forall x1, x2 {:trigger Transform(x1), Transform(x2)} :: Transform(x1) == Transform(x2) ==> x1 == x2;       

function {:opaque} Looper(input:seq<int>) : seq<int>
    ensures |Looper(input)| == |input|;
    ensures forall i :: 0 <= i < |input| ==> Looper(input)[i] == Transform(input[i])
{
    if |input| == 0 then []
    else [Transform(input[0])] + Looper(input[1..])
}

//lemma {:fuel Looper,2} proof(s1:seq<int>, s2:seq<int>)  // Succeeds
lemma proof(s1:seq<int>, s2:seq<int>)
    requires Looper(s1) == Looper(s2);
    ensures forall i :: i in s1 <==> i in s2;
{
    reveal_Looper();
    TransformProperties();
}

Inside the proof lemma, the new Dafny sets the fuel for all opaque functions to their respective base values via statements like:

assume StartFuel_F = Base_F
assume StartFuelAssert_F = Base_F

The reveal call then says:

assume StartFuel_F = LS(MoreFuel_F1)
assume StartFuelAssert_F = LS(LS(MoreFuel_F1))

for a new constant MoreFuel_F1.

This then gives us:

                LS(MoreFuel_F1) == LS(LS(MoreFuel_F1))
                ==> MoreFuel_F1 == LS(MoreFuel_F1)

This produces a trigger loop of infinite fuel, which produced an impressive 2.5 million instantiations in 30 seconds.

It succeeds when we give it more fuel because we then get:

StartFuel_F = LS(LS(Base_F))
StartFuelAssert_F = LS(LS(LS(Base_F)))

StartFuel_F = LS(MoreFuel_F1)
StartFuelAssert_F = LS(LS(MoreFuel_F1))

There are a couple of potential solutions here. My current proposal is that we have reveal instead emit:

StartFuel_F = LS(MoreFuel_F1)
StartFuelAssert_F = LS(LS(MoreFuelAssert_F1))

In other words, use a different constant for the StartFuel and the StartFuelAssert. That should prevent this kind of loop (and indeed works for this example).

Just a minor nitpick. When running Dafny with /trace, it produces output such as:

Verifying CheckWellformed$$_.foo ...
  [0.716 s, 2 proof obligations]  verified

Verifying Impl$$_.foo ...
  [187.421 s, 225 proof obligations]  verified

However, the line for "Verifying" only appears in the console window at the same time that the second line with the result information is printed, so you're never sure what Dafny is currently attempting to verify. I assume this could be fixed by adding an fflush()-equivalent between the two print statements.

The following code causes the Visual Studio plugin's call to DafnyDriver.Verify to hit an exception. An easy repro is to load the following code in the VS extension and watch it happily accept false.

lemma Foo()
{
var x := (0, 0);
assert false;
}

Here's the exception call stack, in which the problem seems to come from the fact that both UniqueIdPrefix and decl.tok.filename are null when it tries to compute prefix. Here, decl is {#_System.tuple#2.#Make2}.

DafnyPipeline.dll!Microsoft.Dafny.Translator.InsertUniqueIdForImplementation(Microsoft.Boogie.Declaration decl) Line 4221 + 0x45 bytes C#
DafnyPipeline.dll!Microsoft.Dafny.Translator.InsertChecksum(Microsoft.Boogie.Declaration decl, byte[] data) Line 4215 + 0xc bytes C#
DafnyPipeline.dll!Microsoft.Dafny.Translator.InsertChecksum(Microsoft.Dafny.DatatypeDecl d, Microsoft.Boogie.Declaration decl) Line 4161 + 0xf bytes C#
DafnyPipeline.dll!Microsoft.Dafny.Translator.AddDatatype(Microsoft.Dafny.DatatypeDecl dt) Line 1131 + 0x27 bytes C#
DafnyPipeline.dll!Microsoft.Dafny.Translator.DoTranslation(Microsoft.Dafny.Program p, Microsoft.Dafny.ModuleDefinition forModule) Line 620 + 0x4f bytes C#
DafnyPipeline.dll!Microsoft.Dafny.Translator.Translate(Microsoft.Dafny.Program p, Microsoft.Dafny.ErrorReporter reporter, Microsoft.Dafny.Translator.TranslatorFlags flags) Line 719 + 0x3c bytes C#
System.Core.dll!System.Linq.Enumerable.SelectManyIterator<System.Tuple<string,Microsoft.Boogie.Program>,Microsoft.Boogie.Implementation>.MoveNext() + 0x184 bytes
System.Core.dll!System.Linq.Enumerable.WhereSelectEnumerableIterator<Microsoft.Boogie.Implementation,string>.MoveNext() + 0x58 bytes
System.Core.dll!System.Linq.Enumerable.ExceptIterator.MoveNext() + 0xb4 bytes
DafnyLanguageService.dll!DafnyLanguage.ResolverTagger.ReInitializeVerificationErrors(string mostRecentRequestId, System.Collections.Generic.IEnumerable<Microsoft.Boogie.Implementation> implementations) Line 166 + 0x63 bytes C#
DafnyLanguageService.dll!DafnyLanguage.DafnyDriver.Verify(Microsoft.Dafny.Program dafnyProgram, DafnyLanguage.ResolverTagger resolver, string uniqueIdPrefix, string requestId, Microsoft.Boogie.ErrorReporterDelegate er) Line 295 + 0x11 bytes C#
DafnyLanguageService.dll!DafnyLanguage.ProgressTagger.RunVerifier(Microsoft.Dafny.Program program, Microsoft.VisualStudio.Text.ITextSnapshot snapshot, string requestId, DafnyLanguage.ResolverTagger errorListHolder, bool diagnoseTimeouts) Line 374 + 0xe1 bytes C#
DafnyLanguageService.dll!DafnyLanguage.ProgressTagger.RunVerifierThreadRoutine(object o) Line 432 + 0x2f bytes C#
mscorlib.dll!System.Threading.ThreadHelper.ThreadStart_Context(object state) + 0x73 bytes
mscorlib.dll!System.Threading.ExecutionContext.RunInternal(System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, object state, bool preserveSyncCtx) + 0xc2 bytes
mscorlib.dll!System.Threading.ExecutionContext.Run(System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, object state, bool preserveSyncCtx) + 0x16 bytes
mscorlib.dll!System.Threading.ExecutionContext.Run(System.Threading.ExecutionContext executionContext, System.Threading.ContextCallback callback, object state) + 0x41 bytes
mscorlib.dll!System.Threading.ThreadHelper.ThreadStart(object obj) + 0x4e bytes

Playing around with things that don't exist yet, I managed to crash what I assume is the parser.

This input:

newtype Even = n: int | exists h :: h * 2 == n

results in this error:

Error from syntax checker dafny-server: 
[FATAL] Exception of type 'cce+UnreachableException' was thrown.

Tried dafny in the online website, looks like it is bug?

method Test(m: nat) returns (r: nat) 
{
  var m1: nat := 0;
  while (m1 < m) {
    m1 := m1 + 1;
  }
  assert m == m1; // fail assert
}

more try:

method Test(m: nat) returns (r: nat) 
{
  var m1: nat := 0;
  while (m1 < m) {
    assert m1 < m;
    m1 := m1 + 1;
  }
  assert !(m1 < m);   // pass
  assert m1 == m || m1 > m;  // pass
  assert m1 == m;  // fail
}

The following function:

function BitvectorCast(x:bv32): int
    ensures x != 0 ==> BitvectorCast(x) != 0;
{
    x as int
}

Causes an assertion failure in Dafny 1.9.8:

When I run Dafny on test2.dfy below, it crashes with the error below. The problem seems to arise from including a file (in this case test1.dfy) that includes a forall.

test1.dfy.txt
test2.dfy.txt

Unhandled Exception: System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.BlockStmt' to type 'Microsoft.Dafny.AssignStmt'.
at Microsoft.Dafny.ForallStmtRewriter.ForAllStmtVisitor.VisitOneStmt(Statement stmt, Boolean& st) in f:\Apps\dafny.git\Source\Dafny\Rewriter.cs:line 116
at Microsoft.Dafny.TopDownVisitor1.Visit(Statement stmt, State st) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9636 at Microsoft.Dafny.TopDownVisitor1.<>c__DisplayClass8.b__5(Statement s) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9639
at Microsoft.Boogie.LinqExtender.Iter[T](IEnumerable1 coll, Action1 fn) in f:\Apps\codeplex\boogie\Source\Core\Util.cs:line 62
at Microsoft.Dafny.TopDownVisitor1.Visit(Statement stmt, State st) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9639 at Microsoft.Dafny.TopDownVisitor1.Visit(Method method, State st) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9673
at Microsoft.Dafny.TopDownVisitor1.Visit(ICallable decl, State st) in f:\Apps\dafny.git\Source\Dafny\DafnyAst.cs:line 9664 at Microsoft.Dafny.ForallStmtRewriter.PostResolve(ModuleDefinition m) in f:\Apps\dafny.git\Source\Dafny\Rewriter.cs:line 85 at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in f:\Apps\dafny.git\Source\Dafny\Resolver.cs:line 380 at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in f:\Apps\dafny.git\Source\Dafny\DafnyMain.cs:line 147 at Microsoft.Dafny.Main.ParseCheck(IList1 files, String programName, ErrorReporter reporter, Program& program) in f:\Apps\dafny.git\Source\Dafny\DafnyMain.cs:line 96
at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList1 dafnyFiles, ReadOnlyCollection1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in f:\Apps\dafny.git\Source\DafnyDriver\DafnyDriver.cs:line 174
at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in f:\Apps\dafny.git\Source\DafnyDriver\DafnyDriver.cs:line 59
at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass1.

Here's an example that suggests Dafny's type inference may be struggling with sequences and generics. In the Example1 function below, we get an error that the return values of RepeatValue may not satisfy the constraints of seq. If we provide the type explicitly when calling RepeatValue (as shown in Example2), then there's no error.

type uint32 = i:int | 0 <= i < 0x1_0000_0000

function RepeatValue<T>(n:T, count:nat) : seq<T>

function Example1(len:nat) : seq<uint32>
{
    // Error: value does not satisfy the subset constraints of 'seq<uint32>'
    RepeatValue(5 as uint32, len)       
}

function Example2(len:nat) : seq<uint32>
{
    // Success
    RepeatValue<uint32>(5 as uint32, len)
}

Rustan has commented that, if the {:layerQuantifier} is to stay at all, that it should be renamed to {:fuelQuantifier}. In addition, if this is kept, the reference manual needs a more complete description of the purpose and effect of this attribute. If it is only used internally its name should start with a leading underscore.

When a lemma in an abstract module has a body, it gets verified, so it shouldn't be necessary to verify that lemma again each time the abstract module is refined. Yet, Dafny seems to try to do this when the abstract module is refined in a different file. Furthermore, this attempt to re-verify can fail in some circumstances.

Here's an example consisting of two files. In file test1.dfy, abstract module m2 is introduced and refined by m3. In file test2.dfy, m2 is refined again by m4, and this causes a failure. This failure when verifying m4 occurs whether or not m3 exists in test1.dfy; I just put m3 in test1.dfy to illustrate that the problem only arises when the refinement happens in a different file.

test1.dfy.txt
test2.dfy.txt

The recent change to opaque ("Rewrite opaque using fuel", commit 01f90e6) causes a change in behavior with opaque functions. Here's an example:

function{:opaque} f(i:int):int { if i > 0 then 1 + f(i - 1) else 0 }

lemma L(x:int)
  requires 10 <= x <= 11 || 20 <= x <= 21;
{
  assert f(x) == x; // it's surprising that this verifies when opaque f is never revealed
}

This verifies even though f is never revealed, because the literals 10, 11, 20, and 21 trigger an axiom that doesn't respect opaque. I worry that this will make it harder to diagnose slow verification performance. Usually, with opaque, I'm confident that the body of an opaque function isn't the cause of slow verification, as long as the function's body is never revealed. With the special behavior for literals, I have to worry that slow performance might be due to the body of an opaque function after all, depending on what literals are in scope.

An alternative would be to make the axiom for literals for opaque functions require fuel, just like the axiom for non-literals for opaque functions, so that opaque behaves more consistently between literals and non-literals. Maybe the literal axiom could still run without consuming the fuel that it's given, but it would need non-zero fuel to get triggered in the first place.