fix: authorization

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,20 @@ 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
+  user : PublicKey
   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) (pub : PublicKey) : Signature where
+  user := pub
   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) (sigs : List Signature) (pub : PublicKey)  : Bool :=
+  sigs.any (fun sig => sig.user == pub && checkKey pub sig.signature)

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
 
@@ -34,29 +33,20 @@ 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]
   [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
   [destructorsEnum : FinEnum 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
   [methodsEnum : FinEnum MethodId]
   [methodsRepr : Repr MethodId]
   [methodsBEq : BEq MethodId]
@@ -87,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
@@ -163,34 +147,6 @@ 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.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

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
@@ -78,7 +63,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)
     vals
     resMsgs
 
@@ -93,16 +78,15 @@ 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
   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)
@@ -160,11 +144,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
@@ -182,7 +165,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
@@ -193,16 +176,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
@@ -214,7 +196,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}
@@ -224,16 +206,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
@@ -314,8 +295,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. -/