Squashed commit of the following:

commit 35ebc97
Author: Jan Mas Rovira <[email protected]>
Date:   Mon Sep 22 17:28:56 2025 +0200

    destructors

commit 18fcdd3
Author: Jan Mas Rovira <[email protected]>
Date:   Mon Sep 22 13:39:48 2025 +0200

    syntax

commit 6df404c
Author: Jan Mas Rovira <[email protected]>
Date:   Mon Sep 22 13:13:24 2025 +0200

    constrs and destr

commit 2165afe
Author: Jan Mas Rovira <[email protected]>
Date:   Mon Sep 22 10:17:33 2025 +0200

    sigs

commit 82e19b9
Author: Jan Mas Rovira <[email protected]>
Date:   Sun Sep 21 23:39:58 2025 +0200

    proofs

commit 2e06fac
Author: Jan Mas Rovira <[email protected]>
Date:   Fri Sep 19 16:33:54 2025 +0200

    wip

commit 72faad1
Author: Jan Mas Rovira <[email protected]>
Date:   Fri Sep 19 08:25:44 2025 +0200

    noSignatures

commit fb64072
Author: Jan Mas Rovira <[email protected]>
Date:   Thu Sep 18 15:23:58 2025 +0200

    signatures wip

commit 4a5495e
Author: Jan Mas Rovira <[email protected]>
Date:   Wed Sep 17 17:29:26 2025 +0200

    store owner

commit dc14617
Author: Jan Mas Rovira <[email protected]>
Date:   Wed Sep 17 15:42:56 2025 +0200

    basic authorization for class members

Author: janmasrovira

AVM/Authorization.lean

@@ -0,0 +1,31 @@
+import Mathlib.Data.Fintype.Basic
+import Prelude
+
+structure PublicKey where
+  key : Nat
+  deriving Repr, BEq, Hashable, DecidableEq, Inhabited
+
+def PublicKey.universal : PublicKey where
+  key := 0
+
+instance PublicKey.hasTypeRep : TypeRep PublicKey where
+  rep := Rep.atomic "PublicKey"
+
+structure PrivateKey where
+  key : Nat
+  deriving Repr, BEq, Hashable, DecidableEq
+
+def PrivateKey.universal : PrivateKey where
+  key := 0
+
+-- mock function
+def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key
+
+structure Signature {A : Type u} (msg : A) : Type where
+  signature : PrivateKey
+
+def Signature.sign {A : Type u} (msg : A) (key : PrivateKey) : Signature msg where
+  signature := key
+
+-- mock function
+def checkSignature {A : Type u} {msg : A} (sig : Signature msg) (pub : PublicKey) : Bool := checkKey pub sig.signature

AVM/Class/Label.lean

@@ -2,6 +2,7 @@ import Anoma.Resource
 import Prelude
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.FinEnum
+import AVM.Authorization
 
 abbrev AVM.ObjectId := Anoma.ObjectId
 
@@ -36,18 +37,23 @@ structure Label : Type 1 where
   [constructorsFinite : Fintype ConstructorId]
   [constructorsRepr : Repr ConstructorId]
   [constructorsBEq : BEq ConstructorId]
+  [constructorsLawfulBEq : LawfulBEq ConstructorId]
 
   DestructorId : Type := Empty
   DestructorArgs : DestructorId -> SomeType := fun _ => ⟨PUnit⟩
+  DestructorSignatureId : DestructorId → Type := fun _ => Empty
   [destructorsFinite : Fintype DestructorId]
   [destructorsRepr : Repr DestructorId]
   [destructorsBEq : BEq DestructorId]
+  [destructorsLawfulBEq : LawfulBEq DestructorId]
 
   MethodId : Type
   MethodArgs : MethodId -> SomeType
+  MethodSignatureId : MethodId → Type := fun _ => Empty
   [methodsFinite : Fintype MethodId]
   [methodsRepr : Repr MethodId]
   [methodsBEq : BEq MethodId]
+  [methodsLawfulBEq : LawfulBEq MethodId]
 
 def Label.dummy : Label where
   name := "Dummy"
@@ -59,22 +65,21 @@ def Label.dummy : Label where
   constructorsRepr := inferInstanceAs (Repr PUnit)
   constructorsBEq := inferInstanceAs (BEq PUnit)
   DestructorId := Empty
-  DestructorArgs := fun _ => ⟨PUnit⟩
-  destructorsFinite := inferInstanceAs (Fintype Empty)
-  destructorsRepr := inferInstanceAs (Repr Empty)
-  destructorsBEq := inferInstanceAs (BEq Empty)
-  MethodId := PUnit
-  MethodArgs := fun _ => ⟨PUnit⟩
-  methodsFinite := inferInstanceAs (Fintype PUnit)
-  methodsRepr := inferInstanceAs (Repr PUnit)
-  methodsBEq := inferInstanceAs (BEq PUnit)
-
-inductive Label.MemberId (lab : Class.Label) where
+  MethodId := Empty
+  MethodArgs f := nomatch f
+
+inductive Label.MemberId (lab : Class.Label) : Type where
   | constructorId (constrId : lab.ConstructorId) : MemberId lab
   | destructorId (destructorId : lab.DestructorId) : MemberId lab
   | 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 _ => Empty
+  | .upgradeId => Empty
+
 instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId lab) where
   beq a b :=
     match a, b with
@@ -89,6 +94,27 @@ instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId l
     | _, methodId _ => false
     | upgradeId, upgradeId => true
 
+instance Label.MemberId.instReflBEq {lab : Class.Label} : ReflBEq lab.MemberId where
+  rfl := by
+    intro a
+    have := lab.constructorsLawfulBEq
+    have := lab.destructorsLawfulBEq
+    have := lab.methodsLawfulBEq
+    cases a
+    iterate 4 {
+      unfold BEq.beq Label.MemberId.hasBEq
+      simp
+    }
+
+instance Label.MemberId.instLawfulBEq {lab : Class.Label} : LawfulBEq (Class.Label.MemberId lab) where
+  eq_of_beq := by
+    intro a b
+    have := lab.constructorsLawfulBEq
+    have := lab.destructorsLawfulBEq
+    have := lab.methodsLawfulBEq
+    unfold BEq.beq Label.MemberId.hasBEq
+    cases a <;> cases b <;> simp
+
 instance Label.MemberId.hasTypeRep (lab : Class.Label) : TypeRep (Class.Label.MemberId lab) where
   rep := Rep.composite "AVM.Class.Label.MemberId" [Rep.atomic lab.name]
 
@@ -108,6 +134,34 @@ 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
+
 instance Label.hasTypeRep : TypeRep Label where
   rep := Rep.atomic "AVM.Class.Label"
 

AVM/Class/Member.lean

@@ -13,14 +13,14 @@ structure Destructor {lab : Ecosystem.Label} (cid : lab.ClassId) (destructorId :
   /-- Destructor call body. -/
   body : (self : Object cid) → destructorId.Args.type → Program.{0} lab PUnit
   /-- Extra destructor logic. -/
-  invariant : (self : Object cid) → destructorId.Args.type → Bool
+  invariant : (self : Object cid) → (args : destructorId.Args.type) → destructorId.Signatures args → 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 (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) → methodId.Args.type → Bool
+  invariant : (self : Object cid) → (args : methodId.Args.type) → methodId.Signatures args → Bool
 
 /-- A class member is a constructor, a destructor or a method. -/
 inductive Member {lab : Ecosystem.Label} (cid : lab.ClassId) where

AVM/Class/Translation/Logics.lean

@@ -14,8 +14,8 @@ private def Constructor.Message.logicFun
   (args : Logic.Args)
   : Bool :=
   let try msg : Message lab := Message.fromResource args.self
-  let try argsData := SomeType.cast msg.args
-  let try vals : (constr.body argsData).params.Product := tryCast msg.vals
+  let try argsData := SomeType.cast msg.contents.args
+  let try vals : (constr.body argsData).params.Product := tryCast msg.contents.vals
   let newObjData := constr.body argsData |>.value vals
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
@@ -36,17 +36,24 @@ private def Destructor.Message.logicFun
   (args : Logic.Args)
   : Bool :=
   let try msg : Message lab := Message.fromResource args.self
-  let try argsData := SomeType.cast msg.args
-  let consumedResObjs := Logic.selectObjectResources args.consumed
-  let createdResObjs := Logic.selectObjectResources args.created
-  let! [selfRes] := consumedResObjs
-  let try selfObj : Object classId := Object.fromResource selfRes
-  Logic.checkResourceValues [selfObj.toObjectValue] createdResObjs
-    && Logic.checkResourcesPersistent consumedResObjs
-    && Logic.checkResourcesEphemeral createdResObjs
-    && destructor.invariant selfObj argsData
+  match msg with
+  | {id := id, contents := contents} =>
+  -- TODO check syntax
+  if h : id == .classMember (Label.MemberId.destructorId destructorId)
+  then
+    let contents : MessageContents lab (.classMember (Label.MemberId.destructorId destructorId)) := eq_of_beq h ▸ contents
+    let argsData := contents.args
+    let signatures : destructorId.Signatures argsData := contents.signatures
+    let consumedResObjs := Logic.selectObjectResources args.consumed
+    let createdResObjs := Logic.selectObjectResources args.created
+    let! [selfRes] := consumedResObjs
+    let try selfObj : Object classId := Object.fromResource selfRes
+    Logic.checkResourceValues [selfObj.toObjectValue] createdResObjs
+      && Logic.checkResourcesPersistent consumedResObjs
+      && Logic.checkResourcesEphemeral createdResObjs
+      && destructor.invariant selfObj argsData signatures
+  else false
 
-/-- Creates a message logic function for a given method. -/
 private def Method.Message.logicFun
   {lab : Ecosystem.Label}
   {classId : lab.ClassId}
@@ -55,18 +62,25 @@ private def Method.Message.logicFun
   (args : Logic.Args)
   : Bool :=
   let try msg : Message lab := Message.fromResource args.self
-  let try argsData := SomeType.cast msg.args
-  let consumedResObjs := Logic.selectObjectResources args.consumed
-  let createdResObjs := Logic.selectObjectResources args.created
-  let! [selfRes] := consumedResObjs
-  let try selfObj : Object classId := Object.fromResource selfRes
-  check method.invariant selfObj argsData
-  let body := method.body selfObj argsData
-  let try vals : body.params.Product := tryCast msg.vals
-  let createdObject : Object classId := body |>.value vals
-  Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs
-    && Logic.checkResourcesPersistent consumedResObjs
-    && Logic.checkResourcesPersistent createdResObjs
+  match msg with
+  | {id := id, contents := contents} =>
+  if h : id == .classMember (Label.MemberId.methodId methodId)
+  then
+    let contents : MessageContents lab (.classMember (Label.MemberId.methodId methodId)) := eq_of_beq h ▸ contents
+    let argsData : methodId.Args.type := contents.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 contents.vals
+    let signatures : methodId.Signatures argsData := contents.signatures
+    check method.invariant selfObj argsData signatures
+    let createdObject : Object classId := body |>.value vals
+    Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs
+      && Logic.checkResourcesPersistent consumedResObjs
+      && Logic.checkResourcesPersistent createdResObjs
+  else false
 
 private def Upgrade.Message.logicFun
   {lab : Ecosystem.Label}
@@ -108,7 +122,7 @@ private def logicFun
     nMessages + 1 == (Logic.filterOutDummy args.consumed).length
       && consumedMessageResources.all fun res =>
         let try msg : Message lab := Message.fromResource res
-        let! [recipient] := msg.recipients.toList
+        let! [recipient] := msg.contents.recipients.toList
         consumedObject.uid == recipient
 
 def Constructor.Message.logic
@@ -157,7 +171,7 @@ def MultiMethod.Message.logicFun
   (data : MultiMethodData)
   : Bool :=
   let try msg : Message lab := Message.fromResource args.self
-  let try fargs : multiId.Args.type := SomeType.cast msg.args
+  let try fargs : multiId.Args.type := SomeType.cast msg.contents.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let try (argsConsumedSelves, argsConstructedEph, argsDestroyed, .unit) :=
@@ -167,7 +181,7 @@ def MultiMethod.Message.logicFun
   let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves.toList
   let prog := method.body argsConsumedObjects fargs
   method.invariant argsConsumedObjects fargs
-   && let try vals : prog.params.Product := tryCast msg.vals
+   && let try vals : prog.params.Product := tryCast msg.contents.vals
       let res : MultiMethodResult multiId := prog |>.value vals
       let consumedUid (arg : multiId.ObjectArgNames) : Anoma.ObjectId := argsConsumedObjects arg |>.uid
       let mkObjectValue {classId : lab.ClassId} (arg : multiId.ObjectArgNames) (d : ObjectData classId) : ObjectValue := ⟨consumedUid arg, d⟩
@@ -228,7 +242,7 @@ private def logicFun
           | .multiMethodId multiId =>
             let try selves : multiId.Selves := multiId.ConsumedToSelves consumedObjectResources
             nMessages + multiId.numObjectArgs == (Logic.filterOutDummy args.consumed).length
-              && Label.MultiMethodId.SelvesToVector selves (fun o => o.uid) ≍? msg.recipients
+              && Label.MultiMethodId.SelvesToVector selves (fun o => o.uid) ≍? msg.contents.recipients
 
 def logic
   {lab : Ecosystem.Label}