Experimenting with no CanConsume

Author: robin-aws

src/Actions/Actions.dfy

@@ -23,12 +23,13 @@ module Actions {
         && CanProduce(consumed, produced)
       decreases height, 0
 
-    ghost predicate CanConsume(consumed: seq<T>, produced: seq<R>, next: T)
-      requires CanProduce(consumed, produced)
+    ghost predicate CanProduce(ins: seq<T>, outs: seq<R>)
       decreases height
 
-    ghost predicate CanProduce(consumed: seq<T>, produced: seq<R>)
+    ghost predicate CanConsume(ins: seq<T>, outs: seq<R>, nextIn: T)
       decreases height
+      ensures CanConsume(ins, outs, nextIn)
+        <==> exists nextOut :: CanProduce(ins + [nextIn], outs + [nextOut])
 
     ghost method Update(t: T, r: R) 
       modifies `consumed, `produced
@@ -41,7 +42,7 @@ module Actions {
 
     method Invoke(t: T) returns (r: R) 
       requires Valid()
-      requires CanConsume(consumed, produced, t)
+      requires exists r :: CanProduce(consumed + [t], produced + [r])
       modifies Repr
       decreases height
       ensures Valid()

src/Actions/Enumerators.dfy

@@ -92,12 +92,14 @@ module Enumerators {
       e.CanProduce(consumed, produced) ==> exists n: nat | n <= limit :: Terminated(produced, None, n)
   }
 
-  ghost predicate ConsumesAnything<T(!new)>(a: Action<(), Option<T>>) {
-    forall consumed, produced, next | a.CanProduce(consumed, produced) :: a.CanConsume(consumed, produced, next)
+  ghost predicate ConsumesAnything<T(!new), R(!new)>(a: Action<T, R>, ins: seq<T>, outs: seq<R>, nextIn: T) 
+    requires a.CanProduce(ins, outs)
+  {
+    exists nextOut :: a.CanProduce(ins + [nextIn], outs + [nextOut])
   }
 
   ghost predicate IsEnumerator<T(!new)>(a: Action<(), Option<T>>) {
-    && ConsumesAnything(a)
+    && forall ins, outs, nextIn | a.CanProduce(ins, outs) :: ConsumesAnything(a, ins, outs, nextIn)
     && exists limit :: EnumerationBoundedBy(a, limit)
   }
 
@@ -207,11 +209,6 @@ module Enumerators {
       Repr := {this};
     }
 
-    ghost predicate CanConsume(consumed: seq<()>, produced: seq<Option<T>>, next: ()) 
-      decreases height
-    {
-      true
-    }
     ghost predicate CanProduce(consumed: seq<()>, produced: seq<Option<T>>) 
       decreases height
     {
@@ -223,7 +220,7 @@ module Enumerators {
 
     method Invoke(t: ()) returns (r: Option<T>) 
       requires Valid()
-      requires CanConsume(consumed, produced, t)
+      requires exists r :: CanProduce(consumed + [t], produced + [r])
       modifies Repr
       decreases height
       ensures Valid()
@@ -285,11 +282,6 @@ module Enumerators {
       Repr := {this};
     }
 
-    ghost predicate CanConsume(consumed: seq<()>, produced: seq<T>, next: ()) 
-      decreases height
-    {
-      |consumed| + 1 <= |elements|
-    }
     ghost predicate CanProduce(consumed: seq<()>, produced: seq<T>) 
       decreases height
     {
@@ -298,7 +290,7 @@ module Enumerators {
 
     method Invoke(t: ()) returns (r: T) 
       requires Valid()
-      requires CanConsume(consumed, produced, t)
+      requires exists r :: CanProduce(consumed + [t], produced + [r])
       modifies Repr
       decreases height
       ensures Valid()
@@ -325,6 +317,11 @@ module Enumerators {
       decreases EnumerationTerminationMetric(e2)
     {
       label beforeLoop: 
+
+      assert IsEnumerator(e2);
+      assert e2.CanProduce(e2.consumed, e2.produced);
+      assert ConsumesAnything(e2, e2.consumed, e2.produced, ());
+      assert exists r :: e2.CanProduce(e2.consumed + [()], e2.produced + [r]);
       var next: Option<int> := e2.Invoke(());
       if next.None? { break; }
       EnumerationTerminationMetricDecreased@beforeLoop(e2, next);

src/Actions/MappingEnumerator.dfy

@@ -53,11 +53,6 @@ module Mapped {
       assert ValidWrappedProduced(consumed, produced, wrapped.produced);
     }
 
-    ghost predicate CanConsume(consumed: seq<()>, produced: seq<Option<R>>, next: ())
-      decreases height
-    {
-      true
-    }
     ghost predicate CanProduce(consumed: seq<()>, produced: seq<Option<R>>)
       decreases height
     {
@@ -71,7 +66,7 @@ module Mapped {
 
     method Invoke(t: ()) returns (r: Option<R>) 
       requires Valid()
-      requires CanConsume(consumed, produced, t)
+      requires exists r :: CanProduce(consumed + [t], produced + [r])
       modifies Repr
       decreases height
       ensures Valid()