fix resource logic functions

Author: lukaszcz

AVM/Class/Translation/Logics.lean

@@ -18,8 +18,10 @@ private def Constructor.Message.logicFun
   let newObjData := constr.body argsData |>.value vals
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
-  Logic.checkResourcesData [newObjData.toSomeObjectData] consumedResObjs
-    && Logic.checkResourcesData [newObjData.toSomeObjectData] createdResObjs
+  let! [newObjRes] := createdResObjs
+  let uid : ObjectId := newObjRes.nonce.value
+  Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs
+    && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs
     && Logic.checkResourcesEphemeral consumedResObjs
     && Logic.checkResourcesPersistent createdResObjs
     && constr.invariant argsData
@@ -38,7 +40,7 @@ private def Destructor.Message.logicFun
   let createdResObjs := Logic.selectObjectResources args.created
   let! [selfRes] := consumedResObjs
   let try selfObj : Object classId.label := Object.fromResource selfRes
-  Logic.checkResourcesData [selfObj.toSomeObjectData] createdResObjs
+  Logic.checkResourceValues [selfObj.toObjectValue] createdResObjs
     && Logic.checkResourcesPersistent consumedResObjs
     && Logic.checkResourcesEphemeral createdResObjs
     && destructor.invariant selfObj argsData
@@ -61,7 +63,7 @@ private def Method.Message.logicFun
   let body := method.body selfObj argsData
   let try vals : body.params.Product := tryCast msg.vals
   let createdObject : Object classId.label := body |>.value vals
-  Logic.checkResourcesData [createdObject.toSomeObjectData] createdResObjs
+  Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs
     && Logic.checkResourcesPersistent consumedResObjs
     && Logic.checkResourcesPersistent createdResObjs
 
@@ -111,5 +113,3 @@ def Method.Message.logic
 def logic {lab : Ecosystem.Label} {classId : lab.ClassId} (cl : Class classId) : Anoma.Logic :=
   { reference := classId.label.logicRef,
     function := logicFun cl }
-
-end AVM.Class

AVM/Logic.lean

@@ -11,20 +11,21 @@ def filterOutDummy (resources : List Anoma.Resource.{u, v}) : List Anoma.Resourc
   resources.filter (not ∘ Action.isDummyResource)
 
 /-- Checks that the number of objects and resources match, and that the
-    resources' quantity, value and labels match the objects' data and labels.
-    This check is used in the constructor and method message logics. Dummy resources
-    in the `resources` list are ignored. -/
-def checkResourcesData (objectData : List SomeObjectData) (resources : List Anoma.Resource) : Bool :=
+    quantity, value and labels of each resource match the corresponding object.
+    This check is used in the constructor, destructor and method message logics.
+    Dummy resources in the `resources` list are ignored. -/
+def checkResourceValues (objectValues : List ObjectValue) (resources : List Anoma.Resource) : Bool :=
   let resources' := Logic.filterOutDummy resources
-  objectData.length == resources'.length
-    && List.and (List.zipWith resourceDataEq objectData resources')
+  objectValues.length == resources'.length
+    && List.and (List.zipWith resourceValueEq objectValues resources')
   where
-    resourceDataEq (sdata : SomeObjectData) (res : Anoma.Resource) : Bool :=
+    resourceValueEq (sdata : ObjectValue) (res : Anoma.Resource) : Bool :=
       sdata.label === res.label &&
       sdata.label.logicRef == res.logicRef &&
       sdata.data.quantity == res.quantity &&
-        let try privateFields := tryCast sdata.data.privateFields
-        res.value == privateFields
+        let try resVal : Object.Resource.Value sdata.label := tryCast res.value
+        resVal.privateFields == sdata.data.privateFields &&
+        resVal.uid == sdata.uid
 
 def checkResourcesEphemeral (resources : List Anoma.Resource) : Bool :=
   Logic.filterOutDummy resources |>.all Anoma.Resource.isEphemeral

AVM/Object.lean

@@ -16,17 +16,13 @@ instance ObjectData.inhabited (lab : Class.Label) : Inhabited (ObjectData lab) w
 instance ObjectData.hasTypeRep (lab : Class.Label) : TypeRep (ObjectData lab) where
   rep := Rep.composite "AVM.ObjectData" [Rep.atomic lab.name]
 
-structure SomeObjectData where
+structure ObjectValue where
   {label : Class.Label}
+  uid : ObjectId
   data : ObjectData label
 
-instance SomeObjectData.hasTypeRep : TypeRep SomeObjectData where
-  rep := Rep.atomic "AVM.SomeObjectData"
-
-instance SomeObjectData.hasBEq : BEq SomeObjectData where
-  beq a b := a.label === b.label && a.data === b.data
-
-def ObjectData.toSomeObjectData {lab : Class.Label} (data : ObjectData lab) : SomeObjectData := {data}
+def ObjectData.toObjectValue {lab : Class.Label} (uid : ObjectId) (data : ObjectData lab) : ObjectValue :=
+  ⟨uid, data⟩
 
 /-- Represents a concrete object, translated into a resource. For class
     represetation (object description), see `AVM.Class`. -/
@@ -52,9 +48,8 @@ instance SomeObject.hasBEq : BEq SomeObject where
 
 def Object.toSomeObject {lab : Class.Label} (object : Object lab) : SomeObject := ⟨object⟩
 
-def Object.toSomeObjectData {lab : Class.Label} (object : Object lab) : SomeObjectData := ⟨object.data⟩
-
-def SomeObject.toSomeObjectData (object : SomeObject) : SomeObjectData := ⟨object.object.data⟩
+def Object.toObjectValue {lab : Class.Label} (obj : Object lab) : ObjectValue :=
+  obj.data.toObjectValue obj.uid
 
 structure Object.Resource.Label where
   /-- The label of the class -/

Anoma/Nonce.lean

@@ -5,7 +5,7 @@ import Anoma.NullifierKey
 namespace Anoma
 
 structure Nonce where
- nat : Nat
+ value : Nat
  deriving BEq
 
 instance Nonce.hasTypeRep : TypeRep Nonce where
@@ -15,4 +15,4 @@ instance Nonce.instInhabited : Inhabited Nonce where
   default := ⟨0⟩
 
 def Nonce.todo : Nonce where
-  nat := 0
+  value := 0