feat: Prelude extractor (#5621)

## Description

This PR adds a way to extract a Dafny model into set of Boogie
declarations. This new feature can be of general use, but its main
application is to justify various axioms in Dafny's `DafnyPrelude.bpl`
by providing a model for them.

## Impact on the Dafny tool

The model for Dafny's underlying type `Seq` is given in
`Source/DafnyCore/Prelude/Sequences.dfy`.

The file `Source/DafnyCore/DafnyPrelude.bpl` should no longer be edited
by hand. Instead, it is now generated from
`Source/DafnyCore/Prelude/PreludeCore.bpl` and from the model
`Sequences.dfy` (and other models in the future, for example for
multisets).

To generate a new version of `DafnyPrelude.bpl`, run `make extract` in
the `Source/DafnyCore` folder. This will run `make` in the
`Source/DafnyCore/Prelude` folder and will then copy the generated
`Prelude/DafnyPrelude.bpl` to `DafnyPrelude.bpl`.

## CLI option

This PR adds a CLI option `--extract:<file>` (where `<file>` is allowed
to be `-` to denote standard output, just like for the various print
options). This option works with the `dafny verify` command.

Caveats:

This gets the job done, but is probably not the best way of doing it.
For instance, one could imagine a `dafny extract` command that performs
this task.

I'm unsure of the code I added to handle this CLI option. In particular,
I don't understand if I have added it just for the `dafny verify`
command or also for other commands, and I don't understand if I have
made the option available via the language server (or if we care).

## Changes to `DafnyPrelude.bpl`

This PR contains changes to `DafnyPrelude.bpl`. The claim is that these
changes make no semantic difference. The changes are:

* differences in whitespace
* other changes to format the code like the Boogie `/print` option does
(for example, `s: Seq, t: Seq` instead of `s, t: Seq`)
* in the `Seq` part of `DafnyPrelude.bpl`, the declarations that are not
part of the model in `Sequences.dfy` have
been moved to the end, so that the extracted declarations can be in one
contiguous part of the file

The third of these bullets do change the order in which things are sent
to the SMT solver, and thus this may impact some users.

## Extract mechanism

Upon successful verification, the new extract mechanism added by this PR
will visit the AST of the given program. For any module marked with
`{:extract}`, the extract-worthy material from the module is output. The
output declarations will be in the same order as they appear textually
in the module (in particular, the fact that module-level Dafny
declarations are collected in an internal class `_default` has no
bearing on the output order).

Three kinds of declarations are extract-worthy:

* A type declaration `A<X, Y, Z>` that bears an attribute
`{:extract_name B}` is extracted into a Boogie type declaration `type B
_ _ _;`.

The definition of the type is ignored. (The intended usage for an
extracted type is that the Dafny program give a definition for the type,
which goes to show the existence of such a type.)

* A function declaration `F(x: X, y: Y): Z` that bears an attribute
`{:extract_name G}` is extracted into a Boogie function declaration
`function G(x: X, y: Y): Z;`.

The body of the Dafny function is ignored. (The intended usage for an
extracted function is that the Dafny program give a definition for the
function, which goes to show the existence of such a function.)

* A lemma declaration `L(x: X, y: Y) requires P ensures Q` that bears an
attribute `{:extract_pattern ...}` or an attribute `{:extract_used_by
...}` is extracted into a Boogie `axiom`. The axiom has the basic form
`axiom (forall x: X, y: Y :: P ==> Q);`.

If the lemma has an attribute `{:extract_used_by F}`, then the axiom
will be emitted into the `uses` clause of the Boogie function generated
for Dafny function `F`.

    If the lemma has no in-parameters, the axiom is just `P ==> Q`.

If the lemma has in-parameters, then any attribute `{:extract_pattern E,
F, G}` adds a matching pattern `{ E, F, G }` to the emitted quantifier.
Also, any attribute `{:extract_attribute "name", E, F, G}` adds an
attribute `{:name E, F, G}` to the quantifier.

## Expressions

The pre- and postconditions of extracted lemmas turn into analogous
Boogie expressions, and the types of function/lemma parameters and bound
variables are extracted into analogous Boogie types. The intended usage
of the extract mechanism is that these expressions and types do indeed
have analogous Boogie types.

At this time, only a limited set of expressions and types are supported,
but more can be added in the future.

Any `forall` and `exists` quantifiers in expressions are allowed to use
`:extract_pattern` and `:extract_attribute` attributes, as described
above for lemmas.

Some extracted expressions are simplified. For example, `true && !!P` is
simplified to `P`.

## Soundness

The Dafny program that is used as input for the extraction is treated
like any other Dafny program. The intended usage of the extraction
mechanism is to prove parts of the axiomatization in `DafnyPrelude.bpl`
to be logically consistent. Whether or not the extracted Boogie
declarations meet this goal depends on the given Dafny program. For
example, if the given Dafny program formalizes sequences in terms of
maps and formalizes maps in terms of sequences, then the extraction
probably does not provide guarantees of consistency.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

.gitignore

@@ -88,3 +88,5 @@ Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.deps.json
 Source/IntegrationTests/TestFiles/LitTests/LitTest/**/*.csproj
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/multimodule/PythonModule2
 /Source/IntegrationTests/TestFiles/LitTests/LitTest/pythonmodule/singlemodule/dafnysource/PythonModule1
+/Source/DafnyCore/Prelude/DafnyPrelude.bpl
+/Source/DafnyCore/Prelude/Sequences.bpl

Source/DafnyCore/Backends/BoogieExtractor.cs

@@ -0,0 +1,350 @@
+//-----------------------------------------------------------------------------
+//
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+//
+//-----------------------------------------------------------------------------
+
+#nullable enable
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Numerics;
+using System.Diagnostics.Contracts;
+using Microsoft.BaseTypes;
+using Microsoft.Boogie;
+
+namespace Microsoft.Dafny.Compilers {
+  public class ExtractorError : Exception {
+    public ExtractorError(string message)
+      : base(message) {
+    }
+  }
+
+  public class BoogieExtractor : ASTVisitor<IASTVisitorContext> {
+    /// <summary>
+    /// Says to look inside the module for contents to extract.
+    /// Can be applied to a module.
+    /// 
+    /// Note: This attribute isn't used yet, so the use of the attribute is just a stylistic thing at the moment.
+    /// Similarly, one can imagine that the extractor will look at a module's export clauses, to--in some way--check that
+    /// the set of Boogie declarations exported are self consistent. But that isn't done yet, either. Instead, all contents
+    /// of all files given to the extractor are considered for extraction.  
+    /// </summary>
+    private const string ExtractAttribute = "extract_boogie";
+
+    /// <summary>
+    /// Gives the Boogie name to be used in the extraction.
+    /// Can be applied to types and functions.
+    /// </summary>
+    private const string NameAttribute = "extract_boogie_name";
+
+    /// <summary>
+    /// Says to place the extracted axiom declaration in the "uses" block of the given function.
+    /// Can be applied to lemmas.
+    /// </summary>
+    private const string UsedByAttribute = "extract_used_by";
+
+    /// <summary>
+    /// Gives a matching pattern to be applied in the quantifier emitted from a lemma or from a quantifier.
+    /// Can be applied to lemmas and quantifiers.
+    /// </summary>
+    private const string PatternAttribute = "extract_pattern";
+
+    /// <summary>
+    /// Specifies an additional attribute to be attached to the quantifier emitted from a lemma.
+    /// Can be applied to lemmas.
+    /// </summary>
+    private const string AttributeAttribute = "extract_attribute";
+
+    /// <summary>
+    /// Throws an "ExtractorError" if the input is unexpected or unsupported.
+    /// </summary>
+    public static Boogie.Program Extract(Program program) {
+      var extractor = new BoogieExtractor();
+      extractor.VisitModule(program.DefaultModule);
+      extractor.FixUpUsedByInformation();
+
+      var extractedProgram = new Boogie.Program();
+      extractedProgram.AddTopLevelDeclarations(extractor.allDeclarations);
+      return extractedProgram;
+    }
+
+    private List<Boogie.Declaration> declarations = new(); // for the current module
+    private List<Boogie.Declaration> allDeclarations = new(); // these are the declarations for all modules marked with {:extract} 
+    private readonly Dictionary<Function, Boogie.Function> functionExtractions = new();
+    private readonly List<(Boogie.Axiom, Function)> axiomUsedBy = new();
+
+    private BoogieExtractor() {
+    }
+
+    void FixUpUsedByInformation() {
+      foreach (var (axiom, function) in axiomUsedBy) {
+        if (!functionExtractions.TryGetValue(function, out var boogieFunction)) {
+          throw new ExtractorError($":{UsedByAttribute} attribute mentions non-extracted function: {function.Name}");
+        }
+        boogieFunction.OtherDefinitionAxioms.Add(axiom);
+      }
+      axiomUsedBy.Clear();
+    }
+
+    public override IASTVisitorContext GetContext(IASTVisitorContext astVisitorContext, bool inFunctionPostcondition) {
+      return astVisitorContext;
+    }
+
+    void VisitModule(ModuleDecl module) {
+      var previousDeclarations = declarations;
+      declarations = new();
+
+      VisitDeclarations(module.Signature.TopLevels.Values.ToList());
+
+      if (Attributes.Contains(module.Signature.ModuleDef.Attributes, ExtractAttribute)) {
+        declarations.Sort((d0, d1) => d0.tok.pos - d1.tok.pos);
+        allDeclarations.AddRange(declarations);
+      }
+      declarations = previousDeclarations;
+    }
+
+    protected override void VisitOneDeclaration(TopLevelDecl decl) {
+      if (decl is ModuleDecl moduleDecl) {
+        VisitModule(moduleDecl);
+        return;
+      }
+
+      if (GetExtractName(decl.Attributes) is { } extractName) {
+        var ty = new Boogie.TypeCtorDecl(decl.tok, extractName, decl.TypeArgs.Count);
+        declarations.Add(ty);
+      }
+
+      base.VisitOneDeclaration(decl); // this will visit the declaration's members
+    }
+
+    public override void VisitMethod(Method method) {
+      if (method is not Lemma lemma) {
+        return;
+      }
+
+      var patterns = Attributes.FindAllExpressions(lemma.Attributes, PatternAttribute);
+      var usedByInfo = Attributes.Find(lemma.Attributes, UsedByAttribute);
+      if (patterns == null && usedByInfo == null) {
+        return;
+      }
+
+      if ((lemma.Ins.Count == 0) != (patterns == null)) {
+        throw new ExtractorError($"a parameterized lemma must specify at least one :{PatternAttribute}: {lemma.Name}");
+      }
+      if (lemma.TypeArgs.Count != 0) {
+        throw new ExtractorError($"an extracted lemma is not allowed to have type parameters: {lemma.Name}");
+      }
+      if (lemma.Outs.Count != 0) {
+        throw new ExtractorError($"an extracted lemma is not allowed to have out-parameters: {lemma.Name}");
+      }
+
+      var tok = lemma.tok;
+
+      var boundVars = lemma.Ins.ConvertAll(formal =>
+        (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type)))
+      );
+
+      var triggers = GetTriggers(tok, patterns);
+
+      var ante = BoogieGenerator.BplAnd(lemma.Req.ConvertAll(req => ExtractExpr(req.E)));
+      var post = BoogieGenerator.BplAnd(lemma.Ens.ConvertAll(ens => ExtractExpr(ens.E)));
+      var body = BoogieGenerator.BplImp(ante, post);
+
+      Boogie.Expr axiomBody;
+      if (boundVars.Count == 0) {
+        axiomBody = body;
+      } else {
+        var kv = GetKeyValues(tok, lemma.Attributes);
+        axiomBody = new Boogie.ForallExpr(tok, new List<TypeVariable>(), boundVars, kv, triggers, body);
+      }
+      var axiom = new Boogie.Axiom(tok, axiomBody);
+      declarations.Add(axiom);
+
+      if (usedByInfo != null) {
+        if (usedByInfo.Args.Count == 1 && usedByInfo.Args[0].Resolved is MemberSelectExpr { Member: Function function }) {
+          axiomUsedBy.Add((axiom, function));
+        } else {
+          throw new ExtractorError($":{UsedByAttribute} argument on lemma '{lemma.Name}' is expected to be an extracted function");
+        }
+      }
+    }
+
+    private Trigger? GetTriggers(IToken tok, List<List<Expression>>? patterns) {
+      if (patterns == null) {
+        return null;
+      }
+
+      Boogie.Trigger? triggers = null;
+      for (var i = 0; i < patterns.Count; i++) {
+        var terms = patterns![i].ConvertAll(ExtractExpr);
+        triggers = new Boogie.Trigger(tok, true, terms, triggers);
+      }
+
+      return triggers;
+    }
+
+    private QKeyValue? GetKeyValues(IToken tok, Attributes attributes) {
+      Boogie.QKeyValue kv = null;
+      var extractAttributes = Attributes.FindAllExpressions(attributes, AttributeAttribute);
+      if (extractAttributes != null) {
+        if (extractAttributes.Count == 0) {
+          throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got no arguments");
+        }
+        for (var i = extractAttributes.Count; 0 <= --i;) {
+          string? attrName = null;
+          var parameters = new List<object>();
+          foreach (var argument in extractAttributes[i]) {
+            if (attrName != null) {
+              parameters.Add(ExtractExpr(argument));
+            } else if (argument is StringLiteralExpr { Value: string name }) {
+              attrName = name;
+            } else {
+              throw new ExtractorError($"first argument to :{AttributeAttribute} is expected to be a literal string; got: {argument}");
+            }
+          }
+
+          kv = new Boogie.QKeyValue(tok, attrName, parameters, kv);
+        }
+      }
+
+      return kv;
+    }
+
+    public override void VisitFunction(Function function) {
+      if (GetExtractName(function.Attributes) is { } extractName) {
+        var tok = function.tok;
+        if (function.TypeArgs.Count != 0) {
+          throw new ExtractorError($"an extracted function is not allowed to have type parameters: {function.Name}");
+        }
+        var inParams = function.Ins.ConvertAll(formal =>
+          (Boogie.Variable)new Boogie.Formal(tok, new TypedIdent(tok, formal.Name, ExtractType(formal.Type)), true)
+        );
+        var result = new Boogie.Formal(tok, new TypedIdent(tok, TypedIdent.NoName, ExtractType(function.ResultType)), false);
+        var fn = new Boogie.Function(tok, extractName, inParams, result);
+        declarations.Add(fn);
+        functionExtractions.Add(function, fn);
+      }
+    }
+
+    private Boogie.Type ExtractType(Type type) {
+      switch (type) {
+        case IntType:
+          return Boogie.Type.Int;
+        case BoolType:
+          return Boogie.Type.Bool;
+        case UserDefinedType udt: {
+            var cl = udt.ResolvedClass;
+            var name = GetExtractName(cl.Attributes) ?? cl.Name;
+            return new Boogie.UnresolvedTypeIdentifier(Boogie.Token.NoToken, name, udt.TypeArgs.ConvertAll(ExtractType));
+          }
+        default:
+          throw new ExtractorError($"type not supported by extractor: {type}");
+      }
+    }
+
+    private string? GetExtractName(Attributes attributes) {
+      if (Attributes.Find(attributes, NameAttribute) is { } extractNameAttribute) {
+        if (extractNameAttribute.Args.Count == 1 && extractNameAttribute.Args[0] is StringLiteralExpr { Value: string extractName }) {
+          return extractName;
+        }
+      }
+      return null;
+    }
+
+    private Boogie.Expr ExtractExpr(Expression expr) {
+      expr = expr.Resolved;
+      var tok = expr.tok;
+      switch (expr) {
+        case LiteralExpr literalExpr: {
+            if (literalExpr.Value is bool boolValue) {
+              // use the specific literals, rather than Boogie.LiteralExpr(bool), in order for the
+              // peephole optimizations to kick in
+              return boolValue ? Boogie.Expr.True : Boogie.Expr.False;
+            } else if (literalExpr.Value is BigInteger intValue) {
+              var n = BigNum.FromBigInt(intValue);
+              return Boogie.Expr.Literal(n);
+            }
+            break;
+          }
+
+        case IdentifierExpr identifierExpr:
+          return new Boogie.IdentifierExpr(tok, identifierExpr.Name);
+
+        case FunctionCallExpr functionCallExpr: {
+            var function = functionCallExpr.Function;
+            var functionName = GetExtractName(function.Attributes) ?? function.Name;
+            Contract.Assert(function.IsStatic);
+            var arguments = functionCallExpr.Args.ConvertAll(ExtractExpr);
+            return new Boogie.NAryExpr(tok, new Boogie.FunctionCall(new Boogie.IdentifierExpr(tok, functionName)), arguments);
+          }
+
+        case BinaryExpr binaryExpr: {
+            var e0 = ExtractExpr(binaryExpr.E0);
+            var e1 = ExtractExpr(binaryExpr.E1);
+            switch (binaryExpr.ResolvedOp) {
+              case BinaryExpr.ResolvedOpcode.EqCommon:
+                return Boogie.Expr.Eq(e0, e1);
+              case BinaryExpr.ResolvedOpcode.NeqCommon:
+                return Boogie.Expr.Neq(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Iff:
+                return BoogieGenerator.BplIff(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Imp:
+                return BoogieGenerator.BplImp(e0, e1);
+              case BinaryExpr.ResolvedOpcode.And:
+                return BoogieGenerator.BplAnd(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Or:
+                return BoogieGenerator.BplOr(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Le:
+                return Boogie.Expr.Le(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Lt:
+                return Boogie.Expr.Lt(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Add:
+                return Boogie.Expr.Add(e0, e1);
+              case BinaryExpr.ResolvedOpcode.Sub:
+                return Boogie.Expr.Sub(e0, e1);
+              default:
+                break;
+            }
+            break;
+          }
+
+        case UnaryOpExpr unaryOpExpr:
+          if (unaryOpExpr.ResolvedOp == UnaryOpExpr.ResolvedOpcode.BoolNot) {
+            var e = ExtractExpr(unaryOpExpr.E);
+            return Boogie.Expr.Not(e);
+          } else {
+            throw new ExtractorError($"extractor does not support unary operator {unaryOpExpr.ResolvedOp}");
+          }
+
+        case QuantifierExpr quantifierExpr: {
+            var boundVars = quantifierExpr.BoundVars.ConvertAll(boundVar =>
+              (Boogie.Variable)new Boogie.BoundVariable(tok, new TypedIdent(tok, boundVar.Name, ExtractType(boundVar.Type)))
+            );
+
+            var patterns = Attributes.FindAllExpressions(quantifierExpr.Attributes, PatternAttribute);
+            if (patterns.Count == 0) {
+              throw new ExtractorError($"extraction expects every quantifier to specify at least one :{PatternAttribute}");
+            }
+            var triggers = GetTriggers(tok, patterns);
+
+            var kv = GetKeyValues(tok, quantifierExpr.Attributes);
+            var body = ExtractExpr(quantifierExpr.LogicalBody());
+            if (quantifierExpr is ExistsExpr) {
+              return new Boogie.ExistsExpr(tok, new List<TypeVariable>(), boundVars, kv, triggers, body);
+            } else {
+              Contract.Assert(quantifierExpr is ForallExpr);
+              return new Boogie.ForallExpr(tok, new List<TypeVariable>(), boundVars, kv, triggers, body);
+            }
+          }
+
+        default:
+          break;
+      }
+
+      throw new ExtractorError($"extraction does not support expression of type {expr.GetType()}: {expr}");
+    }
+  }
+}

Source/DafnyCore/DafnyOptions.cs

@@ -320,6 +320,7 @@ public enum ContractTestingMode {
     public PrintModes PrintMode = PrintModes.Everything; // Default to printing everything
     public bool DafnyVerify = true;
     public string DafnyPrintResolvedFile = null;
+    public string BoogieExtractionTargetFile = null;
     public List<string> DafnyPrintExportedViews = new List<string>();
     public bool Compile = true;
     public List<string> MainArgs = new List<string>();