feat: Add simple authorization for class members

AVM/Authorization.lean

@@ -0,0 +1,39 @@
+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 u where
+  msg : A
+  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
+
+instance {A B} (msgA : A) (msgB : B) : HBEq (Signature msgA) (Signature msgB) where
+  hbeq a b := a.raw == b.raw
+
+def Signature.sign {A : Type u} (msg : A) (key : PrivateKey) : Signature msg where
+  signature := key
+  msg
+
+-- 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
 
@@ -33,21 +34,33 @@ 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
   [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
+  DestructorSignatureIdEnum : (s : DestructorId) → FinEnum (DestructorSignatureId s)
+    := by intro s; cases s <;> infer_instance
   [destructorsFinite : Fintype DestructorId]
   [destructorsRepr : Repr DestructorId]
   [destructorsBEq : BEq DestructorId]
+  [destructorsLawfulBEq : LawfulBEq DestructorId]
 
   MethodId : Type
   MethodArgs : MethodId -> SomeType
+  MethodSignatureId : MethodId → Type := fun _ => Empty
+  MethodSignatureIdEnum : (s : MethodId) → FinEnum (MethodSignatureId s)
+    := by intro s; cases s <;> infer_instance
   [methodsFinite : Fintype MethodId]
   [methodsRepr : Repr MethodId]
   [methodsBEq : BEq MethodId]
+  [methodsLawfulBEq : LawfulBEq MethodId]
 
 def Label.dummy : Label where
   name := "Dummy"
@@ -59,25 +72,24 @@ 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)
+  MethodId := Empty
+  MethodArgs f := nomatch f
 
 def Label.logicRef (lab : Label) : Anoma.LogicRef :=
   ⟨"class-logic-" ++ lab.name⟩
 
-inductive Label.MemberId (lab : Class.Label) where
+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 m => lab.ConstructorSignatureId m
+  | .upgradeId => Empty
+
 instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId lab) where
   beq a b :=
     match a, b with
@@ -92,16 +104,37 @@ 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]
 
-def Label.ConstructorId.Args {lab : Class.Label} (constrId : lab.ConstructorId) : SomeType :=
+abbrev Label.ConstructorId.Args {lab : Class.Label} (constrId : lab.ConstructorId) : SomeType :=
   lab.ConstructorArgs constrId
 
-def Label.MethodId.Args {lab : Class.Label} (methodId : lab.MethodId) : SomeType :=
+abbrev Label.MethodId.Args {lab : Class.Label} (methodId : lab.MethodId) : SomeType :=
   lab.MethodArgs methodId
 
-def Label.DestructorId.Args {lab : Class.Label} (destructorId : lab.DestructorId) : SomeType.{0} :=
+abbrev Label.DestructorId.Args {lab : Class.Label} (destructorId : lab.DestructorId) : SomeType.{0} :=
   lab.DestructorArgs destructorId
 
 def Label.MemberId.Args {lab : Class.Label} (memberId : MemberId lab) : SomeType :=
@@ -111,6 +144,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

@@ -7,20 +7,20 @@ structure Constructor {lab : Ecosystem.Label} (cid : lab.ClassId) (constrId : ci
   body : constrId.Args.type → Program.{0} lab (ObjectData cid)
   /-- Extra constructor logic. The constructor invariant is combined with
       auto-generated constructor body constraints to create the constructor logic. -/
-  invariant : constrId.Args.type → Bool
+  invariant : (args : constrId.Args.type) → constrId.Signatures args →  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 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,7 +14,9 @@ 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
+  check h : msg.id == .classMember (Label.MemberId.constructorId constrId)
+  let argsData := cast (by simp! [eq_of_beq h]) msg.args
+  let signatures := cast (by grind only) msg.signatures
   let try vals : (constr.body argsData).params.Product := tryCast msg.vals
   let newObjData := constr.body argsData |>.value vals
   let consumedResObjs := Logic.selectObjectResources args.consumed
@@ -25,7 +27,7 @@ private def Constructor.Message.logicFun
     && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs
     && Logic.checkResourcesEphemeral consumedResObjs
     && Logic.checkResourcesPersistent createdResObjs
-    && constr.invariant argsData
+    && constr.invariant argsData signatures
 
 /-- Creates a message logic function for a given destructor. -/
 private def Destructor.Message.logicFun
@@ -36,17 +38,18 @@ 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
+  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
   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
+    && destructor.invariant selfObj argsData signatures
 
-/-- Creates a message logic function for a given method. -/
 private def Method.Message.logicFun
   {lab : Ecosystem.Label}
   {classId : lab.ClassId}
@@ -55,14 +58,16 @@ 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
+  check h : msg.id == .classMember (Label.MemberId.methodId methodId)
+  let argsData : methodId.Args.type := cast (by simp! [eq_of_beq h]) 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 signatures : methodId.Signatures argsData := cast (by grind only) msg.signatures
+  check method.invariant selfObj argsData signatures
   let createdObject : Object classId := body |>.value vals
   Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs
     && Logic.checkResourcesPersistent consumedResObjs
@@ -171,7 +176,8 @@ 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
+  check h : msg.id == .multiMethodId multiId
+  let fargs : multiId.Args.type := cast (by simp! [eq_of_beq h]) msg.args
   let consumedResObjs := Logic.selectObjectResources args.consumed
   let createdResObjs := Logic.selectObjectResources args.created
   let try (argsConsumedSelves, argsConstructedEph, .unit) :=
@@ -180,32 +186,34 @@ def MultiMethod.Message.logicFun
       |>.splitsExact [multiId.numObjectArgs, data.numConstructed]
   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 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⟩
-      let reassembled : List ObjectValue := res.assembled.withOldUidList.map (fun x => mkObjectValue x.arg x.objectData)
-      let constructedObjects : List ObjectValue := res.constructed
-      let consumedDestroyedObjects : List ObjectValue :=
-        multiId.objectArgNamesVec.toList.filterMap (fun arg =>
+  let signatures := cast (by grind only) msg.signatures
+  check method.invariant argsConsumedObjects fargs signatures
+  let try vals : prog.params.Product := tryCast msg.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⟩
+  let reassembled : List ObjectValue := res.assembled.withOldUidList.map (fun x => mkObjectValue x.arg x.objectData)
+  let constructedObjects : List ObjectValue := res.constructed
+  let consumedDestroyedObjects : List ObjectValue :=
+    multiId.objectArgNamesVec.toList.filterMap
+      (fun arg =>
         let argObject := argsConsumedObjects arg
         match res.argDeconstruction arg with
         | .Destroyed => argObject |>.data.toObjectValue argObject.uid
         | .Disassembled => none)
-      let try (argsCreated, argsConstructed, argsSelvesDestroyedEph, .unit) :=
-        createdResObjs
-        |> Logic.filterOutDummy
-        |>.splitsExact [reassembled.length, data.numConstructed, data.numSelvesDestroyed]
-      Logic.checkResourceValues reassembled argsCreated.toList
-        && Logic.checkResourceValues constructedObjects argsConstructed.toList
-        && Logic.checkResourceValues constructedObjects argsConstructedEph.toList
-        && Logic.checkResourceValues consumedDestroyedObjects argsSelvesDestroyedEph.toList
-        && Logic.checkResourcesPersistent argsConsumedSelves.toList
-        && Logic.checkResourcesPersistent argsCreated.toList
-        && Logic.checkResourcesPersistent argsConstructed.toList
-        && Logic.checkResourcesEphemeral argsConstructedEph.toList
-        && Logic.checkResourcesEphemeral argsSelvesDestroyedEph.toList
+  let try (argsCreated, argsConstructed, argsSelvesDestroyedEph, .unit) :=
+    createdResObjs
+    |> Logic.filterOutDummy
+    |>.splitsExact [reassembled.length, data.numConstructed, data.numSelvesDestroyed]
+  Logic.checkResourceValues reassembled argsCreated.toList
+    && Logic.checkResourceValues constructedObjects argsConstructed.toList
+    && Logic.checkResourceValues constructedObjects argsConstructedEph.toList
+    && Logic.checkResourceValues consumedDestroyedObjects argsSelvesDestroyedEph.toList
+    && Logic.checkResourcesPersistent argsConsumedSelves.toList
+    && Logic.checkResourcesPersistent argsCreated.toList
+    && Logic.checkResourcesPersistent argsConstructed.toList
+    && Logic.checkResourcesEphemeral argsConstructedEph.toList
+    && Logic.checkResourcesEphemeral argsSelvesDestroyedEph.toList
 
 def MultiMethod.Message.logic
   {lab : Ecosystem.Label}