feat: Prelude extractor #5621

RustanLeino · 2024-07-12T03:33:18Z

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.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

The difference between the legacy/refresh resolver runs is that some bound variables and an empty set are typed with …Node… in legacy and …Node?… in refresh.

atomb

I think this looks great. The one change I think would be good to include is the one you suggest in the summary: to make it a separate top-level command. Along the way, I think it might be better to use a more descriptive term than "extract". I was thinking "extract-boogie-axioms", though it could be just "extract-axioms" if there's a possibility it might support other languages eventually.

atomb · 2024-07-18T23:27:01Z

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -28,6 +36,13 @@ public static class VerifyCommand {
  public static readonly Option<string> FilterPosition = new("--filter-position",
    @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");

+  public static readonly Option<string> ExtractTarget = new("--extract", @"


I think I'd prefer for this to be a top-level command, and perhaps a little more explanatory. One possibility would be dafny extract-boogie-axioms. (The types and functions are missing definitions, and are essentially axioms, as well.)

One possible downside is that I'm not sure whether commands can be hidden...

I, too, would like to see this as a top-level command. However, since I don't understand how commands are added to the source or how we make a command do certain things, I'm leaving this as is for now. I will ask @keyboardDrummer for help to make such a change in a separate PR.

Source/DafnyDriver/Commands/VerifyCommand.cs

atomb · 2024-07-18T23:29:29Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/Fuel.legacy.dfy.expect

@@ -21,19 +21,19 @@ Fuel.legacy.dfy(324,21): Related location
 Fuel.legacy.dfy(313,41): Related location
 Fuel.legacy.dfy(335,26): Error: function precondition could not be proved
 Fuel.legacy.dfy(324,21): Related location
-Fuel.legacy.dfy(314,72): Related location


Someday I want to refactor this test so that the output doesn't get reordered every time we breathe on the verifier. :)

atomb · 2024-07-18T23:30:26Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-2026.dfy

        invariant forall j :: 0 <= j < i ==> j % 2 == 1 ==> ret[j] == "odd"
+        invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even"


I'm continually amazed by the edits that can resolve brittleness issues!

Yeah, here, I think it picked a different path or picked a different failing value for j.

... or what can cause them in the first place (here, some reordering of axioms in DafnyPrelude.bpl).

atomb · 2024-07-18T23:41:49Z

Source/DafnyCore/Prelude/Sequences.dfy

+  import opened Boxes
+
+  // boogie: type Seq;
+  type {:extract_name "Seq"} Seq = List<Box>


Suggested change

type {:extract_name "Seq"} Seq = List<Box>

type {:boogie_name "Seq"} Seq = List<Box>

And so on, elsewhere.

I changed :extract_name to :extract_boogie_name, and changed (the unused) :extract to :extract_boogie. I also modified the source to define these as constants in BoogieExtractor.cs, so they can easily be renamed in the future.

atomb · 2024-07-18T23:43:23Z

Source/DafnyCore/Prelude/Sequences.dfy

+  //   Seq#Contains(Seq#Drop(s, n), x) <==>
+  //     (exists i: int :: { Seq#Index(s, i) }
+  //       0 <= n && n <= i && i < Seq#Length(s) && Seq#Index(s, i) == x));
+  lemma {:extract_pattern Contains(Drop(s, n), x)} DropContains(s: Seq, n: int, x: Box)


I'm tempted to have a different name for this attribute, too, though I'm not sure what...

I left these as is. If we think of a better naming scheme in the future, we can change them then.

atomb · 2024-07-18T23:44:12Z

Source/DafnyCore/Backends/Extractor.cs

Maybe BoogieExtractor.cs?

atomb · 2024-07-18T23:49:20Z

Source/DafnyCore/Backends/Extractor.cs

+      return null;
+    }
+
+    private Boogie.Expr ExtractExpr(Expression expr) {


Is there a possibility of making this share more with the verifier?

It wasn't clear. For example, the verifier doesn't offer to rename types and functions using the extract names. At least the subset of Dafny used in these model files will be small.

One thing that is shared is the pretty printing of the Boogie itself. For example, BoogieExtractor.cs here does not need to worry about operator precedence in Boogie, since the Boogie pretty printer will add parentheses where they are needed.

Co-authored-by: Aaron Tomb <[email protected]>

# Conflicts: # Source/DafnyDriver/Commands/VerifyCommand.cs # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect

atomb

I'm excited about this!

# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

keyboardDrummer · 2024-09-04T13:34:13Z

I'm a bit spooked by the edits to SchorrWaite.dfy. The method SchorrWaite now has both {:isolate_assertions} and focus blocks, so I imagine there's large amount of assertions that are verified as asserts, multiple times.

keyboardDrummer · 2024-09-04T13:36:36Z

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -21,6 +22,13 @@ static VerifyCommand() {
    OptionRegistry.RegisterOption(FilterSymbol, OptionScope.Cli);
    OptionRegistry.RegisterOption(FilterPosition, OptionScope.Cli);
    OptionRegistry.RegisterOption(PerformanceStatisticsOption, OptionScope.Cli);
+    OptionRegistry.RegisterOption(ExtractTarget, OptionScope.Cli);
+
+    DafnyOptions.RegisterLegacyBinding(ExtractTarget, (options, f) => {


Why are we using the legacy way of introducing new options here?

Though I've tried, I still don't understand where to put these options to make them fire for the right commands. I would very much welcome an improvement of how extraction is handled. As mentioned above, it would be nice if it were a verb extract rather than an option for the verify verb.

keyboardDrummer · 2024-09-04T13:36:42Z

Source/DafnyDriver/Commands/VerifyCommand.cs

@@ -35,6 +43,13 @@ static VerifyCommand() {
  public static readonly Option<string> FilterPosition = new("--filter-position",
    @"Filter what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, `dafny verify dfyconfig.toml --filter-position=source1.dfy:5` will only verify things that range over line 5 in the file `source1.dfy`. In combination with `--isolate-assertions`, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: `dafny verify MyFile.dfy --filter-position=:23`");

+  public static readonly Option<string> ExtractTarget = new("--extract", @"
+Extract Dafny types, functions, and lemmas to Boogie.


What does this do? It's still not clear to me how this is different from --bprint. Does this ignore the input program and only output something relates to Dafny internals? If so, why is it part of dafny verify ?

Extraction is the output that the Dafny tool will incorporate into DafnyPrelude.bpl. These are not verification conditions but axioms and other definitions. In contrast, --bprint shows the verification conditions that are sent to Boogie.

To accomplish its task, extraction pays attention to :extract_boogie_name attributes and renames things accordingly. Extraction turns lemmas into universally quantified axioms (whereas VC generation turns them into Boogie procedures). Finally, extraction looks at the input Dafny expressions as they were Boogie expressions, more or less. So, the extraction output is free of well-formedness conditions and $Is predicates and other such things that are part of VC generation.

keyboardDrummer · 2024-09-04T13:37:16Z

Source/DafnyDriver/Commands/VerifyCommand.cs

+            var extractedProgram = BoogieExtractor.Extract(resolution.ResolvedProgram);
+            engine.PrintBplFile(options.BoogieExtractionTargetFile, extractedProgram, true, pretty: true);
+          } catch (ExtractorError extractorError) {
+            options.OutputWriter.WriteLine($"Boogie axiom extraction error: {extractorError.Message}");


Could you resolve these warnings?

Are you saying to remove this try catch? These errors are generated if the input to the extractor is invalid, so they need to stay.

No, the build was outputting warnings because this was using WriteLine instead of WriteLineAsync

Touchup PR for #5621 ### Description - Change the --extractTarget option into a hidden command - Make `--help` work when used on hidden commandds ### How has this been tested? - Ran `make extract` in DafnyCore <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>

RustanLeino added 30 commits July 10, 2024 21:36

Make some BoogieGenerator methods public

efb92f7

Add —extract option

655583a

Add beginning of extractor

69a233a

Add support for :extract_attribute

22f1043

Add support for :extract_used_by

8a09af0

Translate expressions

740cf74

Look for :extract on module

eaf91d8

Sort declarations from each module

c8c76ac

Remove debugging comment

0f2b6e2

Add scripts to generate prelude

1fc1aaa

Ignore files

727c9cd

chore: Mostly whitespace changes

01eeec5

Rename files to have better names

827bba1

Don’t include this generated file

8969d7a

chore: Change formatting to match generated

083e0d9

Move non-generated seq decls into Core file

5bd75ce

Don’t include this generated file

2e6bf6d

Change order of declarations

cbc6e87

chore: Change formatting

0fdae0d

chore: Name parameters

204fa36

Fix forall/exists distinction

88f563a

chore: Adjust formatting

589c6ac

Remove the used Seq#Singleton

005109e

chore: Add spaces after commas

3a8a234

chore: Remove trailing spaces

9855a01

Update formatting using pretty-printed Boogie

f98bde4

Fix extraction of logical not

fd3efe5

Adjust formatting

d0afb38

Fix order of pattern attributes in output

8a6902d

Adjust formatting

02c45ca

RustanLeino added 4 commits July 11, 2024 17:33

Merge branch 'master' into prelude-extractor

3abc19d

Add error handling

ecd4fdc

Enable some simplifications

c16a10f

Add release notes

797e4c9

parno mentioned this pull request Jul 12, 2024

Change Seq to an enum and verify its axioms verus-lang/verus#988

Draft

RustanLeino added 3 commits July 12, 2024 15:54

Format Dafny code

8d8d2c8

Account for order change of error messages

bfaa289

Use :isolate_assertions with SchorrWaite.dfy

f010720

The difference between the legacy/refresh resolver runs is that some bound variables and an empty set are typed with …Node… in legacy and …Node?… in refresh.

atomb requested changes Jul 18, 2024

View reviewed changes

RustanLeino and others added 5 commits August 20, 2024 14:18

Update Source/DafnyDriver/Commands/VerifyCommand.cs

3e126cc

Co-authored-by: Aaron Tomb <[email protected]>

Rename “Extractor” “BoogieExtractor”

4efe617

Overhaul the attribute names

c6e2015

Merge branch 'master' into prelude-extractor

cd87e9c

# Conflicts: # Source/DafnyDriver/Commands/VerifyCommand.cs # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.expect # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny1/SchorrWaite.dfy.refresh.expect

Adjust resource count in expect file

81c44f3

atomb previously approved these changes Aug 21, 2024

View reviewed changes

RustanLeino added 2 commits August 26, 2024 11:33

Merge branch 'master' into prelude-extractor

374d8c4

Merge branch 'master' into prelude-extractor

ac69f69

# Conflicts: # Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/SubsetTypes.dfy.expect

RustanLeino dismissed atomb’s stale review via ac69f69 August 28, 2024 21:32

RustanLeino added 2 commits August 29, 2024 12:36

Merge branch 'master' into prelude-extractor

26c98d1

Update resource counts for SchorrWaite.dfy

6a3f5f6

RustanLeino enabled auto-merge (squash) August 30, 2024 00:46

atomb approved these changes Aug 30, 2024

View reviewed changes

RustanLeino merged commit b3f70a8 into dafny-lang:master Aug 30, 2024
22 checks passed

keyboardDrummer reviewed Sep 4, 2024

View reviewed changes

RustanLeino deleted the prelude-extractor branch September 27, 2024 17:39

keyboardDrummer mentioned this pull request Sep 30, 2024

Change the --extractTarget option into a command #5799

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: Prelude extractor #5621

feat: Prelude extractor #5621

RustanLeino commented Jul 12, 2024

atomb left a comment

atomb Jul 18, 2024

atomb Jul 18, 2024

RustanLeino Aug 20, 2024

atomb Jul 18, 2024

atomb Jul 18, 2024

RustanLeino Aug 20, 2024

RustanLeino Aug 20, 2024

atomb Jul 18, 2024

atomb Jul 18, 2024

RustanLeino Aug 20, 2024

atomb Jul 18, 2024

RustanLeino Aug 20, 2024

atomb Jul 18, 2024

atomb Jul 18, 2024

RustanLeino Aug 20, 2024

atomb left a comment

keyboardDrummer commented Sep 4, 2024

keyboardDrummer Sep 4, 2024

RustanLeino Sep 27, 2024

keyboardDrummer Sep 4, 2024

RustanLeino Sep 27, 2024

keyboardDrummer Sep 4, 2024

RustanLeino Sep 27, 2024

keyboardDrummer Sep 30, 2024

		invariant forall j :: 0 <= j < i ==> j % 2 == 1 ==> ret[j] == "odd"
		invariant forall j :: 0 <= j < i ==> j % 2 == 0 ==> ret[j] == "even"

	type {:extract_name "Seq"} Seq = List<Box>
	type {:boogie_name "Seq"} Seq = List<Box>

feat: Prelude extractor #5621

feat: Prelude extractor #5621

Conversation

RustanLeino commented Jul 12, 2024

Description

Impact on the Dafny tool

CLI option

Changes to DafnyPrelude.bpl

Extract mechanism

Expressions

Soundness

atomb left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

atomb left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Sep 4, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Changes to `DafnyPrelude.bpl`