fix: check for at least one message in object RL (#108)

- Closes #106

---------

Co-authored-by: Copilot <[email protected]>

Author: lukaszcz

AVM/Class/Translation/Logics.lean

@@ -67,18 +67,23 @@ private def Method.Message.logicFun
     && Logic.checkResourcesPersistent consumedResObjs
     && Logic.checkResourcesPersistent createdResObjs
 
-/-- The class logic checks if all consumed messages in the action correspond
-  to class members and the single consumed object is the receiver. -/
+/-- The class logic checks if all consumed messages in the action correspond to
+    class members, the single consumed object is the receiver, and there is
+    at least one message. -/
 private def logicFun {lab : Ecosystem.Label} {classId : lab.ClassId} (cl : Class classId) (args : Logic.Args) : Bool :=
   let try self : Object classId.label := Object.fromResource args.self
   check cl.invariant self args
   match args.status with
   | Created => true
   | Consumed =>
     let consumedMessageResources : List Anoma.Resource := Logic.selectMessageResources args.consumed
+    let nMessages := consumedMessageResources.length
     let! [consumedObjectResource] : List Anoma.Resource := Logic.selectObjectResources args.consumed
     let try consumedObject : Object classId.label := Object.fromResource consumedObjectResource
-    consumedMessageResources.length + 1 == (Logic.filterOutDummy args.consumed).length
+    -- NOTE: consumedObject == self by definition of Logic.Args; we only check
+    -- that there are no other consumed objects
+    nMessages >= 1
+      && nMessages + 1 == (Logic.filterOutDummy args.consumed).length
       && consumedMessageResources.all fun res =>
         let try msg : Message classId.label := Message.fromResource res
         consumedObject.uid == msg.recipient

AVM/Logic.lean

@@ -34,7 +34,7 @@ def checkResourcesPersistent (resources : List Anoma.Resource) : Bool :=
   Logic.filterOutDummy resources |>.all Anoma.Resource.isPersistent
 
 def selectObjectResources.{u, v} (resources : List Anoma.Resource.{u, v}) : List Anoma.Resource.{u, v} :=
-  resources.filter Resource.isSomeObject.{u, v, v}
+  resources.filter Resource.isSomeObject.{u, v}
 
 def selectMessageResources.{u, v} (resources : List Anoma.Resource.{u, v}) : List Anoma.Resource.{u, v} :=
   resources.filter Resource.isSomeMessage

AVM/Object.lean

@@ -106,13 +106,13 @@ def Object.fromResource
           data := ⟨res.quantity, value.privateFields⟩,
           nonce := res.nonce }
 
-def SomeObject.fromResource
-  (res : Anoma.Resource)
-  : Option SomeObject :=
+def SomeObject.fromResource.{u, v}
+  (res : Anoma.Resource.{u, v})
+  : Option SomeObject.{max u v + 1} :=
   let try resLab : Object.Resource.Label := tryCast res.label
   let lab : Class.Label := resLab.classLabel
   let try obj := @Object.fromResource lab res
   some {label := lab, object := obj}
 
-def Resource.isSomeObject.{u, v, w} (res : Anoma.Resource.{u, v}) : Bool :=
-  Option.isSome (SomeObject.fromResource.{u, v, w} res)
+def Resource.isSomeObject.{u, v} (res : Anoma.Resource.{u, v}) : Bool :=
+  Option.isSome (SomeObject.fromResource.{u, v} res)