feat: Actions and streaming standard libraries #6074
Conversation
…-streaming-stdlibs
…-streaming-stdlibs # Conflicts: # Source/DafnyStandardLibraries/src/Std/Collections/Seq.dfy
…-streaming-stdlibs
…/dafny into actions-and-streaming-stdlibs
robin-aws
changed the title
| @@ -774,6 +774,25 @@ module Std.Collections.Seq { | |||
| } | |||
| } | |||
|
|
|||
| lemma {:induction false} LemmaMapPartialFunctionDistributesOverConcat<T,R>(f: (T --> R), xs: seq<T>, ys: seq<T>) | |||
There was a problem hiding this comment.
I found this was necessary because MapPartialFunction was introduced, not sure if there's a better solution?
| ghost predicate Valid() | ||
| reads this, Repr | ||
| ensures Valid() ==> this in Repr | ||
| ensures Valid() ==> CanProduce(history) |
There was a problem hiding this comment.
(This is the first occurrences of CanProduce I see, so maybe the answer to my thought will be clear to me later, but) my first impression is that CanProduce ought to be separate from Valid
| && nextValue == |history| | ||
| } | ||
|
|
||
| constructor() |
There was a problem hiding this comment.
Code style: constructor() looks like JavaScript to me. I would have written it with a space before the (), just like a named constructor constructor Init() but with an empty-string name.
| for enumerated := 0 to 5 | ||
| invariant e.Valid() | ||
| invariant enumerated == |e.history| | ||
| invariant fresh(e.Repr - old@before(e.Repr)) |
There was a problem hiding this comment.
Is old@before(e.Repr) all fresh as well? If so, you could just write fresh(e.Repr).
| // but this case seems less useful in practice, | ||
| // so the definition of a MostlyGenericFunction | ||
| // that may only modify the heap deterministically | ||
| // is left as an invitation to the sufficiently motivated Dafny contributor!) |
| // the CanConsume and CanProduce predicates, | ||
| // which the action's specification of behavior are drawn from, | ||
| // specifically avoid reading the current state of the action. | ||
| // That is so extrisnic properties of an action do NOT depend on their current state. |
There was a problem hiding this comment.
| // That is so extrisnic properties of an action do NOT depend on their current state. | |
| // That is so extrinsic properties of an action do NOT depend on their current state. |
| // | ||
| // The downside is that these are then forced to use quantifiers | ||
| // to talk about all possible states of an action. | ||
| // The solution is the trait proof pattern, |
There was a problem hiding this comment.
Nice. (I have yet to review it, but this sounds like a nice idea.)
| // 1. An Action<T, Option<R>> can produce None to indicate there is no value, | ||
| // but the action could still be called again. Similarly a Result<R, E> | ||
| // output could indicate a failure that is only related to that invocation. |
There was a problem hiding this comment.
Under this option, is a subsequent invocation of the action obligated/guaranteed to produce "no value" again?
There was a problem hiding this comment.
Oh, the next bullets answer my question--it depends on what kind of Action it is.
| reads this, Repr | ||
| ensures Valid() ==> this in Repr | ||
| ensures Valid() ==> CanProduce(history) | ||
| decreases height, 0 |
There was a problem hiding this comment.
Where is height declared? I don't see it here and I don't see it in either GenericAction or Validatable.
There was a problem hiding this comment.
| history := history + [(t, r)]; | ||
| } | ||
|
|
||
| ghost function Consumed(): seq<T> |
There was a problem hiding this comment.
I'm reading the names Consumed() and Produced() as if they were returned a boolean (like Terminated() below). A slightly longer name, but possibly better at resolving such ambiguity, is ConsumedSoFar() (and ProducedSoFar()). Hmm, maybe those have the same problem. Maybe ConsumptionHistory or ConsumeHistory? Or ElementsConsumed (but "elements" is not quite right)?
| modifies a.Repr | ||
| ensures a.Valid() | ||
| { | ||
| while (true) |
There was a problem hiding this comment.
| while (true) | |
| while true |
| ensures Terminated(left + right, stop, |left| + n) | ||
| {} | ||
|
|
||
| lemma TerminatedUndistributes<T>(left: seq<T>, right: seq<T>, stop: T -> bool, n: nat) |
There was a problem hiding this comment.
Instead of ...Distributes and ...Undistributes, consider ...Composition and ...Decomposition.
| assert StopFn()(before[|before| - 1]); | ||
| assert !StopFn()(Action().Produced()[|Action().Produced()| - 1]); | ||
| assert |Action().Produced()| <= m; | ||
| assert !StopFn()(Action().Produced()[|before| - 1]); | ||
| assert false; |
There was a problem hiding this comment.
Alternatively, this could be formulated as
assert false by {
// the other 4 asserts
}| case Some(result) => { | ||
| var (newState, result') := result; |
There was a problem hiding this comment.
This looks nice. But if you prefer, it should also be possible to write it with a nested pattern:
case Some((newState, result')) =>Also, note that the curly braces around an entire case body is never necessary, because each case is already a block scope by itself.
(Still WIP but worth a first review pass)
What was changed?
See documentation.
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.