From 5d47cc38eb58f8c265db2113f887c8a9af852d8a Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 17 Oct 2025 11:43:54 +0200
Subject: [PATCH 1/7] update summary

---
 SUMMARY.md | 17 +++++++++++++----
 1 file changed, 13 insertions(+), 4 deletions(-)

diff --git a/SUMMARY.md b/SUMMARY.md
index 4751497f..6cf4ad32 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -19,6 +19,7 @@ A high-level summary description of GOOSE v0.3.1. The description intentionally
 		- [MultiMethod](#multimethod)
 		- [Class](#class)
 		- [Ecosystem](#ecosystem)
+		- [Authorization](#authorization)
 	- [AVM -\> RM translation](#avm---rm-translation)
 		- [Object](#object-1)
 			- [Resource data check](#resource-data-check)
@@ -209,6 +210,9 @@ Action sending the call messages:
     - destroyed selves,
     - constructed objects.
   - `recipients : List ObjectId`. The recipients of the message.
+  - `signatures : List Signature`. Authorization signatures for the message. Each signature consists of:
+    - public identifier of the signer,
+    - signature data: the message `id` and `args` cryptographically signed with signer's private key.
 
 ### Constructor
 - `Class.Constructor` in `AVM/Class/Member.lean`
@@ -218,7 +222,7 @@ Action sending the call messages:
 	- `id : label.ConstructorId` determines the unique id of the constructor.
 	- `Args := label.ConstructorArgs id` is the type of constructor arguments.
 	- `body : Args -> Program ObjectData`. Constructor body, returning the object data for the object created by the constructor call.
-	- `invariant : Args -> Bool`. Extra constructor logic. The constructor message logic is a conjunction of auto-generated constructor logic and the extra constructor logic.
+	- `invariant : Message -> Args -> Bool`. Extra constructor logic. The constructor message logic is a conjunction of auto-generated constructor logic and the extra constructor logic.
 
 ### Destructor
 - `Class.Destructor` in `AVM/Class/Member.lean`
@@ -228,7 +232,7 @@ Action sending the call messages:
 	- `id : label.DestructorId` determines the unique id of the destructor.
 	- `Args := label.DestructorArgs id` is the type of destructor arguments excluding `self`.
 	- `body : (self : Object) -> Args -> Program Unit`. Destructor body program.
-	- `invariant : (self : Object) -> Args -> Bool`. Extra destructor logic. The destructor message logic is a conjunction of auto-generated destructor logic and the extra destructor logic.
+	- `invariant : Message -> (self : Object) -> Args -> Bool`. Extra destructor logic. The destructor message logic is a conjunction of auto-generated destructor logic and the extra destructor logic.
 
 ### Method
 - `Class.Method` in `AVM/Class/Member.lean`
@@ -238,7 +242,7 @@ Action sending the call messages:
 	- `id : label.MethodId` determines the unique id of the method.
 	- `Args := label.MethodArgs id` is the type of method arguments excluding `self`.
 	- `body : (self : Object) -> Args -> Program Object`. Method body program. The return value is the updated `self`.
-	- `invariant : (self : Object) -> Args -> Bool`. Extra method logic. The method message logic is a conjunction of auto-generated method logic and the extra method logic.
+	- `invariant : Message -> (self : Object) -> Args -> Bool`. Extra method logic. The method message logic is a conjunction of auto-generated method logic and the extra method logic.
 
 ### MultiMethod
 - `MultiMethod` in `AVM/Ecosystem/Member.lean`
@@ -253,7 +257,7 @@ Action sending the call messages:
 		- `destroyed : List Object`. List of destroyed selves. Destroyed object resources are balanced with automatically generated created ephemeral resources. The `destroyed` list must be a sublist of `selves`.
 		- `assembled : List Object`. List of assembled objects into which disassembled objects are transformed as a result of the multi-method call. It is the responsibility of the user to ensure that assembled object resources balance with the disassembled selves.
 		- `constructed : List Object`. List of constructed objects. Constructed object resources are balanced with automatically generated consumed ephemeral resources.
-	- `invariant : (selves : List Object) -> Args -> Bool`. Extra multi-method logic. The multi-method message logic is a conjunction of the auto-generated multi-method logic and the extra multi-method logic.
+	- `invariant : Message -> (selves : List Object) -> Args -> Bool`. Extra multi-method logic. The multi-method message logic is a conjunction of the auto-generated multi-method logic and the extra multi-method logic.
 - `selves : List Object` in `body` and `invariant` above is a list of `self` arguments - objects whose classes are described by `label.MultiMethodSelves id`.
 - `selves = disassembled ++ destroyed`.
 
@@ -275,6 +279,11 @@ Action sending the call messages:
 	- `classes : Set Class`. Classes in the ecosystem. A class is in exactly one ecosystem.
 	- `multiMethods : Set MultiMethod`. Multi-methods in the ecosystem. A multi-method is in exactly one ecosystem.
 
+### Authorization
+The GOOSE framework provides a function `checkSignature : Message -> PublicKey -> Bool` which checks that a given message was signed with the private key corresponding to a given public key. In other words, `checkSignature(msg, pubKey)` checks that decrypting `msg.signature` with `pubKey` yields (a digest of) `msg`.
+
+The `checkSignature` function can be used in invariants to perform authorization of the received messages.
+
 ## AVM -> RM translation
 
 ### Object

From 82e2fe344355783c610a9c22671189181d180684 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 17 Oct 2025 12:00:41 +0200
Subject: [PATCH 2/7] update summary - multi-methods

---
 AVM/Message/Base.lean |  4 ++--
 SUMMARY.md            | 14 ++++++++------
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean
index 4d77ec4c..e341785d 100644
--- a/AVM/Message/Base.lean
+++ b/AVM/Message/Base.lean
@@ -17,10 +17,10 @@ structure Message (lab : Ecosystem.Label) : Type 1 where
   logicRef : Anoma.LogicRef
   /-- The arguments of the message. -/
   args : id.Args.type
-  /-- The signature of the arguments -/
-  signatures : id.Signatures args
   /-- The recipients of the message. -/
   recipients : List ObjectId
+  /-- The signature of the arguments -/
+  signatures : id.Signatures args
 
 def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat :=
   let {id := id, signatures := signatures, ..} := msg
diff --git a/SUMMARY.md b/SUMMARY.md
index 6cf4ad32..295d7b2c 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -205,10 +205,6 @@ Action sending the call messages:
   - `vals : Vals`. Message parameter values. The message parameters are object resources and generated random values that are used in the body of the call associated with the message. These need to be provided in the message, because the associated Resource Logic cannot fetch object resources from the Anoma system or generate new object identifiers.
   - `id : MessageId`. The message ID.
   - `args : id.Args`. The arguments of the message, where `id.Args` is the type of arguments based on the message id. The message arguments are the non-self arguments of the corresponding member or multi-method call.
-  - `data : Option MultiMethodData`. Extra data for multi-methods which contains the numbers of:
-    - disassembled selves,
-    - destroyed selves,
-    - constructed objects.
   - `recipients : List ObjectId`. The recipients of the message.
   - `signatures : List Signature`. Authorization signatures for the message. Each signature consists of:
     - public identifier of the signer,
@@ -603,12 +599,18 @@ Multi-method message logic has access to RL arguments which contain the followin
 
 - `consumed : List Resource`. List of resources consumed in the transaction.
 - `created : List Resource`. List of resources created in the transaction.
-- `msgRes : Resource`. The resource of the method message `msg`, which contains the method call arguments `args` and the `data` field with the numbers of:
+- `msgRes : Resource`. The resource of the method message `msg`, which contains the method call arguments `args` and parameter values `vals`.
+
+For a given multi-method, the number `n` of `selves` is specified in the
+multi-method definition. We re-create the `selves` objects from the first `n`
+object resources in `consumed`.
+
+With `selves`, `args` and `vals`, we compute the result of of the multi-method. In this way, we obtain the numbers of:
   - disassembled selves,
   - destroyed selves,
   - constructed objects.
 
-For a given multi-method, we use the numbers stored in `msg.data` to partition the object resources in `consumed` into:
+We use the above numbers to partition the object resources in `consumed` into:
 
 - `disassembledSelves` list of persistent object resources corresponding to disassembled selves,
 - `destroyedSelves` list of persistent object resources corresponding to destroyed selves,

From 75701b1e261c70f3a75ce79801ebf4b6598775d6 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Fri, 17 Oct 2025 18:48:14 +0200
Subject: [PATCH 3/7] fix: authorization (wip)

---
 AVM/Authorization.lean              | 17 +++---
 AVM/Class/Label.lean                | 36 +++----------
 AVM/Class/Member.lean               | 15 ++++--
 AVM/Class/Translation/Logics.lean   |  7 ++-
 AVM/Class/Translation/Messages.lean | 83 +++++++++++++++--------------
 AVM/Class/Translation/Tasks.lean    |  8 +--
 AVM/Ecosystem/Label/Base.lean       | 10 ----
 AVM/Ecosystem/Member.lean           |  5 +-
 AVM/Message.lean                    |  4 +-
 AVM/Message/Base.lean               | 47 +++++-----------
 AVM/Message/Data.lean               | 34 ++++++++++++
 AVM/Program.lean                    |  8 +--
 Applib/Surface/Member.lean          | 22 ++++----
 Applib/Surface/MultiMethod.lean     |  6 +--
 Applib/Surface/Program.lean         | 16 +++---
 Apps/KudosBank.lean                 |  7 +--
 16 files changed, 164 insertions(+), 161 deletions(-)
 create mode 100644 AVM/Message/Data.lean

diff --git a/AVM/Authorization.lean b/AVM/Authorization.lean
index 94d95e5f..bb667490 100644
--- a/AVM/Authorization.lean
+++ b/AVM/Authorization.lean
@@ -1,5 +1,8 @@
 import Mathlib.Data.Fintype.Basic
 import Prelude
+import AVM.Message.Data
+
+namespace AVM
 
 structure PublicKey where
   key : Nat
@@ -21,19 +24,17 @@ def PrivateKey.universal : PrivateKey where
 -- mock function
 private def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key
 
-structure Signature {A : Type u} (msg : A) : Type u where
-  msg : A
+structure Signature where
   private signature : PrivateKey
 
 -- Mock function that returns the `raw` bytes of the signature
-def Signature.raw {A : Type u} (msg : A) (_s : Signature msg ) : Nat := 0
+def Signature.raw (_s : Signature) : Nat := 0
 
-instance {A B} (msgA : A) (msgB : B) : HBEq (Signature msgA) (Signature msgB) where
-  hbeq a b := a.raw == b.raw
+instance : BEq Signature where
+  beq a b := a.raw == b.raw
 
-def Signature.sign {A : Type u} (msg : A) (key : PrivateKey) : Signature msg where
+def Signature.sign {lab : Ecosystem.Label} (_msg : MessageData lab) (key : PrivateKey) : Signature where
   signature := key
-  msg
 
 -- mock function
-def checkSignature {A : Type u} {msg : A} (sig : Signature msg) (pub : PublicKey) : Bool := checkKey pub sig.signature
+def checkSignature {lab : Ecosystem.Label} (_msg : MessageData lab) (sig : Signature) (pub : PublicKey) : Bool := checkKey pub sig.signature
diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean
index a523bea8..d8819219 100644
--- a/AVM/Class/Label.lean
+++ b/AVM/Class/Label.lean
@@ -2,7 +2,6 @@ import Anoma.Resource
 import Prelude
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.FinEnum
-import AVM.Authorization
 
 abbrev AVM.ObjectId := Anoma.ObjectId
 
@@ -163,33 +162,14 @@ def Label.MemberId.Args {lab : Class.Label} (memberId : MemberId lab) : SomeType
   | methodId c => lab.MethodArgs c
   | upgradeId => ⟨PUnit⟩
 
-abbrev Label.MemberId.Signatures
-  {lab : Class.Label}
-  (f : MemberId lab)
-  (args : f.Args.type)
-  : Type :=
-  f.SignatureId → Signature (f, args)
-
-abbrev Label.MethodId.Signatures
-  {lab : Class.Label}
-  (f : lab.MethodId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.methodId f |>.Signatures args
-
-abbrev Label.ConstructorId.Signatures
-  {lab : Class.Label}
-  (f : lab.ConstructorId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.constructorId f |>.Signatures args
-
-abbrev Label.DestructorId.Signatures
-  {lab : Class.Label}
-  (f : lab.DestructorId)
-  (args : f.Args.type)
-  : Type :=
-  MemberId.destructorId f |>.Signatures args
+def Label.ConstructorId.SignatureId {lab : Class.Label} (constrId : lab.ConstructorId) : Type :=
+  lab.ConstructorSignatureId constrId
+
+def Label.DestructorId.SignatureId {lab : Class.Label} (destrId : lab.DestructorId) : Type :=
+  lab.DestructorSignatureId destrId
+
+def Label.MethodId.SignatureId {lab : Class.Label} (methodId : lab.MethodId) : Type :=
+  lab.MethodSignatureId methodId
 
 instance Label.hasTypeRep : TypeRep Label where
   rep := Rep.atomic "AVM.Class.Label"
diff --git a/AVM/Class/Member.lean b/AVM/Class/Member.lean
index 5e36740d..556752d7 100644
--- a/AVM/Class/Member.lean
+++ b/AVM/Class/Member.lean
@@ -2,25 +2,34 @@ import AVM.Program
 
 namespace AVM.Class
 
+def Label.ConstructorId.Signatures {lab : Class.Label} (constrId : lab.ConstructorId) : Type :=
+  constrId.SignatureId -> Signature
+
+def Label.DestructorId.Signatures {lab : Class.Label} (destrId : lab.DestructorId) : Type :=
+  destrId.SignatureId -> Signature
+
+def Label.MethodId.Signatures {lab : Class.Label} (methodId : lab.MethodId) : Type :=
+  methodId.SignatureId -> Signature
+
 structure Constructor {lab : Ecosystem.Label} (cid : lab.ClassId) (constrId : cid.label.ConstructorId) : Type 1 where
   /-- Constructor call body. -/
   body : constrId.Args.type → Program.{0} lab.toScope (ObjectData cid)
   /-- Extra constructor logic. The constructor invariant is combined with
       auto-generated constructor body constraints to create the constructor logic. -/
-  invariant : (args : constrId.Args.type) → constrId.Signatures args →  Bool
+  invariant : (msg : Message lab) → (args : constrId.Args.type) → Bool
 
 structure Destructor {lab : Ecosystem.Label} (cid : lab.ClassId) (destructorId : cid.label.DestructorId) : Type 1 where
   /-- Destructor call body. -/
   body : (self : Object cid) → destructorId.Args.type → Program.{0} lab.toScope PUnit
   /-- Extra destructor logic. -/
-  invariant : (self : Object cid) → (args : destructorId.Args.type) → destructorId.Signatures args → Bool
+  invariant : (msg : Message lab) → (self : Object cid) → (args : destructorId.Args.type) → Bool
 
 structure Method {lab : Ecosystem.Label} (cid : lab.ClassId) (methodId : cid.label.MethodId) : Type 1 where
   /-- Method call body. -/
   body : (self : Object cid) → methodId.Args.type → Program lab.toScope (Object cid)
   /-- Extra method logic. The method invariant is combined with auto-generated
       method body constraints to create the method logic. -/
-  invariant : (self : Object cid) → (args : methodId.Args.type) → methodId.Signatures args → Bool
+  invariant : (msg : Message lab) → (self : Object cid) → (args : methodId.Args.type) → Bool
 
 /-- A class member is a constructor, a destructor or a method. -/
 inductive Member {lab : Ecosystem.Label} (cid : lab.ClassId) where
diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean
index b7b4c9d4..11e56f7a 100644
--- a/AVM/Class/Translation/Logics.lean
+++ b/AVM/Class/Translation/Logics.lean
@@ -78,7 +78,7 @@ def checkMessageResourceValues {lab : Ecosystem.Label} (vals : List (Program.Mes
   List.all₂
     (fun val res =>
       let try msg : Message lab := Message.fromResource res
-      msg.id == val.id && msg.args === val.args && msg.logicRef == val.logicRef)
+      msg.data.id == val.id && msg.data.args === val.args && msg.data.logicRef == val.logicRef)
     vals
     resMsgs
 
@@ -99,10 +99,9 @@ def MultiMethod.Message.logicFun
   let createdResObjs := Logic.selectObjectResources args.created
   let argsConsumedSelves := consumedResObjs.take multiId.numObjectArgs
   let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves
+  check method.invariant msg argsConsumedObjects fargs
   let prog := method.body argsConsumedObjects fargs
-  let signatures := cast (by grind only) msg.signatures
-  check method.invariant argsConsumedObjects fargs signatures
-  let try vals : prog.params.Product := tryCast msg.vals
+  let try vals : prog.params.Product := tryCast msg.data.vals
   let res : MultiMethodResult multiId := prog.value vals
   let valsObjs := prog.objects vals
   let fetchedObjValues := valsObjs.map (·.toObjectValue)
diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean
index 970289ee..f97abc05 100644
--- a/AVM/Class/Translation/Messages.lean
+++ b/AVM/Class/Translation/Messages.lean
@@ -1,4 +1,4 @@
-import AVM.Ecosystem.Label
+import AVM.Ecosystem
 import AVM.Class
 import AVM.Message
 import AVM.Class.Translation.Logics
@@ -14,14 +14,15 @@ def Constructor.message
   (vals : Vals.type)
   (newId : ObjectId)
   (args : constrId.Args.type)
-  (signatures : Class.Label.MemberId.constructorId constrId |>.Signatures args)
+  (signatures : constrId.Signatures)
   : Message lab :=
-  { id := .classMember (.constructorId constrId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [newId] }
+  let data : MessageData lab :=
+    { id := .classMember (.constructorId constrId)
+      logicRef := Logic.trivialLogicRef
+      vals
+      args
+      recipients := [newId] }
+  { data, signatures }
 
 def Destructor.message
   {lab : Ecosystem.Label}
@@ -32,14 +33,15 @@ def Destructor.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : destrId.Args.type)
-  (signatures : Class.Label.MemberId.destructorId destrId |>.Signatures args)
+  (signatures : destrId.Signatures)
   : Message lab :=
-  { id := .classMember (.destructorId destrId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (.destructorId destrId)
+      logicRef := Logic.trivialLogicRef
+      vals
+      args
+      recipients := [selfId] }
+  { data, signatures }
 
 def Method.message
   {lab : Ecosystem.Label}
@@ -50,27 +52,29 @@ def Method.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : methodId.Args.type)
-  (signatures : Class.Label.MemberId.methodId methodId |>.Signatures args)
+  (signatures : methodId.Signatures)
   : Message lab :=
-  { id := .classMember (.methodId methodId)
-    logicRef := Logic.trivialLogicRef
-    vals
-    args
-    signatures
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (.methodId methodId)
+      logicRef := Logic.trivialLogicRef
+      vals
+      args
+      recipients := [selfId] }
+  { data, signatures }
 
 def Upgrade.message
   {lab : Ecosystem.Label}
   (classId : lab.ClassId)
   (selfId : ObjectId)
   : Message lab :=
-  { id := .classMember (classId := classId) .upgradeId
-    logicRef := Logic.trivialLogicRef
-    Vals := ⟨PUnit⟩
-    vals := PUnit.unit
-    args := .unit
-    signatures f := nomatch f
-    recipients := [selfId] }
+  let data : MessageData lab :=
+    { id := .classMember (classId := classId) .upgradeId
+      logicRef := Logic.trivialLogicRef
+      Vals := ⟨PUnit⟩
+      vals := PUnit.unit
+      args := .unit
+      recipients := [selfId] }
+  { data, signatures := fun f => nomatch f}
 
 end AVM.Class
 
@@ -82,17 +86,18 @@ def MultiMethod.message
   (method : MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : multiId.Signatures)
   (vals : (method.body selves args).params.Product)
   (data : MultiMethodData)
   (rands : MultiMethodRandoms data)
   : Message lab :=
-  { id := .multiMethodId multiId
-    logicRef := Logic.trivialLogicRef
-    Vals := ⟨(method.body selves args).params.Product⟩
-    vals
-    args
-    signatures
-    recipients :=
-      (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList)
-        ++ rands.constructedNonces.toList.map (·.value) }
+  let data : MessageData lab :=
+    { id := .multiMethodId multiId
+      logicRef := Logic.trivialLogicRef
+      Vals := ⟨(method.body selves args).params.Product⟩
+      vals
+      args
+      recipients :=
+        (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList)
+          ++ rands.constructedNonces.toList.map (·.value) }
+  { data, signatures }
diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean
index 77aac00d..de31b78d 100644
--- a/AVM/Class/Translation/Tasks.lean
+++ b/AVM/Class/Translation/Tasks.lean
@@ -160,7 +160,7 @@ private partial def Class.Constructor.task'
   (newId : ObjectId)
   (r : Nat)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures args)
+  (signatures : constrId.Signatures)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (ObjectData classId)) := constr.body args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (newObjectData : ULift (ObjectData classId)) : ActionData :=
@@ -193,7 +193,7 @@ private partial def Class.Destructor.task'
   (r : Nat)
   (self : Object classId)
   (args : destructorId.Args.type)
-  (signatures : destructorId.Signatures args)
+  (signatures : destructorId.Signatures)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift Unit) := destructor.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (_ : ULift Unit) : ActionData :=
@@ -223,7 +223,7 @@ private partial def Class.Method.task'
   (r : Nat)
   (self : Object classId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures args)
+  (signatures : methodId.Signatures)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (Object classId)) := method.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (lobj : ULift (Object classId)) : ActionData :=
@@ -274,7 +274,7 @@ partial def Ecosystem.MultiMethod.task'
   (method : Ecosystem.MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : multiId.Signatures)
   : Task' :=
   let body := method.body selves args
 
diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean
index fe61eec4..16cf77f1 100644
--- a/AVM/Ecosystem/Label/Base.lean
+++ b/AVM/Ecosystem/Label/Base.lean
@@ -1,5 +1,4 @@
 import AVM.Class.Label
-import AVM.Authorization
 
 namespace AVM.Ecosystem
 
@@ -104,9 +103,6 @@ abbrev Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType :=
 
 abbrev SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId
 
-abbrev Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) (args : multiId.Args.type) : Type :=
-  multiId.SignatureId → Signature (multiId, args)
-
 def ObjectArgNames {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type :=
   lab.MultiMethodObjectArgNames multiId
 
@@ -199,12 +195,6 @@ abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType.{0} :=
   | multiMethodId f => lab.MultiMethodArgs f
   | classMember m => Class.Label.MemberId.Args m
 
-abbrev Signatures {lab : Ecosystem.Label} (mem : MemberId lab) (args : mem.Args.type)
-  : Type :=
-  match mem with
-  | .classMember m => m.Signatures args
-  | .multiMethodId m => m.Signatures args
-
 /-- The number of object arguments (selves) for this member ID. -/
 def numObjectArgs {lab : Ecosystem.Label} (memberId : MemberId lab) : Nat :=
   match memberId with
diff --git a/AVM/Ecosystem/Member.lean b/AVM/Ecosystem/Member.lean
index 9feccd42..14bf1d0d 100644
--- a/AVM/Ecosystem/Member.lean
+++ b/AVM/Ecosystem/Member.lean
@@ -92,8 +92,11 @@ def data
 
 end MultiMethodResult
 
+def Ecosystem.Label.MultiMethodId.Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type :=
+  multiId.SignatureId -> Signature
+
 structure Ecosystem.MultiMethod {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type 1 where
   /-- Computes the result of a multiMethod call. See `MultiMethodResult`. -/
   body (selves : multiId.Selves) (args : multiId.Args.type) : Program.{1} lab.toScope (MultiMethodResult multiId)
   /-- Extra multiMethod logic. -/
-  invariant (selves : multiId.Selves) (args : multiId.Args.type) (signatures : multiId.Signatures args) : Bool
+  invariant (msg : Message lab) (selves : multiId.Selves) (args : multiId.Args.type) : Bool
diff --git a/AVM/Message.lean b/AVM/Message.lean
index 0d6f22fc..cbb4f680 100644
--- a/AVM/Message.lean
+++ b/AVM/Message.lean
@@ -9,7 +9,7 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
   { Val := ⟨PUnit⟩,
     Label := ⟨SomeMessage⟩,
     label := msg,
-    logicRef := msg.message.logicRef,
+    logicRef := msg.message.data.logicRef,
     value := PUnit.unit,
     quantity := 1,
     nullifierKeyCommitment := default,
@@ -18,7 +18,7 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
 
 def SomeMessage.fromResource (res : Anoma.Resource) : Option SomeMessage :=
   let try msg : SomeMessage := tryCast res.label
-  check (msg.message.logicRef == res.logicRef)
+  check (msg.message.data.logicRef == res.logicRef)
   some msg
 
 def Message.toResource {lab : Ecosystem.Label} (msg : Message lab) (nonce : Anoma.Nonce) : Anoma.Resource :=
diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean
index e341785d..17579faf 100644
--- a/AVM/Message/Base.lean
+++ b/AVM/Message/Base.lean
@@ -1,29 +1,16 @@
-import AVM.Ecosystem.Data
+import AVM.Message.Data
+import AVM.Authorization
 
 namespace AVM
 
 /-- A message is a communication sent from one object to another in the AVM. -/
 structure Message (lab : Ecosystem.Label) : Type 1 where
-  /-- The message ID. -/
-  id : lab.MemberId
-  {Vals : SomeType.{0}}
-  /-- Message parameter values. The message parameters are object resources and
-    generated random values that are used in the body of the call associated with
-    the message. These need to be provided in the message, because the
-    associated Resource Logic cannot fetch object resources from the Anoma
-    system or generate new object identifiers. -/
-  vals : Vals.type
-  /-- Resource logic reference for the message logic. -/
-  logicRef : Anoma.LogicRef
-  /-- The arguments of the message. -/
-  args : id.Args.type
-  /-- The recipients of the message. -/
-  recipients : List ObjectId
+  data : MessageData lab
   /-- The signature of the arguments -/
-  signatures : id.Signatures args
+  signatures : data.id.SignatureId → Signature
 
 def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat :=
-  let {id := id, signatures := signatures, ..} := msg
+  let {data := {id := id, ..}, signatures := signatures, ..} := msg
   match id with
   | .multiMethodId m => lab.MultiMethodSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
   | .classMember (classId := clab) c => match c with
@@ -41,14 +28,7 @@ instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) wher
 
 instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where
   beq a b :=
-    let {id := aid, args := aargs, signatures := asigs, ..} := a
-    let {id := bid, args := bargs, signatures := bsigs, ..} := b
-    check h : aid == bid
-    let h' := eq_of_beq h
-    check a.vals === b.vals
-    check s : aargs == cast (by simp! [h']) bargs
-    check a.recipients == b.recipients
-    check a.rawSignatures == b.rawSignatures
+    a.data == b.data && a.rawSignatures == b.rawSignatures
 
 structure SomeMessage : Type 1 where
   {label : Ecosystem.Label}
@@ -68,13 +48,14 @@ instance SomeMessage.hasBEq : BEq SomeMessage where
 instance : Inhabited SomeMessage where
   default := { label := Ecosystem.Label.dummy
                message :=
-                { id := .classMember (classId := .unit) (.constructorId PUnit.unit)
-                  Vals := ⟨PUnit⟩
-                  vals := PUnit.unit
-                  logicRef := default
-                  signatures f := nomatch f
-                  args := PUnit.unit
-                  recipients := [] }}
+                { data :=
+                    { id := .classMember (classId := .unit) (.constructorId PUnit.unit)
+                      Vals := ⟨PUnit⟩
+                      vals := PUnit.unit
+                      logicRef := default
+                      args := PUnit.unit
+                      recipients := [] },
+                  signatures f := nomatch f }}
 
 def Message.toSomeMessage {lab : Ecosystem.Label} (msg : Message lab) : SomeMessage :=
   { label := lab, message := msg }
diff --git a/AVM/Message/Data.lean b/AVM/Message/Data.lean
new file mode 100644
index 00000000..4d5ec91b
--- /dev/null
+++ b/AVM/Message/Data.lean
@@ -0,0 +1,34 @@
+import AVM.Ecosystem.Data
+
+namespace AVM
+
+/-- A message is a communication sent from one object to another in the AVM. -/
+structure MessageData (lab : Ecosystem.Label) : Type 1 where
+  /-- The message ID. -/
+  id : lab.MemberId
+  {Vals : SomeType.{0}}
+  /-- Message parameter values. The message parameters are object resources and
+    generated random values that are used in the body of the call associated with
+    the message. These need to be provided in the message, because the
+    associated Resource Logic cannot fetch object resources from the Anoma
+    system or generate new object identifiers. -/
+  vals : Vals.type
+  /-- Resource logic reference for the message logic. -/
+  logicRef : Anoma.LogicRef
+  /-- The arguments of the message. -/
+  args : id.Args.type
+  /-- The recipients of the message. -/
+  recipients : List ObjectId
+
+instance MessageData.hasTypeRep (lab : Ecosystem.Label) : TypeRep (MessageData lab) where
+  rep := Rep.composite "AVM.MessageData" [Rep.atomic lab.name]
+
+instance MessageData.hasBEq {lab : Ecosystem.Label} : BEq (MessageData lab) where
+  beq a b :=
+    let {id := aid, args := aargs, ..} := a
+    let {id := bid, args := bargs, ..} := b
+    check h : aid == bid
+    let h' := eq_of_beq h
+    check a.vals === b.vals
+    check s : aargs == cast (by simp! [h']) bargs
+    check a.recipients == b.recipients
diff --git a/AVM/Program.lean b/AVM/Program.lean
index 670e3f86..de8b2cc1 100644
--- a/AVM/Program.lean
+++ b/AVM/Program.lean
@@ -14,7 +14,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.Signatures args)
+    (signatures : constrId.SignatureId -> Signature)
     (next : ObjectId → Program scope ReturnType)
     : Program scope ReturnType
   | /-- Destructor call. -/
@@ -24,7 +24,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.Signatures args)
+    (signatures : destrId.SignatureId -> Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Method call. -/
@@ -34,7 +34,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.Signatures args)
+    (signatures : methodId.SignatureId -> Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- MultiMethod call. -/
@@ -43,7 +43,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (mid : eid.label.MultiMethodId)
     (selvesIds : mid.SelvesIds)
     (args : mid.Args.type)
-    (signatures : mid.Signatures args)
+    (signatures : mid.SignatureId -> Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Object upgrade -/
diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean
index 2fe7248d..3a9bc86f 100644
--- a/Applib/Surface/Member.lean
+++ b/Applib/Surface/Member.lean
@@ -10,17 +10,17 @@ macro "noDestructors" : term => `(fun x => Empty.elim x)
 macro "noMethods" : term => `(fun x => Empty.elim x)
 
 def unsigned
-  {Args SignatureId : Type}
-  {args : Args}
-  : SignatureId → Signature args := fun _ => Signature.sign args PrivateKey.universal
+  {lab : Ecosystem.Label}
+  {SignatureId : Type}
+  : MessageData lab → SignatureId → Signature := fun msg _ => Signature.sign msg PrivateKey.universal
 
 def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId}
  (body : (self : cl) → methodId.Args.type → Program i.label.toScope cl)
- (invariant : (self : cl) → (args : methodId.Args.type) → methodId.Signatures args → Bool := fun _ _ _ => true)
+ (invariant : (msg : Message i.label) → (self : cl) → (args : methodId.Args.type) → Bool := fun _ _ _ => true)
  : Class.Method i.classId methodId where
-    invariant (self : Object i.classId) (args : methodId.Args.type) :=
+    invariant (msg : Message i.label) (self : Object i.classId) (args : methodId.Args.type) :=
       let self' : cl := i.fromObject self.data
-      invariant self' args
+      invariant msg self' args
     body (self : Object i.classId) (args : methodId.Args.type) :=
       let self' := i.fromObject self.data
       let prog := body self' args
@@ -29,17 +29,17 @@ def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId
 
 def defConstructor {cl : Type} [i : IsObject cl] {constrId : i.classId.label.ConstructorId}
  (body : constrId.Args.type → Program i.label.toScope cl)
- (invariant : (args : constrId.Args.type) → (signatures : constrId.Signatures args) → Bool := fun _ _ => true)
+ (invariant : (msg : Message i.label) → (args : constrId.Args.type) → Bool := fun _ _ => true)
  : Class.Constructor i.classId constrId where
-    invariant (args : constrId.Args.type) := invariant args
+    invariant (msg : Message i.label) (args : constrId.Args.type) := invariant msg args
     body (args : constrId.Args.type) := body args |>.map i.toObject |>.toAVM
 
 def defDestructor {cl : Type} [i : IsObject cl] {destructorId : i.classId.label.DestructorId}
  (body : (self : cl) → destructorId.Args.type → Program i.label.toScope PUnit := fun _ _ => Program.return ())
- (invariant : (self : cl) -> (args : destructorId.Args.type) → destructorId.Signatures args → Bool := fun _ _ _ => true)
+ (invariant : (msg : Message i.label) → (self : cl) -> (args : destructorId.Args.type) → Bool := fun _ _ _ => true)
  : Class.Destructor i.classId destructorId where
-    invariant (self : Object i.classId) (args : destructorId.Args.type) (signatures : destructorId.Signatures args) :=
+    invariant (msg : Message i.label) (self : Object i.classId) (args : destructorId.Args.type) :=
       let self' := i.fromObject self.data
-      invariant self' args signatures
+      invariant msg self' args
     body (self : Object i.classId) (args : destructorId.Args.type) :=
       body (i.fromObject self.data) args |>.toAVM
diff --git a/Applib/Surface/MultiMethod.lean b/Applib/Surface/MultiMethod.lean
index a3f083fa..a65479a6 100644
--- a/Applib/Surface/MultiMethod.lean
+++ b/Applib/Surface/MultiMethod.lean
@@ -59,12 +59,12 @@ def defMultiMethod
   (multiId : lab.MultiMethodId)
   (argsInfo : (a : multiId.ObjectArgNames) → ObjectArgInfo lab multiId a)
   (body : ObjectArgs lab multiId argsInfo → multiId.Args.type → Program lab.toScope (MultiMethodResult multiId))
-  (invariant : ObjectArgs lab multiId argsInfo → (args : multiId.Args.type) → (signatures : multiId.Signatures args) → Bool := fun _ _ _ => true)
+  (invariant : AVM.Message lab → ObjectArgs lab multiId argsInfo → (args : multiId.Args.type) → Bool := fun _ _ _ => true)
   : AVM.Ecosystem.MultiMethod multiId where
   body (selves : multiId.Selves) (args : multiId.Args.type) : AVM.Program lab.toScope (AVM.MultiMethodResult multiId) :=
     (body (getArg selves) args).map (MultiMethodResult.toAVM) |>.toAVM
-  invariant (selves : multiId.Selves) (args : multiId.Args.type) (signatures : multiId.Signatures args) : Bool :=
-    invariant (getArg selves) args signatures
+  invariant (msg : AVM.Message lab) (selves : multiId.Selves) (args : multiId.Args.type) : Bool :=
+    invariant msg (getArg selves) args
   where
     getArg (selves : multiId.Selves) (argName : multiId.ObjectArgNames) : (argsInfo argName).type :=
       (argsInfo argName).isObjectOf.fromObject (selves argName).data
diff --git a/Applib/Surface/Program.lean b/Applib/Surface/Program.lean
index bb392993..a6d0818f 100644
--- a/Applib/Surface/Program.lean
+++ b/Applib/Surface/Program.lean
@@ -13,7 +13,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.Signatures args)
+    (signatures : constrId.Signatures)
     (next : ObjectId → Program lab α)
     : Program lab α
   | destroy
@@ -23,7 +23,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.Signatures args)
+    (signatures : destrId.Signatures)
     (next : Program lab α)
     : Program lab α
   | call
@@ -33,7 +33,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.Signatures args)
+    (signatures : methodId.Signatures)
     (next : Program lab α)
     : Program lab α
   | multiCall
@@ -42,7 +42,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (multiId : eid.label.MultiMethodId)
     (selves : multiId.SelvesIds)
     (args : multiId.Args.type)
-    (signatures : multiId.Signatures args)
+    (signatures : multiId.Signatures)
     (next : Program lab α)
     : Program lab α
   | upgrade
@@ -125,7 +125,7 @@ def Program.create'
   (inScope : i.label ∈ lab)
   (constrId : i.classId.label.ConstructorId)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures args)
+  (signatures : constrId.Signatures)
   (next : Reference C → Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -146,7 +146,7 @@ def Program.destroy'
   (inScope : i.label ∈ lab)
   (destrId : i.classId.label.DestructorId)
   (args : destrId.Args.type)
-  (signatures : destrId.Signatures args)
+  (signatures : destrId.Signatures)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -168,7 +168,7 @@ def Program.call'
   (inScope : i.label ∈ lab)
   (methodId : i.classId.label.MethodId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures args)
+  (signatures : methodId.Signatures)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -203,7 +203,7 @@ def Program.multiCall'
   (multiId : eid.label.MultiMethodId)
   (selves : multiId.SelvesReferences)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures args)
+  (signatures : multiId.Signatures)
   (next : Program lab α)
   : Program lab α :=
   let selves' : multiId.SelvesIds := fun x => selves x |>.ref.objId
diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean
index 6db9d41a..954e2fbd 100644
--- a/Apps/KudosBank.lean
+++ b/Apps/KudosBank.lean
@@ -2,6 +2,7 @@ import AVM
 import Applib
 
 open Applib
+open AVM
 
 def Std.HashMap.modifyDefault
 {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : HashMap α β) (a : α) (f : β → β) : HashMap α β := m.alter a fun
@@ -10,7 +11,7 @@ def Std.HashMap.modifyDefault
 
 structure Denomination where
   originator : PublicKey
-  deriving BEq, Inhabited, Hashable, DecidableEq
+  deriving BEq, Inhabited, Hashable
 
 structure Account where
   assets : Std.HashMap Denomination Nat
@@ -471,9 +472,9 @@ def kudosTransfer : @Class.Method label Classes.Bank Methods.Transfer := defMeth
         |> Balances.addTokens args.newOwner args.denom args.quantity
         |> Balances.subTokens args.oldOwner args.denom args.quantity)
   ⟫)
-  (invariant := fun (self : KudosBank) (args : TransferArgs) signatures =>
+  (invariant := fun (msg : Message label) (self : KudosBank) (args : TransferArgs) =>
     0 < args.quantity
-    && checkSignature (signatures .owner) args.oldOwner
+    && checkSignature msg.data (msg.signatures Methods.Transfer.SignatureId.owner) args.oldOwner
     && args.quantity <= self.getBalance args.oldOwner args.denom)
 
 def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod KudosBank

From 0e1fbd23e407cb86cecec65b68a1b51a584bfefd Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 20 Oct 2025 13:26:36 +0200
Subject: [PATCH 4/7] fix logics translation

---
 AVM/Class/Translation/Logics.lean | 35 ++++++++++++++-----------------
 1 file changed, 16 insertions(+), 19 deletions(-)

diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean
index 11e56f7a..f8f37bc3 100644
--- a/AVM/Class/Translation/Logics.lean
+++ b/AVM/Class/Translation/Logics.lean
@@ -93,8 +93,8 @@ def MultiMethod.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .multiMethodId multiId
-  let fargs : multiId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
+  check h : msg.data.id == .multiMethodId multiId
+  let fargs : multiId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let argsConsumedSelves := consumedResObjs.take multiId.numObjectArgs
@@ -159,11 +159,10 @@ private def Constructor.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.constructorId constrId)
-  let argsData : constrId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
-  let signatures : constrId.Signatures argsData := cast (by grind only) msg.signatures
+  check h : msg.data.id == .classMember (Label.MemberId.constructorId constrId)
+  let argsData : constrId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let body := constr.body argsData
-  let try vals : body.params.Product := tryCast msg.vals
+  let try vals : body.params.Product := tryCast msg.data.vals
   let newObjData := body.value vals
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
@@ -181,7 +180,7 @@ private def Constructor.Message.logicFun
     && Logic.checkResourcesEphemeral [consumedObjRes]
     && Logic.checkResourcesPersistent createdResObjs
     && Logic.checkResourcesPersistent consumedFetchedResObjs
-    && constr.invariant argsData signatures
+    && constr.invariant msg argsData
 
 /-- Creates a message logic function for a given destructor. -/
 private def Destructor.Message.logicFun
@@ -192,16 +191,15 @@ private def Destructor.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.destructorId destructorId)
-  let argsData := cast (by simp! [eq_of_beq h]) msg.args
-  let signatures : destructorId.Signatures argsData := cast (by grind only) msg.signatures
+  check h : msg.data.id == .classMember (Label.MemberId.destructorId destructorId)
+  let argsData := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let! (selfRes :: _) := consumedResObjs
   let! (createdResObj :: createdFetchedResObjs) := createdResObjs
   let try selfObj : Object classId := Object.fromResource selfRes
   let body := destructor.body selfObj argsData
-  let try vals : body.params.Product := tryCast msg.vals
+  let try vals : body.params.Product := tryCast msg.data.vals
   let messageValues := Program.messageValues body vals
   let createdResMsgs := Logic.selectMessageResources args.created
   let valsObjs := body.objects vals
@@ -213,7 +211,7 @@ private def Destructor.Message.logicFun
     && Logic.checkResourcesPersistent consumedResObjs
     && Logic.checkResourcesEphemeral [createdResObj]
     && Logic.checkResourcesPersistent createdFetchedResObjs
-    && destructor.invariant selfObj argsData signatures
+    && destructor.invariant msg selfObj argsData
 
 private def Method.Message.logicFun
   {lab : Ecosystem.Label}
@@ -223,16 +221,15 @@ private def Method.Message.logicFun
   (msg : Message lab)
   (args : Logic.Args)
   : Bool :=
-  check h : msg.id == .classMember (Label.MemberId.methodId methodId)
-  let argsData : methodId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
+  check h : msg.data.id == .classMember (Label.MemberId.methodId methodId)
+  let argsData : methodId.Args.type := cast (by simp! [eq_of_beq h]) msg.data.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let! (selfRes :: _) := consumedResObjs
   let try selfObj : Object classId := Object.fromResource selfRes
   let body := method.body selfObj argsData
-  let try vals : body.params.Product := tryCast msg.vals
-  let signatures : methodId.Signatures argsData := cast (by grind only) msg.signatures
-  check method.invariant selfObj argsData signatures
+  let try vals : body.params.Product := tryCast msg.data.vals
+  check method.invariant msg selfObj argsData
   let createdObject : Object classId := body |>.value vals
   let messageValues := Program.messageValues body vals
   let createdResMsgs := Logic.selectMessageResources args.created
@@ -313,8 +310,8 @@ private def logicFun
       -- Note: the success of the `try` below ensures that the message is "legal"
       -- for the consumed objects - it is from the same ecosystem
       let try msg : Message lab := Message.fromResource consumedMessageResource
-      self.uid ∈ msg.recipients
-      && Member.logicFun eco msg.id msg args
+      self.uid ∈ msg.data.recipients
+      && Member.logicFun eco msg.data.id msg args
 
 /-- The class logic that is the Resource Logic of each resource corresponding to
   an object of this class. -/

From 9b23293cfeb594ce2d6b0cf0dde7fade054a2213 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Mon, 20 Oct 2025 14:19:28 +0200
Subject: [PATCH 5/7] fix authorization

---
 AVM/Authorization.lean                   |  7 +++--
 AVM/Class/Label.lean                     | 24 --------------
 AVM/Class/Member.lean                    |  9 ------
 AVM/Class/Translation/Logics.lean        |  2 +-
 AVM/Class/Translation/Messages.lean      | 28 ++++++++---------
 AVM/Class/Translation/Tasks.lean         |  8 ++---
 AVM/Ecosystem/Label/Base.lean            |  9 ------
 AVM/Ecosystem/Member.lean                |  3 --
 AVM/Logic.lean                           |  1 +
 AVM/Logic/Base.lean                      | 15 +++++++++
 AVM/Message.lean                         |  7 +++--
 AVM/Message/Base.lean                    | 16 +++-------
 AVM/Message/Data.lean                    |  2 --
 AVM/Program.lean                         |  8 ++---
 Applib/Surface/Member.lean               |  3 +-
 Applib/Surface/Program.lean              | 16 +++++-----
 Apps/Kudos.lean                          | 18 +++++------
 Apps/KudosBank.lean                      | 40 ++++++++++--------------
 Apps/OwnedCounter.lean                   | 14 ++++-----
 SUMMARY.md                               |  2 +-
 Tests/Applib/Surface/Program/Syntax.lean |  2 +-
 21 files changed, 93 insertions(+), 141 deletions(-)
 create mode 100644 AVM/Logic/Base.lean

diff --git a/AVM/Authorization.lean b/AVM/Authorization.lean
index bb667490..5d89e011 100644
--- a/AVM/Authorization.lean
+++ b/AVM/Authorization.lean
@@ -25,6 +25,7 @@ def PrivateKey.universal : PrivateKey where
 private def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key
 
 structure Signature where
+  user : PublicKey
   private signature : PrivateKey
 
 -- Mock function that returns the `raw` bytes of the signature
@@ -33,8 +34,10 @@ def Signature.raw (_s : Signature) : Nat := 0
 instance : BEq Signature where
   beq a b := a.raw == b.raw
 
-def Signature.sign {lab : Ecosystem.Label} (_msg : MessageData lab) (key : PrivateKey) : Signature where
+def Signature.sign {lab : Ecosystem.Label} (_msg : MessageData lab) (key : PrivateKey) (pub : PublicKey) : Signature where
+  user := pub
   signature := key
 
 -- mock function
-def checkSignature {lab : Ecosystem.Label} (_msg : MessageData lab) (sig : Signature) (pub : PublicKey) : Bool := checkKey pub sig.signature
+def checkSignature {lab : Ecosystem.Label} (_msg : MessageData lab) (sigs : List Signature) (pub : PublicKey)  : Bool :=
+  sigs.any (fun sig => sig.user == pub && checkKey pub sig.signature)
diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean
index d8819219..bfe01a48 100644
--- a/AVM/Class/Label.lean
+++ b/AVM/Class/Label.lean
@@ -33,9 +33,6 @@ structure Label : Type 1 where
 
   ConstructorId : Type
   ConstructorArgs : ConstructorId -> SomeType
-  ConstructorSignatureId : ConstructorId → Type := fun _ => Empty
-  ConstructorSignatureIdEnum : (s : ConstructorId) → FinEnum (ConstructorSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [constructorsEnum : FinEnum ConstructorId]
   [constructorsRepr : Repr ConstructorId]
   [constructorsBEq : BEq ConstructorId]
@@ -43,9 +40,6 @@ structure Label : Type 1 where
 
   DestructorId : Type := Empty
   DestructorArgs : DestructorId -> SomeType := fun _ => ⟨PUnit⟩
-  DestructorSignatureId : DestructorId → Type := fun _ => Empty
-  DestructorSignatureIdEnum : (s : DestructorId) → FinEnum (DestructorSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [destructorsEnum : FinEnum DestructorId]
   [destructorsRepr : Repr DestructorId]
   [destructorsBEq : BEq DestructorId]
@@ -53,9 +47,6 @@ structure Label : Type 1 where
 
   MethodId : Type
   MethodArgs : MethodId -> SomeType
-  MethodSignatureId : MethodId → Type := fun _ => Empty
-  MethodSignatureIdEnum : (s : MethodId) → FinEnum (MethodSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [methodsEnum : FinEnum MethodId]
   [methodsRepr : Repr MethodId]
   [methodsBEq : BEq MethodId]
@@ -86,12 +77,6 @@ inductive Label.MemberId (lab : Class.Label) : Type where
   | methodId (methodId : lab.MethodId) : MemberId lab
   | upgradeId : MemberId lab
 
-abbrev Label.MemberId.SignatureId {lab : Class.Label} : Label.MemberId lab → Type
-  | .methodId m => lab.MethodSignatureId m
-  | .destructorId m => lab.DestructorSignatureId m
-  | .constructorId m => lab.ConstructorSignatureId m
-  | .upgradeId => Empty
-
 instance Label.MemberId.instHashable {lab : Class.Label} : Hashable (Class.Label.MemberId lab) where
   hash l := Hashable.Mix.run do
     mix lab
@@ -162,15 +147,6 @@ def Label.MemberId.Args {lab : Class.Label} (memberId : MemberId lab) : SomeType
   | methodId c => lab.MethodArgs c
   | upgradeId => ⟨PUnit⟩
 
-def Label.ConstructorId.SignatureId {lab : Class.Label} (constrId : lab.ConstructorId) : Type :=
-  lab.ConstructorSignatureId constrId
-
-def Label.DestructorId.SignatureId {lab : Class.Label} (destrId : lab.DestructorId) : Type :=
-  lab.DestructorSignatureId destrId
-
-def Label.MethodId.SignatureId {lab : Class.Label} (methodId : lab.MethodId) : Type :=
-  lab.MethodSignatureId methodId
-
 instance Label.hasTypeRep : TypeRep Label where
   rep := Rep.atomic "AVM.Class.Label"
 
diff --git a/AVM/Class/Member.lean b/AVM/Class/Member.lean
index 556752d7..1674d798 100644
--- a/AVM/Class/Member.lean
+++ b/AVM/Class/Member.lean
@@ -2,15 +2,6 @@ import AVM.Program
 
 namespace AVM.Class
 
-def Label.ConstructorId.Signatures {lab : Class.Label} (constrId : lab.ConstructorId) : Type :=
-  constrId.SignatureId -> Signature
-
-def Label.DestructorId.Signatures {lab : Class.Label} (destrId : lab.DestructorId) : Type :=
-  destrId.SignatureId -> Signature
-
-def Label.MethodId.Signatures {lab : Class.Label} (methodId : lab.MethodId) : Type :=
-  methodId.SignatureId -> Signature
-
 structure Constructor {lab : Ecosystem.Label} (cid : lab.ClassId) (constrId : cid.label.ConstructorId) : Type 1 where
   /-- Constructor call body. -/
   body : constrId.Args.type → Program.{0} lab.toScope (ObjectData cid)
diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean
index f8f37bc3..1c45a879 100644
--- a/AVM/Class/Translation/Logics.lean
+++ b/AVM/Class/Translation/Logics.lean
@@ -78,7 +78,7 @@ def checkMessageResourceValues {lab : Ecosystem.Label} (vals : List (Program.Mes
   List.all₂
     (fun val res =>
       let try msg : Message lab := Message.fromResource res
-      msg.data.id == val.id && msg.data.args === val.args && msg.data.logicRef == val.logicRef)
+      msg.data.id == val.id && msg.data.args === val.args)
     vals
     resMsgs
 
diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean
index f97abc05..7f9a78d7 100644
--- a/AVM/Class/Translation/Messages.lean
+++ b/AVM/Class/Translation/Messages.lean
@@ -1,7 +1,6 @@
 import AVM.Ecosystem
 import AVM.Class
 import AVM.Message
-import AVM.Class.Translation.Logics
 
 namespace AVM.Class
 
@@ -14,15 +13,15 @@ def Constructor.message
   (vals : Vals.type)
   (newId : ObjectId)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
   let data : MessageData lab :=
     { id := .classMember (.constructorId constrId)
-      logicRef := Logic.trivialLogicRef
       vals
       args
       recipients := [newId] }
-  { data, signatures }
+  { data,
+    signatures := signatures data }
 
 def Destructor.message
   {lab : Ecosystem.Label}
@@ -33,15 +32,15 @@ def Destructor.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : destrId.Args.type)
-  (signatures : destrId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
   let data : MessageData lab :=
     { id := .classMember (.destructorId destrId)
-      logicRef := Logic.trivialLogicRef
       vals
       args
       recipients := [selfId] }
-  { data, signatures }
+  { data,
+    signatures := signatures data }
 
 def Method.message
   {lab : Ecosystem.Label}
@@ -52,15 +51,15 @@ def Method.message
   (vals : Vals.type)
   (selfId : ObjectId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Message lab :=
   let data : MessageData lab :=
     { id := .classMember (.methodId methodId)
-      logicRef := Logic.trivialLogicRef
       vals
       args
       recipients := [selfId] }
-  { data, signatures }
+  { data,
+    signatures := signatures data }
 
 def Upgrade.message
   {lab : Ecosystem.Label}
@@ -69,12 +68,11 @@ def Upgrade.message
   : Message lab :=
   let data : MessageData lab :=
     { id := .classMember (classId := classId) .upgradeId
-      logicRef := Logic.trivialLogicRef
       Vals := ⟨PUnit⟩
       vals := PUnit.unit
       args := .unit
       recipients := [selfId] }
-  { data, signatures := fun f => nomatch f}
+  { data, signatures := []}
 
 end AVM.Class
 
@@ -86,18 +84,18 @@ def MultiMethod.message
   (method : MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures)
+  (signatures : MessageData lab → List Signature)
   (vals : (method.body selves args).params.Product)
   (data : MultiMethodData)
   (rands : MultiMethodRandoms data)
   : Message lab :=
   let data : MessageData lab :=
     { id := .multiMethodId multiId
-      logicRef := Logic.trivialLogicRef
       Vals := ⟨(method.body selves args).params.Product⟩
       vals
       args
       recipients :=
         (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList)
           ++ rands.constructedNonces.toList.map (·.value) }
-  { data, signatures }
+  { data,
+    signatures := signatures data }
diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean
index de31b78d..cdf54a57 100644
--- a/AVM/Class/Translation/Tasks.lean
+++ b/AVM/Class/Translation/Tasks.lean
@@ -160,7 +160,7 @@ private partial def Class.Constructor.task'
   (newId : ObjectId)
   (r : Nat)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (ObjectData classId)) := constr.body args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (newObjectData : ULift (ObjectData classId)) : ActionData :=
@@ -193,7 +193,7 @@ private partial def Class.Destructor.task'
   (r : Nat)
   (self : Object classId)
   (args : destructorId.Args.type)
-  (signatures : destructorId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift Unit) := destructor.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (_ : ULift Unit) : ActionData :=
@@ -223,7 +223,7 @@ private partial def Class.Method.task'
   (r : Nat)
   (self : Object classId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body : Program.{1} lab.toScope (ULift (Object classId)) := method.body self args |>.lift
   let mkActionData (rands : List Nat) (vals : body.params.Product) (lobj : ULift (Object classId)) : ActionData :=
@@ -274,7 +274,7 @@ partial def Ecosystem.MultiMethod.task'
   (method : Ecosystem.MultiMethod multiId)
   (selves : multiId.Selves)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures)
+  (signatures : MessageData lab → List Signature)
   : Task' :=
   let body := method.body selves args
 
diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean
index 16cf77f1..85031335 100644
--- a/AVM/Ecosystem/Label/Base.lean
+++ b/AVM/Ecosystem/Label/Base.lean
@@ -19,9 +19,6 @@ structure Label : Type 1 where
   MultiMethodObjectArgNames : MultiMethodId → Type := fun _ => PUnit
   /-- Class identifiers for `self` arguments. -/
   MultiMethodObjectArgClass : {f : MultiMethodId} → MultiMethodObjectArgNames f → ClassId
-  MultiMethodSignatureId : MultiMethodId → Type := fun _ => Empty
-  MultiMethodSignatureIdEnum : (s : MultiMethodId) → FinEnum (MultiMethodSignatureId s)
-    := by intro s; cases s <;> infer_instance
   [ObjectArgNamesEnum (f : MultiMethodId) : FinEnum (MultiMethodObjectArgNames f)]
   [ObjectArgNamesBEq (f : MultiMethodId) : BEq (MultiMethodObjectArgNames f)]
   [multiMethodsFinite : FinEnum MultiMethodId]
@@ -101,8 +98,6 @@ namespace MultiMethodId
 abbrev Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType :=
   lab.MultiMethodArgs multiId
 
-abbrev SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId
-
 def ObjectArgNames {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type :=
   lab.MultiMethodObjectArgNames multiId
 
@@ -186,10 +181,6 @@ instance instLawfulBEq {lab : Ecosystem.Label} : LawfulBEq lab.MemberId where
       subst x; simp
     contradiction
 
-abbrev SignatureId (lab : Ecosystem.Label) : MemberId lab → Type
-  | .classMember m => m.SignatureId
-  | .multiMethodId m => m.SignatureId
-
 abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType.{0} :=
   match memberId with
   | multiMethodId f => lab.MultiMethodArgs f
diff --git a/AVM/Ecosystem/Member.lean b/AVM/Ecosystem/Member.lean
index 14bf1d0d..8bd99d7e 100644
--- a/AVM/Ecosystem/Member.lean
+++ b/AVM/Ecosystem/Member.lean
@@ -92,9 +92,6 @@ def data
 
 end MultiMethodResult
 
-def Ecosystem.Label.MultiMethodId.Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type :=
-  multiId.SignatureId -> Signature
-
 structure Ecosystem.MultiMethod {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type 1 where
   /-- Computes the result of a multiMethod call. See `MultiMethodResult`. -/
   body (selves : multiId.Selves) (args : multiId.Args.type) : Program.{1} lab.toScope (MultiMethodResult multiId)
diff --git a/AVM/Logic.lean b/AVM/Logic.lean
index 5f58da13..86c9712b 100644
--- a/AVM/Logic.lean
+++ b/AVM/Logic.lean
@@ -3,6 +3,7 @@ import Anoma
 import AVM.Object
 import AVM.Message
 import AVM.Action.DummyResource
+import AVM.Logic.Base
 
 namespace AVM.Logic
 
diff --git a/AVM/Logic/Base.lean b/AVM/Logic/Base.lean
new file mode 100644
index 00000000..73998243
--- /dev/null
+++ b/AVM/Logic/Base.lean
@@ -0,0 +1,15 @@
+import Anoma
+import AVM.Ecosystem.Label.Base
+
+namespace AVM.Logic
+
+def classLogicRef {lab : Ecosystem.Label} (classId : lab.ClassId) : Anoma.LogicRef :=
+  classId.label.logicRef
+
+def trivialLogicRef : Anoma.LogicRef := Anoma.LogicRef.mk "Anoma.TrivialLogic"
+
+def trivialLogic : Anoma.Logic :=
+  { reference := trivialLogicRef,
+    function := fun _ => true }
+
+abbrev builtinLogics : List Anoma.Logic := [trivialLogic]
diff --git a/AVM/Message.lean b/AVM/Message.lean
index cbb4f680..251c5aa4 100644
--- a/AVM/Message.lean
+++ b/AVM/Message.lean
@@ -2,6 +2,7 @@ import AVM.Class.Label
 import AVM.Ecosystem.Label
 import AVM.Ecosystem.Data
 import AVM.Authorization
+import AVM.Logic.Base
 
 namespace AVM
 
@@ -9,7 +10,7 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
   { Val := ⟨PUnit⟩,
     Label := ⟨SomeMessage⟩,
     label := msg,
-    logicRef := msg.message.data.logicRef,
+    logicRef := Logic.trivialLogicRef,
     value := PUnit.unit,
     quantity := 1,
     nullifierKeyCommitment := default,
@@ -18,7 +19,6 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res
 
 def SomeMessage.fromResource (res : Anoma.Resource) : Option SomeMessage :=
   let try msg : SomeMessage := tryCast res.label
-  check (msg.message.data.logicRef == res.logicRef)
   some msg
 
 def Message.toResource {lab : Ecosystem.Label} (msg : Message lab) (nonce : Anoma.Nonce) : Anoma.Resource :=
@@ -30,3 +30,6 @@ def Message.fromResource {lab : Ecosystem.Label} (res : Anoma.Resource) : Option
 
 def Resource.isSomeMessage (res : Anoma.Resource) : Bool :=
   Option.isSome (SomeMessage.fromResource res)
+
+def Message.checkSignature {lab : Ecosystem.Label} (msg : Message lab) (pub : PublicKey)  : Bool :=
+  AVM.checkSignature msg.data msg.signatures pub
diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean
index 17579faf..891b3ac0 100644
--- a/AVM/Message/Base.lean
+++ b/AVM/Message/Base.lean
@@ -6,18 +6,11 @@ namespace AVM
 /-- A message is a communication sent from one object to another in the AVM. -/
 structure Message (lab : Ecosystem.Label) : Type 1 where
   data : MessageData lab
-  /-- The signature of the arguments -/
-  signatures : data.id.SignatureId → Signature
+  /-- Signatures for `data`. -/
+  signatures : List Signature
 
 def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat :=
-  let {data := {id := id, ..}, signatures := signatures, ..} := msg
-  match id with
-  | .multiMethodId m => lab.MultiMethodSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-  | .classMember (classId := clab) c => match c with
-    | .methodId m => clab.label.MethodSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .destructorId m => clab.label.DestructorSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .constructorId m => clab.label.ConstructorSignatureIdEnum m |>.toList.map (fun s => signatures s |>.raw)
-    | .upgradeId => []
+  msg.signatures.map Signature.raw
 
 instance Message.instHashable (lab : Ecosystem.Label) : Hashable (Message lab) where
   hash m := Hashable.Mix.run do
@@ -52,10 +45,9 @@ instance : Inhabited SomeMessage where
                     { id := .classMember (classId := .unit) (.constructorId PUnit.unit)
                       Vals := ⟨PUnit⟩
                       vals := PUnit.unit
-                      logicRef := default
                       args := PUnit.unit
                       recipients := [] },
-                  signatures f := nomatch f }}
+                  signatures := [] }}
 
 def Message.toSomeMessage {lab : Ecosystem.Label} (msg : Message lab) : SomeMessage :=
   { label := lab, message := msg }
diff --git a/AVM/Message/Data.lean b/AVM/Message/Data.lean
index 4d5ec91b..b2f38c83 100644
--- a/AVM/Message/Data.lean
+++ b/AVM/Message/Data.lean
@@ -13,8 +13,6 @@ structure MessageData (lab : Ecosystem.Label) : Type 1 where
     associated Resource Logic cannot fetch object resources from the Anoma
     system or generate new object identifiers. -/
   vals : Vals.type
-  /-- Resource logic reference for the message logic. -/
-  logicRef : Anoma.LogicRef
   /-- The arguments of the message. -/
   args : id.Args.type
   /-- The recipients of the message. -/
diff --git a/AVM/Program.lean b/AVM/Program.lean
index de8b2cc1..7fcf8f9e 100644
--- a/AVM/Program.lean
+++ b/AVM/Program.lean
@@ -14,7 +14,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.SignatureId -> Signature)
+    (signatures : MessageData eid.label → List Signature)
     (next : ObjectId → Program scope ReturnType)
     : Program scope ReturnType
   | /-- Destructor call. -/
@@ -24,7 +24,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.SignatureId -> Signature)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Method call. -/
@@ -34,7 +34,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.SignatureId -> Signature)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- MultiMethod call. -/
@@ -43,7 +43,7 @@ inductive Program.{u} (scope : Scope.Label) (ReturnType : Type u) : Type (max u
     (mid : eid.label.MultiMethodId)
     (selvesIds : mid.SelvesIds)
     (args : mid.Args.type)
-    (signatures : mid.SignatureId -> Signature)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program scope ReturnType)
     : Program scope ReturnType
   | /-- Object upgrade -/
diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean
index 3a9bc86f..a6080854 100644
--- a/Applib/Surface/Member.lean
+++ b/Applib/Surface/Member.lean
@@ -11,8 +11,7 @@ macro "noMethods" : term => `(fun x => Empty.elim x)
 
 def unsigned
   {lab : Ecosystem.Label}
-  {SignatureId : Type}
-  : MessageData lab → SignatureId → Signature := fun msg _ => Signature.sign msg PrivateKey.universal
+  : MessageData lab → List Signature := fun _ => []
 
 def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId}
  (body : (self : cl) → methodId.Args.type → Program i.label.toScope cl)
diff --git a/Applib/Surface/Program.lean b/Applib/Surface/Program.lean
index a6d0818f..69193038 100644
--- a/Applib/Surface/Program.lean
+++ b/Applib/Surface/Program.lean
@@ -13,7 +13,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (cid : eid.label.ClassId)
     (constrId : cid.label.ConstructorId)
     (args : constrId.Args.type)
-    (signatures : constrId.Signatures)
+    (signatures : MessageData eid.label → List Signature)
     (next : ObjectId → Program lab α)
     : Program lab α
   | destroy
@@ -23,7 +23,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (destrId : cid.label.DestructorId)
     (selfId : ObjectId)
     (args : destrId.Args.type)
-    (signatures : destrId.Signatures)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | call
@@ -33,7 +33,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (methodId : cid.label.MethodId)
     (selfId : ObjectId)
     (args : methodId.Args.type)
-    (signatures : methodId.Signatures)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | multiCall
@@ -42,7 +42,7 @@ inductive Program (lab : Scope.Label) : (α : Type u) → Type (u + 1) where
     (multiId : eid.label.MultiMethodId)
     (selves : multiId.SelvesIds)
     (args : multiId.Args.type)
-    (signatures : multiId.Signatures)
+    (signatures : MessageData eid.label → List Signature)
     (next : Program lab α)
     : Program lab α
   | upgrade
@@ -125,7 +125,7 @@ def Program.create'
   (inScope : i.label ∈ lab)
   (constrId : i.classId.label.ConstructorId)
   (args : constrId.Args.type)
-  (signatures : constrId.Signatures)
+  (signatures : MessageData i.label → List Signature)
   (next : Reference C → Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -146,7 +146,7 @@ def Program.destroy'
   (inScope : i.label ∈ lab)
   (destrId : i.classId.label.DestructorId)
   (args : destrId.Args.type)
-  (signatures : destrId.Signatures)
+  (signatures : MessageData i.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -168,7 +168,7 @@ def Program.call'
   (inScope : i.label ∈ lab)
   (methodId : i.classId.label.MethodId)
   (args : methodId.Args.type)
-  (signatures : methodId.Signatures)
+  (signatures : MessageData i.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let ⟨eid, _⟩ := inScope
@@ -203,7 +203,7 @@ def Program.multiCall'
   (multiId : eid.label.MultiMethodId)
   (selves : multiId.SelvesReferences)
   (args : multiId.Args.type)
-  (signatures : multiId.Signatures)
+  (signatures : MessageData eid.label → List Signature)
   (next : Program lab α)
   : Program lab α :=
   let selves' : multiId.SelvesIds := fun x => selves x |>.ref.objId
diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean
index 7b4730c0..babbde9a 100644
--- a/Apps/Kudos.lean
+++ b/Apps/Kudos.lean
@@ -104,17 +104,14 @@ def clab : Class.Label where
   MethodId := Methods
   MethodArgs := fun
     | Methods.Transfer => ⟨TransferArgs⟩
-  MethodSignatureId := Methods.SignatureId
 
   ConstructorId := Constructors
   ConstructorArgs := fun
     | Constructors.Mint => ⟨MintArgs⟩
-  ConstructorSignatureId := Constructors.SignatureId
 
   DestructorId := Destructors
   DestructorArgs := fun
     | Destructors.Burn => ⟨PUnit⟩
-  DestructorSignatureId := Destructors.SignatureId
 
 inductive MultiMethods where
   | Merge
@@ -199,17 +196,17 @@ def kudosMint : @Class.Constructor label .unit Constructors.Mint := defConstruct
         owner := args.originator
         originator := args.originator : Kudos}
   ⟫)
-  (invariant := fun (args : MintArgs) signatures => checkSignature (signatures .originator) args.originator)
+  (invariant := fun msg (args : MintArgs) => msg.checkSignature args.originator)
 
 def kudosTransfer : @Class.Method label .unit Methods.Transfer := defMethod Kudos
   (body := fun (self : Kudos) (args : TransferArgs) =>
     ⟪return {self with owner := args.newOwner : Kudos}⟫)
-  (invariant := fun (self : Kudos) (_args : TransferArgs) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun msg (self : Kudos) (_args : TransferArgs) =>
+    msg.checkSignature self.owner)
 
 def kudosBurn : @Class.Destructor label .unit Destructors.Burn := defDestructor
-  (invariant := fun (self : Kudos) (_args : PUnit) signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun msg (self : Kudos) (_args : PUnit) =>
+    msg.checkSignature self.owner
     && self.originator == self.owner)
 
 def kudosClass : @Class label .unit where
@@ -243,10 +240,11 @@ def kudosEcosystem : Ecosystem label where
                     }
                   }
                 ⟫)
-        (invariant := fun kudos _args _signatures =>
+        (invariant := fun msg kudos _args =>
                   let k1 := kudos .Kudos1
                   let k2 := kudos .Kudos2
-                  k1.originator == k2.originator
+                  msg.checkSignature k1.owner
+                  && k1.originator == k2.originator
                   && k1.owner == k2.owner)
 
     | .Split =>
diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean
index 954e2fbd..84667023 100644
--- a/Apps/KudosBank.lean
+++ b/Apps/KudosBank.lean
@@ -250,7 +250,6 @@ def BankLabel : Class.Label where
     | Methods.Transfer => ⟨TransferArgs⟩
     | Methods.Mint => ⟨MintArgs⟩
     | Methods.Burn => ⟨BurnArgs⟩
-  MethodSignatureId := Methods.SignatureId
 
   ConstructorId := Constructors
   ConstructorArgs := fun
@@ -259,7 +258,6 @@ def BankLabel : Class.Label where
   DestructorId := Destructors
   DestructorArgs := fun
     | Destructors.Close => ⟨PUnit⟩
-  DestructorSignatureId := Destructors.SignatureId
 
 inductive MultiMethods where
   | IssueCheck
@@ -405,12 +403,6 @@ def label : AVM.Ecosystem.Label where
      | .auction => Classes.Auction
    | MultiMethods.EndAuction => fun
      | .auction => Classes.Auction
-  MultiMethodSignatureId := fun
-    | .IssueCheck => IssueCheck.SignatureId
-    | .DepositCheck => DepositCheck.SignatureId
-    | .NewAuction => NewAuction.SignatureId
-    | .Bid => Bid.SignatureId
-    | .EndAuction => EndAuction.SignatureId
   ObjectArgNamesBEq (f : MultiMethods) := by cases f <;> exact inferInstance
   ObjectArgNamesEnum (f : MultiMethods) := by cases f <;> exact inferInstance
 
@@ -474,7 +466,7 @@ def kudosTransfer : @Class.Method label Classes.Bank Methods.Transfer := defMeth
   ⟫)
   (invariant := fun (msg : Message label) (self : KudosBank) (args : TransferArgs) =>
     0 < args.quantity
-    && checkSignature msg.data (msg.signatures Methods.Transfer.SignatureId.owner) args.oldOwner
+    && msg.checkSignature args.oldOwner
     && args.quantity <= self.getBalance args.oldOwner args.denom)
 
 def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod KudosBank
@@ -483,15 +475,15 @@ def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod Kudos
       self.overBalances (fun b => b
         |> Balances.subTokens args.denom.originator args.denom args.quantity)
   ⟫)
-  (invariant := fun (self : KudosBank) (args : BurnArgs) signatures =>
-    checkSignature (signatures .originator) args.denom.originator
-    && checkSignature (signatures .owner) args.owner
+  (invariant := fun (msg : Message label) (self : KudosBank) (args : BurnArgs) =>
+    msg.checkSignature args.denom.originator
+    && msg.checkSignature args.owner
     && 0 < args.quantity
     && args.quantity <= self.getBalance args.denom.originator args.denom)
 
 def kudosClose : @Class.Destructor label Classes.Bank Destructors.Close := defDestructor
-  (invariant := fun (self : KudosBank) (_args : PUnit) signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun (msg : Message label) (self : KudosBank) (_args : PUnit) =>
+    msg.checkSignature self.owner
     && self.balances.isEmpty)
 
 def kudosClass : @Class label Classes.Bank where
@@ -544,9 +536,9 @@ def issueCheck : @Ecosystem.MultiMethod label .IssueCheck :=
                           quantity := args.quantity
                           : Check }]}
     ⟫)
-  (invariant := fun selves args signatures =>
+  (invariant := fun msg selves args =>
     let bank := selves .bank
-    checkSignature (signatures .owner) args.owner
+    msg.checkSignature args.owner
     && 0 < args.quantity
     && args.quantity <= bank.getBalance args.owner args.denomination)
 
@@ -572,8 +564,8 @@ def depositCheck : @Ecosystem.MultiMethod label .DepositCheck :=
           | .bank => .Disassembled
           | .check => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
-    checkSignature (signatures .owner) (selves .check).owner)
+  (invariant := fun msg selves _args =>
+    msg.checkSignature (selves .check).owner)
 
 def newAuction : @Ecosystem.MultiMethod label .NewAuction :=
   defMultiMethod label .NewAuction
@@ -596,8 +588,8 @@ def newAuction : @Ecosystem.MultiMethod label .NewAuction :=
           match arg with
           | .check => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
-    checkSignature (signatures .owner) (selves .check).owner)
+  (invariant := fun msg selves _args =>
+    msg.checkSignature (selves .check).owner)
 
 def bid : @Ecosystem.MultiMethod label .Bid :=
   defMultiMethod label .Bid
@@ -632,10 +624,10 @@ def bid : @Ecosystem.MultiMethod label .Bid :=
           | .check => .Destroyed
           | .auction => .Disassembled }
     ⟫)
-  (invariant := fun selves _args signatures =>
+  (invariant := fun msg selves _args =>
     let bid := selves .check
     let auction := selves .auction
-    checkSignature (signatures .owner) bid.owner
+    msg.checkSignature bid.owner
     && bid.denomination == auction.biddingDenomination
     && bid.quantity > auction.highestBid)
 
@@ -663,9 +655,9 @@ def endAuction : @Ecosystem.MultiMethod label .EndAuction :=
           match arg with
           | .auction => .Destroyed }
     ⟫)
-  (invariant := fun selves _args signatures =>
+  (invariant := fun msg selves _args =>
     let auction := selves .auction
-    checkSignature (signatures .owner) auction.owner)
+    msg.checkSignature auction.owner)
 
 def kudosEcosystem : Ecosystem label where
   classes := fun
diff --git a/Apps/OwnedCounter.lean b/Apps/OwnedCounter.lean
index edbfe861..577197d4 100644
--- a/Apps/OwnedCounter.lean
+++ b/Apps/OwnedCounter.lean
@@ -62,12 +62,10 @@ def clab : Class.Label where
   MethodArgs := fun
     | Methods.Incr => ⟨Nat⟩
     | Methods.Transfer => ⟨PublicKey⟩
-  MethodSignatureId := Methods.SignatureId
   ConstructorId := Constructors
   ConstructorArgs := fun
     | Constructors.Zero => ⟨Unit⟩
   DestructorId := Destructors
-  DestructorSignatureId := Destructors.SignatureId
 
 def label : Ecosystem.Label := Ecosystem.Label.singleton clab
 
@@ -97,19 +95,19 @@ def counterConstructor : @Class.Constructor label .unit Constructors.Zero := def
 
 def counterIncr : @Class.Method label .unit Methods.Incr := defMethod OwnedCounter
   (body := fun (self : OwnedCounter) (step : Nat) => ⟪return self.incrementBy step⟫)
-  (invariant := fun (self : OwnedCounter) (_step : Nat) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun (msg : Message label) (self : OwnedCounter) (_step : Nat) =>
+    msg.checkSignature self.owner)
 
 def counterTransfer : @Class.Method label .unit Methods.Transfer := defMethod OwnedCounter
   (body := fun (self : OwnedCounter) (newOwner : PublicKey) =>
     ⟪return {self with owner := newOwner : OwnedCounter}⟫)
-  (invariant := fun (self : OwnedCounter) (_newOwner : PublicKey) signatures =>
-    checkSignature (signatures .owner) self.owner)
+  (invariant := fun msg (self : OwnedCounter) (_newOwner : PublicKey) =>
+    msg.checkSignature self.owner)
 
 /-- We only allow the counter to be destroyed if its count is at least 10 -/
 def counterDestroy : @Class.Destructor label .unit Destructors.Ten := defDestructor
-  (invariant := fun (self : OwnedCounter) () signatures =>
-    checkSignature (signatures .owner) self.owner
+  (invariant := fun (msg : Message label) (self : OwnedCounter) () =>
+    msg.checkSignature self.owner
     && self.count >= 10)
 
 def counterClass : @Class label .unit where
diff --git a/SUMMARY.md b/SUMMARY.md
index 295d7b2c..00ec1366 100644
--- a/SUMMARY.md
+++ b/SUMMARY.md
@@ -208,7 +208,7 @@ Action sending the call messages:
   - `recipients : List ObjectId`. The recipients of the message.
   - `signatures : List Signature`. Authorization signatures for the message. Each signature consists of:
     - public identifier of the signer,
-    - signature data: the message `id` and `args` cryptographically signed with signer's private key.
+    - signature data: the message `id`, `args` and `vals` cryptographically signed with signer's private key.
 
 ### Constructor
 - `Class.Constructor` in `AVM/Class/Member.lean`
diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean
index 1a179ecb..1f264724 100644
--- a/Tests/Applib/Surface/Program/Syntax.lean
+++ b/Tests/Applib/Surface/Program/Syntax.lean
@@ -217,7 +217,7 @@ namespace OwnedCounter
 
 abbrev scope := label.toScope
 
-example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program scope (Reference OwnedCounter) := ⟪
+example (r : Reference OwnedCounter) (newOwner : AVM.PublicKey) : Program scope (Reference OwnedCounter) := ⟪
   c := fetch r
   call OwnedCounter.Methods.Transfer r newOwner
   r' := create OwnedCounter OwnedCounter.Constructors.Zero ()

From a42e4e4f3f8430942ec4397cec78259586d5fa5f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?=C5=81ukasz=20Czajka?=
 <62751+lukaszcz@users.noreply.github.com>
Date: Mon, 20 Oct 2025 14:25:31 +0200
Subject: [PATCH 6/7] Update Apps/KudosBank.lean

Co-authored-by: Copilot <175728472+Copilot@users.noreply.github.com>
---
 Apps/KudosBank.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean
index 84667023..4af2545e 100644
--- a/Apps/KudosBank.lean
+++ b/Apps/KudosBank.lean
@@ -11,7 +11,7 @@ def Std.HashMap.modifyDefault
 
 structure Denomination where
   originator : PublicKey
-  deriving BEq, Inhabited, Hashable
+  deriving BEq, Inhabited, Hashable, DecidableEq
 
 structure Account where
   assets : Std.HashMap Denomination Nat

From ec4ced7c63f2ecb350a7e0f1eb1f0be6f69102d3 Mon Sep 17 00:00:00 2001
From: Lukasz Czajka <lukasz@heliax.dev>
Date: Wed, 22 Oct 2025 13:56:23 +0200
Subject: [PATCH 7/7] fix compilation

---
 AVM/Class/Translation/Logics.lean | 15 ---------------
 AVM/Message/Base.lean             |  2 +-
 Apps/Kudos.lean                   |  4 ++--
 Apps/OwnedCounter.lean            |  2 +-
 4 files changed, 4 insertions(+), 19 deletions(-)

diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean
index 1c45a879..f9c03103 100644
--- a/AVM/Class/Translation/Logics.lean
+++ b/AVM/Class/Translation/Logics.lean
@@ -3,21 +3,6 @@ import AVM.Message
 import AVM.Logic
 import AVM.Ecosystem
 
-namespace AVM.Logic
-
-def classLogicRef {lab : Ecosystem.Label} (classId : lab.ClassId) : Anoma.LogicRef :=
-  classId.label.logicRef
-
-def trivialLogicRef : Anoma.LogicRef := Anoma.LogicRef.mk "Anoma.TrivialLogic"
-
-def trivialLogic : Anoma.Logic :=
-  { reference := trivialLogicRef,
-    function := fun _ => true }
-
-abbrev builtinLogics : List Anoma.Logic := [trivialLogic]
-
-end AVM.Logic
-
 namespace AVM.Program
 
 structure MessageValue (lab : Ecosystem.Label) where
diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean
index 891b3ac0..32749e32 100644
--- a/AVM/Message/Base.lean
+++ b/AVM/Message/Base.lean
@@ -14,7 +14,7 @@ def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat
 
 instance Message.instHashable (lab : Ecosystem.Label) : Hashable (Message lab) where
   hash m := Hashable.Mix.run do
-    mix m.id
+    mix m.data.id
 
 instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) where
   rep := Rep.composite "AVM.Message" [Rep.atomic lab.name]
diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean
index babbde9a..000a5c85 100644
--- a/Apps/Kudos.lean
+++ b/Apps/Kudos.lean
@@ -14,8 +14,8 @@ open Applib
 /- 3. Burn: The owner of a kudos token can destroy it if themself is the originator of the token -/
 
 structure KudosData where
-  originator : PublicKey
-  owner : PublicKey
+  originator : AVM.PublicKey
+  owner : AVM.PublicKey
   deriving DecidableEq, Inhabited, Hashable
 
 structure Kudos extends KudosData where
diff --git a/Apps/OwnedCounter.lean b/Apps/OwnedCounter.lean
index 577197d4..200b8f30 100644
--- a/Apps/OwnedCounter.lean
+++ b/Apps/OwnedCounter.lean
@@ -5,7 +5,7 @@ open Applib
 
 structure OwnedCounter where
   count : Nat
-  owner : PublicKey
+  owner : AVM.PublicKey
   deriving Inhabited, Repr, BEq, Hashable
 
 namespace OwnedCounter