wip

Author: janmasrovira

AVM/Class/Label.lean

@@ -86,6 +86,9 @@ instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId l
     | _, destructorId _ => false
     | methodId m1, methodId m2 => lab.methodsBEq.beq m1 m2
 
+instance Label.MemberId.instReflBEq {lab : Class.Label} : ReflBEq (Class.Label.MemberId lab) where
+  rfl := sorry
+
 instance Label.MemberId.hasTypeRep (lab : Class.Label) : TypeRep (Class.Label.MemberId lab) where
   rep := Rep.composite "AVM.Class.Label.MemberId" [Rep.atomic lab.name]
 

AVM/Class/Translation/Logics.lean

@@ -61,14 +61,36 @@ private def Method.Message.logicFun
   let! [selfRes] := consumedResObjs
   let try selfObj : Object classId := Object.fromResource selfRes
   check method.invariant selfObj argsData
-  check method.authorization selfObj argsData sorry
+  let signatures0 : msg.id.Signatures msg.args := msg.signatures
+  let signatures : methodId.Signatures argsData := sorry
+  check method.authorization selfObj argsData signatures
   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
 
+private def Method.Message.logicFun2
+  {lab : Ecosystem.Label}
+  {classId : lab.ClassId}
+  {methodId : classId.label.MethodId}
+  (method : Class.Method classId methodId)
+  (args : Logic.Args)
+  : Bool :=
+  let try msg : Message lab := Message.fromResource args.self
+
+  -- 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 signatures0 : msg.id.Signatures msg.args := msg.signatures
+  -- let signatures : methodId.Signatures argsData := sorry
+  -- false
+
 /-- The class logic checks if all consumed messages in the action correspond to
     class members, the single consumed object is the receiver, and there is
     at least one message. -/

AVM/Message.lean

@@ -21,6 +21,7 @@ structure Message (lab : Ecosystem.Label) : Type 1 where
   /-- The arguments of the message. -/
   args : id.Args.type
   /-- The signature of the arguments -/
+  -- TODO sign over memberId and args. Anything else?
   signatures : id.Signatures args
   /-- Extra data. -/
   data : id.Data