feat: Actions, Frames, Termination, and Ordinal standard libraries #6074

robin-aws · 2025-01-24T00:41:18Z

What was changed?

See Std/Actions/Actions.md etc.

Also:

Fixed a Java code generation bug I happened to hit (partial fix to Java tries to use unboxed primitive types for type parameters in trait method overrides #6147)
Added a nondeterministic sub-project to examples, for code that isn't valid in --enforce-determinism mode

How has this been tested?

See ActionsExamples.dfy etc.

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

…-streaming-stdlibs

…-streaming-stdlibs # Conflicts: # Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy

…-streaming-stdlibs

…-streaming-stdlibs # Conflicts: # Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs # Source/DafnyStandardLibraries/Makefile # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-cs.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-go.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-java.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-js.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-notarget.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries-py.doo # Source/DafnyStandardLibraries/binaries/DafnyStandardLibraries.doo

…/dafny into actions-and-streaming-stdlibs

…-streaming-stdlibs

RustanLeino

This is a substantial amount of very nice work. I have some comments, but they can easily be addressed.

RustanLeino · 2025-04-05T00:14:37Z

Source/DafnyStandardLibraries/examples/FramesExamples.dfy

+        nodeCount := left.nodeCount + right.nodeCount + 1;
+      }
+
+      if (right is Node<T>) {


No need for parentheses

RustanLeino · 2025-04-05T00:15:50Z

Source/DafnyStandardLibraries/examples/Actions/ActionsExamples.dfy

+    }
+
+    ghost predicate ValidInput(history: seq<((), Box)>, next: ())
+      requires ValidHistory(history)


Precondition not necessary in this override, but I agree it's good style to include it here. Especially since these examples will serve as a guide to other subtypes.

RustanLeino · 2025-04-05T00:18:53Z

Source/DafnyStandardLibraries/examples/nondeterministic/ActionsExamples.dfy

+  import opened Std.Wrappers
+
+
+  // Adapting an iterator to a producer


Nice inclusion.

I do still want to add an example of enumerating a codatatype, but I'll include that in the next batch of changes to this library.

RustanLeino · 2025-04-05T00:21:13Z

Source/DafnyStandardLibraries/examples/nondeterministic/ActionsExamples.dfy

+    {
+      this.iter := new FibonacciIterator();
+      new;
+      Repr := {this, iter} + NonNullElements(iter._reads) + NonNullElements(iter._modifies) + NonNullElements(iter._new);


Hmm, so the type of _reads, _modifies, and _new is set<object?>? That must be legacy from before Dafny had non-null types. Good for now here, but this would be nice (as easy, I imagine) to change in Dafny.

Yeah I was surprised too. Probably not worth changing by itself, but worth changing if and when we revamp iterators in general.

RustanLeino · 2025-04-05T00:22:07Z

Source/DafnyStandardLibraries/examples/nondeterministic/ActionsExamples.dfy

+
+  }
+
+  method {:test} FibonnaciExample() {


spelling (Fibonacci)

RustanLeino · 2025-04-05T00:59:54Z

Source/DafnyStandardLibraries/src/Std/Frames.dfy

+    // TODO: Okay it's now or never - Repr or repr?? :)
+    ghost var Repr: set<object>


My vote is for Repr. It's an abstraction of something and it is something that public clients need to know about. For example, a class that implements a set would probably declare ghost var Elements: set<T>.

So it sounds like you'd like to amend the Dafny style guide to add a clause something like:

"Any fields or constants that public clients may reference are named with PascalCase, and camelCase otherwise. This includes at least all symbols included in at least one export set."

The style guide currently doesn't say anything about fields and non-static constants, and I think most users have inferred that they should always be camelCase. The existing standard library code is already not consistent -for example DynamicArray has:

ghost var items: seq<A> ghost var Repr: set<object>

I'll definitely keep Repr here, but independently we should clarify this point and then go back and align the code better throughout (possibly as part of Dafny 5.0 since we may want change symbols that may already be in use).

RustanLeino · 2025-04-05T01:03:36Z

Source/DafnyStandardLibraries/src/Std/Frames.dfy

+    // TODO: Similarly, would Invariant() be better?
+    ghost predicate Valid()


I vote for Valid. The intention is that the condition be invariant, but it describes what it means for the data structure to be valid. Also, it's a bit funny to say that a method "requires and ensures the invariant", since it's the fact that the method "requires and ensures X" that makes X an invariant in the first place.

RustanLeino · 2025-04-05T01:06:46Z

Source/DafnyStandardLibraries/src/Std/Ordinal.dfy

+    ensures forall result' {:trigger} |
+              forall right' | right' < right :: Plus(left, right') < result' :: result <= result'


The fact that you're using {:trigger} here suggests to me that Dafny doesn't recognize that <= on ORDINAL would be acceptable as a trigger. We should consider extending Dafny to do that.

I'd definitely love to consider adding more axioms and operations on ordinals in the future in general, but only if we think anything besides this module would benefit.

RustanLeino · 2025-04-05T01:08:20Z

Source/DafnyStandardLibraries/src/Std/Ordinal.dfy

+    ensures a < b <==> a + 1 <= b
+
+  ghost function {:axiom} PlusLimit(left: ORDINAL, right: ORDINAL): (result: ORDINAL)
+    decreases right, 0


I usually write the decreases clause after requires, reads, modifies, and ensures. If you feel the same, feel free to make that change here and below.

For the record I've actually always preferred this order:

requires ... reads ... modifies ... decreases ... ensures ...

Mainly because I think of it "chronologically", and it feels like the decreases is relevant "during" the evaluation to ensure termination, and the ensures is relevant "after".

But I do see that the style guide agrees with you so I'm happy to align. :)

I see. That's a decent rule. For the record, here are two other thoughts on this matter:

I, too, think of requires as happening before reads, but the language design is actually to allow the two to be mutually dependent. For example,

class Cell { var data: int } function F(a: array<Cell>, i: nat): int requires i < a.Length && a[i].data == 10 reads a, a[i]

I think the reason I've placed decreases last is because it feels relevant to the implementation of the function/method, not so much to the caller. This makes sense for a function/method M that is in its own SCC and is itself recursive. But for a caller that's mutually recursive with M, the decreases clause of M is part of the specification that a caller needs to know about.

RustanLeino · 2025-04-05T01:22:37Z

Source/DafnyStandardLibraries/src/Std/Termination.dfy

+    // parent is a MaxOrdinal() parameter just to prove termination,
+    // but doesn't affect the actual result.


This comment would be good on MaxOrdinal as well.

…-streaming-stdlibs

robin-aws added 30 commits May 20, 2024 15:20

Just Action trait (doesn’t verify yet)

31afc77

Use DynamicArray in ArrayAggregator

9ed2550

Fix verification

c7a97c7

Another type characteristic requirement bites the dust

813912f

—function-syntax

4162f32

More function-syntax

02ebe4b

Sketching out Enumerable<T> trait

6f7fa28

Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

a6a245f

…-streaming-stdlibs

Fresh snapshot

83fc0f3

Fixed loop

9d71295

Very cool SetEnumerator example

56776c8

Tweaks

d5aaabc

Aggregators and Enumerators mostly verifying

5395c16

ProducesSetProof

1732277

Disable verification in a few places for now

a320930

Another one

9ed029a

Lift some common things up

b25c48a

Missing postconditions

38702a2

Comment

5e91c5f

Missing ghost

d57c9ea

Commenting out some code that doesn't work for Rust

153a282

Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

7f583cd

…-streaming-stdlibs # Conflicts: # Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy

Add streams as well

0dadc06

Fix names

3482109

Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

fb6199e

…-streaming-stdlibs

Fix verification after CanCall change

d9c5fcb

Uncomment Folder

ad032b0

CanCall fixes

0184e8f

One more

4abfd81

Typo

66cd68d

robin-aws reopened this Mar 25, 2025

robin-aws added 2 commits March 25, 2025 15:40

Fixes

341259d

robin-aws changed the title ~~feat: Actions, Frames, and Termination standard libraries (temp closed to avoid CI)~~ feat: Actions, Frames, and Termination standard libraries Mar 26, 2025

robin-aws added 11 commits March 26, 2025 09:22

Fix type-system-refresh regressions

dd5abe6

Merge branch 'master' into actions-and-streaming-stdlibs

aaa0f47

Remove example from source

bfadc5d

Merge branch 'actions-and-streaming-stdlibs' of github.com:dafny-lang…

a0eea70

…/dafny into actions-and-streaming-stdlibs

Remove height, extract Ordinal module and progress on proofs

aeb6810

Lots of progress on proving oridinal lemmas

17f577e

Progressed but found typo, capturing state before reverting to axioms

cc2bf6a

Flip Ordinal arguments to use < and <= instead

ed3c74c

Remove TerminationMetric.Valid(), improve resource limits

72d4553

Improve Producers verification efficiency

38a1d3b

docs and formatting

74fe8b6

robin-aws changed the title ~~feat: Actions, Frames, and Termination standard libraries~~ feat: Actions, Frames, Termination, and Ordinal standard libraries Mar 31, 2025

robin-aws added 3 commits March 31, 2025 16:16

Release note, fix examples

ade6bff

Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

685ef64

…-streaming-stdlibs

Cleanup, removing unneeded assertions

d8b24c5

RustanLeino requested changes Apr 5, 2025

View reviewed changes

robin-aws added 3 commits April 7, 2025 11:26

PR feedback

3430798

Merge branch 'master' of github.com:dafny-lang/dafny into actions-and…

5000d77

…-streaming-stdlibs

Poke CI

e55f545

robin-aws enabled auto-merge (squash) April 7, 2025 21:52

Merge branch 'master' into actions-and-streaming-stdlibs

b2fee27

RustanLeino approved these changes Apr 7, 2025

View reviewed changes

robin-aws merged commit 713a07b into master Apr 7, 2025
22 checks passed

robin-aws deleted the actions-and-streaming-stdlibs branch April 7, 2025 23:32

robin-aws mentioned this pull request Apr 9, 2025

Ordered quantification (foreach loops and sequence comprehensions - take 2) dafny-lang/rfcs#10

Open

botantony mentioned this pull request Aug 26, 2025

dafny 4.11.0 Homebrew/homebrew-core#234941

Merged

		import opened Std.Wrappers


		// Adapting an iterator to a producer

		// TODO: Okay it's now or never - Repr or repr?? :)
		ghost var Repr: set<object>

		// TODO: Similarly, would Invariant() be better?
		ghost predicate Valid()

		ensures forall result' {:trigger} \|
		forall right' \| right' < right :: Plus(left, right') < result' :: result <= result'

		// parent is a MaxOrdinal() parameter just to prove termination,
		// but doesn't affect the actual result.

feat: Actions, Frames, Termination, and Ordinal standard libraries #6074

feat: Actions, Frames, Termination, and Ordinal standard libraries #6074

Uh oh!

Conversation

robin-aws commented Jan 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What was changed?

How has this been tested?

Uh oh!

RustanLeino left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

robin-aws commented Jan 24, 2025 •

edited

Loading