dafny-admitter

Extracts failing verification obligations from Dafny verify output and inserts them as admits or assertions to help with incremental verification.

How It Works

1. Run dafny verify file.dfy to get failing verification obligations
2. Parse Dafny output for:
   • Error locations (e.g., file.dfy(493,46): Error: a postcondition could not be proved)
   • Related locations (e.g., file.dfy(489,39): Related location: this is the postcondition)
3. Extract the actual contract expression from the Dafny source:
   • For assertions: Extract from the assert statement at the error location
   • For preconditions: Extract from the requires clause and substitute call-site arguments
   • For postconditions: Extract from the ensures clause
   • For invariants: Extract from the invariant clause
4. Insert at the appropriate location:
   • Postconditions → at end of method body
   • Preconditions → before the call site
   • Assertions → at the assertion location
5. Re-insert as either assert P; or Admit("…", P);

This approach handles:

• ✅ User assertions → extracted from assert statements
• ✅ Preconditions → with actual-for-formal substitution at call sites
• ✅ Postconditions → inserted at method body end
• ✅ Loop invariants → from invariant clauses

Install

pip install -e .

Usage

dafny-admitter examples/sample.dfy --mode assert --stdout
# or
dafny-admitter PATH/TO/file.dfy --mode admit
# or for gradual verification (admit + runtime checks)
dafny-admitter PATH/TO/file.dfy --mode gradual

Flags

• --mode {assert,admit,gradual}: What to insert:
  • assert: emit assert P; (requires full verification)
  • admit: emit Admit("…", P); (verification bypass)
  • gradual: emit expect P; Admit("…", P); for methods (runtime checks + verification bypass), Admit("…", P); only for lemmas/functions (ghost code)
• --dafny-bin: override Dafny binary (default: dafny)
• --stdout: print patched Dafny instead of writing *.patched.dfy
• --timeout: timeout in seconds for Dafny verification
• --max-iterations: maximum number of iterations for iterative patching (default: 1 for assert mode, 10 for admit/gradual)

Examples

Postcondition Failure (on return path)

lemma theorem_preservation(t: tm)
  requires has_type(map[], t).Some?
  requires step(t).Some?
  ensures has_type(map[], step(t).get) == has_type(map[], t)
{
  if (t.tapp? && t.f.tabs? && value(t.arg)) {
    // Empty block - postcondition fails here
  } else if (...) {
    ...
  }
}

The tool inserts the assertion inside the failing block:

if (t.tapp? && t.f.tabs? && value(t.arg)) {
  // SKETCH-INSERT begin (dafny@493:46)
  assert has_type(map[], step(t).get) == has_type(map[], t);
  // SKETCH-INSERT end
} else if (...) {

Precondition Failure

method Foo(x: int)
  requires x > 0
{ }

method Bar() {
  Foo(-1);  // fails precondition
}

The tool inserts (with actual argument substituted):

// SKETCH-INSERT begin (dafny@6:5)
assert -1 > 0;
// SKETCH-INSERT end

Regular Assertion

method Test(x: int)
  requires x > 0
{
  assert x > 5;  // fails
}

The tool inserts:

// SKETCH-INSERT begin (bpl@2969:5)
assert x > 5;
// SKETCH-INSERT end

Gradual Verification Mode

Gradual mode (--mode gradual) provides runtime checks for methods while allowing verification to proceed. This enables iterative debugging: the program verifies but fails at runtime when an admit is invalid.

method Divide(x: int, y: int) returns (r: int)
  requires y != 0
{ r := x / y; }

method TestDivide() {
  var result := Divide(10, 0);  // fails precondition
}

lemma TestLemma(x: int)
  ensures x > 0
{ }  // fails postcondition

With --mode gradual, the tool generates:

method TestDivide() {
  // SKETCH-INSERT begin (dafny@6:22)
  expect 0 != 0, "Runtime check failed: dafny@6:22";
  Admit("dafny@6:22", 0 != 0);
  // SKETCH-INSERT end
  var result := Divide(10, 0);
}

lemma TestLemma(x: int)
  ensures x > 0
{
  // SKETCH-INSERT begin (dafny@11:0)
  Admit("ensures@11:0", x > 0);
  // SKETCH-INSERT end
}

Note: Methods get both expect (runtime check) and Admit (verification bypass), while lemmas/functions only get Admit (since ghost code doesn't execute at runtime).

Notes

• Contract expressions (requires/ensures/invariant/assert) are extracted directly from Dafny source for maximum accuracy.
• Preconditions are substituted with actual call-site arguments for better context.
• Postconditions are inserted at the end of method bodies (the correct proof locus).
• The tool supports iterative patching, converging when the file verifies with 0 errors.