Can I use Dafny for formally verifying compilers?

[ichxorya]

Title. I'm new to both Dafny and formal semantics, and would like to use the language as the basis for my Master's thesis on formally verifying a compiler. Luckily, an example on a compiler (C# + ANTLR 4 + Dafny) was provided officially by Dafny (https://github.com/dafny-lang/dafny/tree/master/Source/IntegrationTests/TestFiles/LitTests/LitTest/examples/Simple_compiler).

As I was trying it out, I noticed that there's a FIXME, with two lemmas (induction = false as a work-around). My question is: "Do Dafny have enough functionality for the task of defining formally verified compilers, and if so, why there is a FIXME in this example?".

I'm new to both Dafny and formal semantics so I don't see anything wrong with the FIXME, it just the SAT Solver underneath can't workout the lemma properly.

lemma {:induction false} compileExprCorrect'(e: DafnyAST.Expr, st: State) // FIXME default induction on e, st breaks things
    ensures interpProg'(compileExpr(e), st) ==
            st.(stack := Cons(DafnyAST.interpExpr(e, st.regs), st.stack))
  {
    match e {
      case Const(n) =>
      case Var(v) =>
      case Op(op, e1, e2) => // Here's the expanded version of the same proof
        interpProg'_Concat(compileExpr(e2), compileExpr(e1), st);
        compileExprCorrect'(e1, st);
        var st' := st.(stack := Cons(DafnyAST.interpExpr(e1, st.regs), st.stack));
        compileExprCorrect'(e2, st');
        // var st'' := st'.(stack := Cons(DafnyAST.interpExpr(e2, st'.regs), st'.stack));
    }
  }

  lemma {:induction false} compileStmtCorrect'(s: DafnyAST.Stmt, st: State)
    ensures interpProg'(compileStmt(s), st) ==
            var InterpResult(ctx', output) := DafnyAST.interpStmt'(s, st.regs);
            st.(regs := ctx', output := st.output + output)
  {
    match s {
      case Skip =>
      case Assign(v, e) =>
        compileExprCorrect'(e, st);
      case Print(e) =>
        compileExprCorrect'(e, st);
      case Seq(s1, s2) =>
        interpProg'_Concat(compileStmt(s2), compileStmt(s1), st);
        compileStmtCorrect'(s1, st);
        compileStmtCorrect'(s2, interpProg'(compileStmt(s1), st));
        // calc { // Here is the original proof
        //   interpProg'(compileStmt(s), st);
        //   interpProg'(compileStmt(DafnyAST.Seq(s1, s2)), st);
        //   interpProg'(Concat(compileStmt(s2), compileStmt(s1)), st);
        //   { interpProg'_Concat(compileStmt(s2), compileStmt(s1), st); }
        //   interpProg'(compileStmt(s2), interpProg'(compileStmt(s1), st));
        //   { compileStmtCorrect'(s1, st); }
        //   var (ctx1, o1) := DafnyAST.interpStmt'(s1, st.regs);
        //   interpProg'(compileStmt(s2), st.(regs := ctx1, output := st.output + o1));
        //   == { compileStmtCorrect'(s2,
        //          var (ctx', output) := DafnyAST.interpStmt'(s1, st.regs);
        //          st.(regs := ctx', output := st.output + output)); }
        //   var (ctx1, o1) := DafnyAST.interpStmt'(s1, st.regs);
        //   var (ctx2, o2) := DafnyAST.interpStmt'(s2, ctx1);
        //   st.(regs := ctx2, output := st.output + o1 + o2);
        // }
    }
  }

Besides the problem above, there is also this similar problem on timeout, #5768

Thank you for reading this!

[keyboardDrummer]

Do Dafny have enough functionality for the task of defining formally verified compilers

It does

, and if so, why there is a FIXME in this example?

Dafny has a feature called automatic induction, which can reduce the amount of code your need to write a proof. In this lemma that feature is turned off using the attribute {:induction false}, and the FIXME is saying something needs to be improved in automatic induction so it can be used there. In any case, using automatic induction is not necessary for any Dafny application.

[ichxorya]

Thank you, does that also mean we can just define inductive proofs by hand in Dafny, just like Coq and other theorem provers?

[keyboardDrummer]

You can define inductive proofs in Dafny, for sure, but Dafny relies on SMT solving to find its proofs while Coq, as far as I understand, relies on tactics, which provides a different proof writing experience.