feat: Actions and streaming standard libraries

Source/DafnyStandardLibraries/README.md

@@ -30,8 +30,6 @@ When using this option with commands like `dafny translate`, `dafny build`, or `
 the contents of the standard libraries will be automatically included in the translated source code as well. 
 This causes conflicts when multiple such translated projects are combined. When combining such projects, please ensure that only one of them has `--translate-standard-library` set to true. 
 
-To combine multiple Dafny projects that were separately built, and were  
-
 Some libraries are dependent on target language utilities, such as `FileIO`.
 When `--standard-libraries` is on,
 the translation process will also include some additional supporting target language source files,
@@ -47,13 +45,15 @@ In particular, `--standard-libraries` currently cannot be used together with `--
 
 The sections below describe how to use each library:
 
+- [Std.Actions](src/Std/Actions/README.md) -- utilities for abstract imperative actions, including enumerating and streaming values
 - [Std.Arithmetic](src/Std/Arithmetic/README.md) -- utilities and lemmas related to basic operations, such as multiplication and exponentiation
 - [Std.Base64](src/Std/Base64.md) -- base-64 encoding and decoding
 - [Std.BoundedInts](src/Std/BoundedInts.md) -- definitions of types and constants for fixed-bit-width integers
 - [Std.Collections](src/Std/Collections/Collections.md) -- properties of the built-in collection types (seq, set, iset, map, imap, array)
 - [Std.Concurrent](src/Std/TargetSpecific) -- types for using Dafny in concurrent environments
 - [Std.DynamicArray](src/Std/DynamicArray.dfy) -- an array that can grow and shrink
 - [Std.FileIO](src/Std/TargetSpecific) -- basic file I/O operations
+- [Std.Frames](src/Std/Frames.md) -- utilities related to working with dynamic framing, often related to reads and modifies clauses
 - [Std.Functions](src/Std/Functions.md) -- properties of functions
 - [Std.JSON](src/Std/JSON/JSON.md) -- JSON serialization and deserialization
 - [Std.Math](src/Std/Math.md) -- common mathematical functions, such as Min and Abs

Source/DafnyStandardLibraries/examples/Actions/ActionsExamples.dfy

@@ -0,0 +1,177 @@
+module ActionsExamples {
+  import opened Std.Actions
+  import opened Std.Enumerators
+  import opened Std.Aggregators
+  import opened Std.Wrappers
+
+  class Box {
+    const i: nat
+
+    constructor(i: nat)
+      reads {}
+      ensures this.i == i
+    {
+      this.i := i;
+    }
+  }
+
+  function SeqRange(n: nat): seq<nat> {
+    seq(n, i => i)
+  }
+
+  lemma SeqRangeIncr(prefix: seq<nat>, n: nat)
+    requires prefix == SeqRange(n)
+    ensures prefix + [n] == SeqRange(n + 1)
+  {}
+
+  @AssumeCrossModuleTermination
+  class BoxEnumerator extends Action<(), Box> {
+
+    var nextValue: nat
+
+    ghost predicate Valid()
+      reads this, Repr
+      ensures Valid() ==> this in Repr
+      ensures Valid() ==> CanProduce(history)
+      decreases height, 0
+    {
+      && this in Repr
+      && CanProduce(history)
+      && nextValue == |history|
+    }
+
+    constructor()
+      ensures Valid()
+      ensures fresh(Repr)
+      ensures history == []
+    {
+      nextValue := 0;
+      history := [];
+      Repr := {this};
+      height := 1;
+    }
+
+    ghost predicate CanConsume(history: seq<((), Box)>, next: ())
+      decreases height
+    {
+      true
+    }
+    ghost predicate CanProduce(history: seq<((), Box)>)
+      decreases height
+    {
+      Seq.Map((b: Box) => b.i, Outputs(history)) == SeqRange(|history|)
+    }
+
+    method Invoke(t: ()) returns (r: Box)
+      requires Requires(t)
+      reads Reads(t)
+      modifies Modifies(t)
+      decreases Decreases(t).Ordinal()
+      ensures Ensures(t, r)
+    {
+      assert Requires(t);
+      ghost var producedBefore := Produced();
+
+      r := new Box(nextValue);
+      Update(t, r);
+      Repr := {this};
+      nextValue := nextValue + 1;
+
+      SeqRangeIncr(Seq.Map((b: Box) => b.i, producedBefore), |producedBefore|);
+      assert Valid();
+    }
+
+    method RepeatUntil(t: (), stop: Box -> bool, ghost eventuallyStopsProof: ProducesTerminatedProof<(), Box>)
+      requires Valid()
+      requires eventuallyStopsProof.Action() == this
+      requires eventuallyStopsProof.FixedInput() == t
+      requires eventuallyStopsProof.StopFn() == stop
+      requires forall i <- Consumed() :: i == t
+      reads Repr
+      modifies Repr
+      decreases Repr
+      ensures Valid()
+    {
+      DefaultRepeatUntil(this, t, stop, eventuallyStopsProof);
+    }
+  }
+
+  method {:rlimit 0} BoxEnumeratorExample() {
+    var enum: BoxEnumerator := new BoxEnumerator();
+    assert |enum.Produced()| == 0;
+    var a := enum.Invoke(());
+
+    assert enum.Produced() == [a];
+    assert Seq.Map((b: Box) => b.i, enum.Produced()) == SeqRange(1) == [0];
+    // assert a.i == 0;
+
+    // var b := enum.Invoke(());
+    // var c := enum.Invoke(());
+    // var d := enum.Invoke(());
+    // var e := enum.Invoke(());
+  }
+
+  method SetEnumeratorExample() {
+    var s: set<nat> := {1, 2, 3, 4, 5};
+    var copy: set<nat> := {};
+    var e: SetEnumerator<nat> := new SetEnumerator(s);
+
+    label before:
+    for enumerated := 0 to 5
+      invariant e.Valid()
+      invariant enumerated == |e.history|
+      invariant fresh(e.Repr - old@before(e.Repr))
+    {
+      var x := e.Invoke(());
+      copy := copy + {x};
+    }
+
+    // TODO: cool enough that we can statically invoke
+    // the enumerator the right number of times!
+    // But now prove that copy == s!
+    // assert |copy| == 5;
+    // assert copy == s;
+  }
+
+  method {:rlimit 0} AggregatorExample() {
+    var a: ArrayAggregator<nat> := new ArrayAggregator();
+    var _ := a.Invoke(1);
+    var _ := a.Invoke(2);
+    var _ := a.Invoke(3);
+    var _ := a.Invoke(4);
+    var _ := a.Invoke(5);
+    var _ := a.Invoke(6);
+    assert a.Consumed() == [1, 2, 3, 4, 5, 6];
+    assert a.storage.items == [1, 2, 3, 4, 5, 6];
+  }
+
+  @AssumeCrossModuleTermination
+  class ExamplePipeline<T> extends Pipeline<T, T> {
+    constructor(upstream: Enumerator<T>)
+      requires upstream.Valid()
+      ensures Valid()
+    {
+      this.upstream := upstream;
+      var buffer := new Collector<T>();
+
+      Repr := {this} + upstream.Repr + buffer.Repr;
+      history := [];
+      this.buffer := buffer;
+      this.height := upstream.height + buffer.height + 1;
+    }
+
+    method Process(u: Option<T>, a: Accumulator<T>)
+      requires a.Valid()
+      reads a.Repr
+      modifies a.Repr
+      ensures a.ValidAndDisjoint()
+    {
+      assert a.Valid();
+
+      if u.Some? {
+        a.CanConsumeAll(a.history, u.value);
+        a.Accept(u.value);
+      }
+    }
+  }
+}