From 559b62ca14a60f9448defabdeae94773914a4451 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Mon, 22 Sep 2025 18:42:09 +0200 Subject: [PATCH 01/17] Squashed commit of the following: commit 35ebc97300b2c3c2eb4168b81effe1978659a7d7 Author: Jan Mas Rovira Date: Mon Sep 22 17:28:56 2025 +0200 destructors commit 18fcdd33671391479c8706c356c50da77964c077 Author: Jan Mas Rovira Date: Mon Sep 22 13:39:48 2025 +0200 syntax commit 6df404ca9ddac5e7e623e55de1b1908e47776f2b Author: Jan Mas Rovira Date: Mon Sep 22 13:13:24 2025 +0200 constrs and destr commit 2165afe1ec7a9344bb7445359be15dcee6d8f17f Author: Jan Mas Rovira Date: Mon Sep 22 10:17:33 2025 +0200 sigs commit 82e19b98d4697731a58a8b8d86564277da5f6197 Author: Jan Mas Rovira Date: Sun Sep 21 23:39:58 2025 +0200 proofs commit 2e06fac00cd53a8027b0e6eb3ed35f61afa2fb75 Author: Jan Mas Rovira Date: Fri Sep 19 16:33:54 2025 +0200 wip commit 72faad1b9f2bb35ede9fff2a3b055bb1fe626551 Author: Jan Mas Rovira Date: Fri Sep 19 08:25:44 2025 +0200 noSignatures commit fb64072e59cba2c5a9fb2d851d9c60274a3c69fd Author: Jan Mas Rovira Date: Thu Sep 18 15:23:58 2025 +0200 signatures wip commit 4a5495ee71535697c74600c55c0c68d3f126c0cc Author: Jan Mas Rovira Date: Wed Sep 17 17:29:26 2025 +0200 store owner commit dc146171b946c1ad2d9387c83a31a14a385ea665 Author: Jan Mas Rovira Date: Wed Sep 17 15:42:56 2025 +0200 basic authorization for class members --- AVM/Authorization.lean | 31 ++++++++++ AVM/Class/Label.lean | 76 ++++++++++++++++++++---- AVM/Class/Member.lean | 4 +- AVM/Class/Translation/Logics.lean | 70 +++++++++++++--------- AVM/Class/Translation/Messages.lean | 74 +++++++++++++---------- AVM/Class/Translation/Tasks.lean | 26 ++++---- AVM/Ecosystem/Label/Base.lean | 67 ++++++++++++++++++--- AVM/Message.lean | 10 ++-- AVM/Message/Base.lean | 43 +++++++++----- AVM/Object.lean | 12 ++-- AVM/Program.lean | 33 +++++----- Applib.lean | 1 - Applib/Authorization.lean | 18 ------ Applib/Surface/Member.lean | 13 ++-- Applib/Surface/Program.lean | 36 ++++++----- Applib/Surface/Program/Syntax.lean | 28 ++++----- Applib/Translation.lean | 1 + Apps/Kudos.lean | 28 ++++++++- Apps/KudosBank.lean | 54 +++++++++++++---- Apps/OwnedCounter.lean | 34 ++++++++++- Apps/TwoCounter.lean | 4 +- Tests/Applib/Surface/Program/Syntax.lean | 64 ++++++++++---------- 22 files changed, 499 insertions(+), 228 deletions(-) create mode 100644 AVM/Authorization.lean delete mode 100644 Applib/Authorization.lean diff --git a/AVM/Authorization.lean b/AVM/Authorization.lean new file mode 100644 index 00000000..de293247 --- /dev/null +++ b/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 diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean index 4e710da4..0dc3d019 100644 --- a/AVM/Class/Label.lean +++ b/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" diff --git a/AVM/Class/Member.lean b/AVM/Class/Member.lean index dc61a3ad..26ff7cb8 100644 --- a/AVM/Class/Member.lean +++ b/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 diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index ba399d16..f2b07ba2 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/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} diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean index 3bf32471..fe1c9f49 100644 --- a/AVM/Class/Translation/Messages.lean +++ b/AVM/Class/Translation/Messages.lean @@ -14,13 +14,16 @@ def Constructor.message (vals : Vals.type) (newId : ObjectId) (args : constrId.Args.type) + (signatures : Class.Label.MemberId.constructorId constrId |>.Signatures args) : Message lab := - { id := .classMember (.constructorId constrId), - data := .unit - logicRef := Constructor.Message.logic.{0, 0} constr |>.reference - vals, - args, - recipients := List.Vector.singleton newId } + { id := .classMember (.constructorId constrId) + contents := + { data := .unit + logicRef := Constructor.Message.logic.{0, 0} constr |>.reference + vals + args + signatures + recipients := List.Vector.singleton newId }} def Destructor.message {lab : Ecosystem.Label} @@ -31,13 +34,16 @@ def Destructor.message (vals : Vals.type) (selfId : ObjectId) (args : destrId.Args.type) + (signatures : Class.Label.MemberId.destructorId destrId |>.Signatures args) : Message lab := { id := .classMember (.destructorId destrId) - data := .unit - logicRef := Destructor.Message.logic.{0, 0} destr |>.reference - vals - args - recipients := List.Vector.singleton selfId } + contents := + { data := .unit + logicRef := Destructor.Message.logic.{0, 0} destr |>.reference + vals + args + signatures + recipients := List.Vector.singleton selfId }} def Method.message {lab : Ecosystem.Label} @@ -48,13 +54,16 @@ def Method.message (vals : Vals.type) (selfId : ObjectId) (args : methodId.Args.type) + (signatures : Class.Label.MemberId.methodId methodId |>.Signatures args) : Message lab := { id := .classMember (.methodId methodId) - data := .unit - logicRef := Method.Message.logic.{0, 0} method |>.reference - vals - args - recipients := List.Vector.singleton selfId } + contents := + { data := .unit + logicRef := Method.Message.logic.{0, 0} method |>.reference + vals + args + signatures + recipients := List.Vector.singleton selfId }} def Upgrade.message {lab : Ecosystem.Label} @@ -62,12 +71,14 @@ def Upgrade.message (selfId : ObjectId) : Message lab := { id := .classMember (classId := classId) .upgradeId - data := .unit - logicRef := Upgrade.Message.logic.{0, 0} classId |>.reference - Vals := ⟨PUnit⟩ - vals := PUnit.unit - args := .unit - recipients := List.Vector.singleton selfId } + contents := + { data := .unit + logicRef := Upgrade.Message.logic.{0, 0} classId |>.reference + Vals := ⟨PUnit⟩ + vals := PUnit.unit + args := .unit + signatures f := nomatch f + recipients := List.Vector.singleton selfId }} end AVM.Class @@ -79,15 +90,16 @@ def MultiMethod.message (method : MultiMethod multiId) (selves : multiId.Selves) (args : multiId.Args.type) - (body : Program lab (MultiMethodResult multiId)) - (vals : body.params.Product) + (vals : (method.body selves args).params.Product) : Message lab := - let res : MultiMethodResult multiId := body.value vals + let res : MultiMethodResult multiId := method.body selves args |>.value vals let data := res.data { id := .multiMethodId multiId - logicRef := MultiMethod.Message.logic.{0, 0} method data |>.reference - data - Vals := ⟨body.params.Product⟩ - vals - args - recipients := Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) } + contents := + { logicRef := MultiMethod.Message.logic.{0, 0} method data |>.reference + data + Vals := ⟨(method.body selves args).params.Product⟩ + vals + args + signatures := .unit + recipients := Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) }} diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean index fd91f2d8..33036372 100644 --- a/AVM/Class/Translation/Tasks.lean +++ b/AVM/Class/Translation/Tasks.lean @@ -5,6 +5,9 @@ import AVM.Ecosystem import AVM.Class.Translation.Messages import AVM.Action +-- TODO needed? +import AVM.Class.Label + namespace AVM /-- Type of functions which adjust object values by modifications that occurred @@ -59,23 +62,23 @@ private partial def Body.tasks' (cont : α → AdjustFun → Tasks (TasksResult .empty β)) : Tasks (TasksResult body.params β) := match body with - | .constructor classId constrId args next => + | .constructor classId constrId args signatures next => let constr := eco.classes classId |>.constructors constrId Tasks.rand fun newId => Tasks.rand fun r => - let task := constr.task' adjust eco newId r args + let task := constr.task' adjust eco newId r args signatures Tasks.task task.task fun vals => Body.tasks' (task.adjust vals) eco (next newId) cont |>.map (fun res => ⟨res.value, res.adjust, ⟨newId, res.bodyParameterValues⟩⟩) - | .destructor classId destrId selfId args next => + | .destructor classId destrId selfId args signatures next => let destr := eco.classes classId |>.destructors destrId Tasks.fetch selfId fun self => Tasks.rand fun r => - let task := destr.task' adjust eco r (adjust self) args + let task := destr.task' adjust eco r (adjust self) args signatures Tasks.task task.task fun vals => Body.tasks' (task.adjust vals) eco next cont - | .method classId methodId selfId args next => + | .method classId methodId selfId args signatures next => let method := eco.classes classId |>.methods methodId Tasks.fetch selfId fun self => Tasks.rand fun r => - let task := method.task' adjust eco r (adjust self) args + let task := method.task' adjust eco r (adjust self) args signatures Tasks.task task.task fun vals => Body.tasks' (task.adjust vals) eco next cont | .multiMethod multiId selvesIds args next => @@ -139,6 +142,7 @@ private partial def Class.Constructor.task' (newId : ObjectId) (r : Nat) (args : constrId.Args.type) + (signatures : constrId.Signatures args) : Task' := let body : Program.{1} lab (ULift (ObjectData classId)) := constr.body args |>.lift let mkActionData (newObjectData : ULift (ObjectData classId)) : ActionData := @@ -154,7 +158,7 @@ private partial def Class.Constructor.task' { consumed := [consumedObj] created := createdObjects } let mkMessage (vals : body.params.Product) : SomeMessage := - constr.message ⟨body.params.Product⟩ vals newId args + constr.message ⟨body.params.Product⟩ vals newId args signatures Body.task' adjust eco body mkReturn mkActionData mkMessage /-- Creates a Task for a given object destructor. -/ @@ -168,6 +172,7 @@ private partial def Class.Destructor.task' (r : Nat) (self : Object classId) (args : destructorId.Args.type) + (signatures : destructorId.Signatures args) : Task' := let body : Program.{1} lab (ULift Unit) := destructor.body self args |>.lift let mkActionData (_ : ULift Unit) : ActionData := @@ -180,7 +185,7 @@ private partial def Class.Destructor.task' { consumed := [consumedObj] created := createdObjects } let mkMessage (vals : body.params.Product) : SomeMessage := - destructor.message ⟨body.params.Product⟩ vals self.uid args + destructor.message ⟨body.params.Product⟩ vals self.uid args signatures Body.task' adjust eco body mkReturn mkActionData mkMessage /-- Creates a Task for a given method. -/ @@ -194,6 +199,7 @@ private partial def Class.Method.task' (r : Nat) (self : Object classId) (args : methodId.Args.type) + (signatures : methodId.Signatures args) : Task' := let body : Program.{1} lab (ULift (Object classId)) := method.body self args |>.lift let mkActionData (lobj : ULift (Object classId)) : ActionData := @@ -207,7 +213,7 @@ private partial def Class.Method.task' { consumed := [consumedObj] created := [createdObject] } let mkMessage (vals : body.params.Product) : SomeMessage := - method.message ⟨body.params.Product⟩ vals self.uid args + method.message ⟨body.params.Product⟩ vals self.uid args signatures Body.task' adjust eco body mkReturn mkActionData mkMessage private partial def Class.Upgrade.task' @@ -300,7 +306,7 @@ partial def Ecosystem.Label.MultiMethodId.task' ensureUnique := rands.reassembledNewUidNonces.toList } let mkMessage (vals : body.params.Product) : SomeMessage := - ⟨(eco.multiMethods multiId).message selves args body vals⟩ + ⟨(eco.multiMethods multiId).message selves args vals⟩ Body.task' adjust eco body mkResult mkActionData mkMessage diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean index 7dcc7609..511c77b3 100644 --- a/AVM/Ecosystem/Label/Base.lean +++ b/AVM/Ecosystem/Label/Base.lean @@ -1,4 +1,5 @@ import AVM.Class.Label +import AVM.Authorization namespace AVM.Ecosystem @@ -10,6 +11,7 @@ structure Label : Type 1 where [classesEnum : FinEnum ClassId] [classesRepr : Repr ClassId] [classesBEq : BEq ClassId] + [classesDecidableEq : DecidableEq ClassId] MultiMethodId : Type := Empty /-- Type of multiMethod arguments excluding `self` arguments. -/ @@ -23,6 +25,7 @@ structure Label : Type 1 where [multiMethodsFinite : FinEnum MultiMethodId] [multiMethodsRepr : Repr MultiMethodId] [multiMethodsBEq : BEq MultiMethodId] + [multiMethodsLawfulBEq : LawfulBEq MultiMethodId] instance Label.hasTypeRep : TypeRep Label where rep := Rep.atomic "AVM.Ecosystem.Label" @@ -96,6 +99,9 @@ namespace MultiMethodId def Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType := lab.MultiMethodArgs multiId +def Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) (_args : multiId.Args.type) : Type := + Unit + def ObjectArgNames {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodObjectArgNames multiId @@ -120,24 +126,67 @@ def argsClassesVec {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : List. end MultiMethodId -inductive MemberId (lab : Ecosystem.Label) where +inductive MemberId (lab : Ecosystem.Label) : Type where | multiMethodId (funId : lab.MultiMethodId) | classMember {classId : lab.ClassId} (memId : classId.MemberId) namespace MemberId -def Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType := +instance instBEq {lab : Ecosystem.Label} : BEq (MemberId lab) where + beq a b := + have := lab.classesDecidableEq + match a, b with + | .multiMethodId m1, .multiMethodId m2 => + have := lab.multiMethodsBEq + m1 == m2 + | .multiMethodId _ , _ => false + | _, .multiMethodId _ => false + | .classMember (classId := c1) m1, classMember (classId := c2) m2 => + if h : c1 = c2 + then m1 == h ▸ m2 + else false + +instance instReflBEq {lab : Ecosystem.Label} : ReflBEq (MemberId lab) where + rfl := by + have := lab.multiMethodsLawfulBEq + intro a; cases a + unfold BEq.beq instBEq; simp + case classMember classId classMem => + unfold BEq.beq instBEq; + have i : ReflBEq classId.MemberId := @Class.Label.MemberId.instReflBEq classId.label + simp + +-- TODO simplify +instance instLawfulBEq {lab : Ecosystem.Label} : LawfulBEq lab.MemberId where + eq_of_beq := by + intro a b e + have i := lab.multiMethodsLawfulBEq + unfold BEq.beq instBEq at e; simp at e; split at e; simp + apply i.eq_of_beq + assumption + contradiction + contradiction + split at e + case h_4.isTrue _ _ _ _ h => + subst h; + have x := Class.Label.MemberId.instLawfulBEq.eq_of_beq e + subst x; simp + contradiction + +abbrev SignatureId (lab : Ecosystem.Label) : MemberId lab → Type + | .classMember m => m.SignatureId + | _ => Empty + +abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType.{0} := match memberId with | multiMethodId f => lab.MultiMethodArgs f | classMember m => Class.Label.MemberId.Args m -instance hasBEq {lab : Ecosystem.Label} : BEq (Ecosystem.Label.MemberId lab) where - beq a b := - match a, b with - | multiMethodId c1, multiMethodId c2 => lab.multiMethodsBEq.beq c1 c2 - | multiMethodId _, _ => false - | _, multiMethodId _ => false - | classMember c1, classMember c2 => c1 === c2 +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 def numObjectArgs {lab : Ecosystem.Label} (memberId : MemberId lab) : Nat := match memberId with diff --git a/AVM/Message.lean b/AVM/Message.lean index 3c298966..78c08ddf 100644 --- a/AVM/Message.lean +++ b/AVM/Message.lean @@ -1,5 +1,7 @@ -import AVM.Message.Base -import AVM.Label +import AVM.Class.Label +import AVM.Ecosystem.Label +import AVM.Ecosystem.Data +import AVM.Authorization namespace AVM @@ -7,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.contents.logicRef, value := PUnit.unit, quantity := 1, nullifierKeyCommitment := default, @@ -16,7 +18,7 @@ def SomeMessage.toResource (msg : SomeMessage) (nonce : Anoma.Nonce) : Anoma.Res def SomeMessage.fromResource (res : Anoma.Resource.{u, v}) : Option SomeMessage := let try msg : SomeMessage := tryCast res.label - check (msg.message.logicRef == res.logicRef) + check (msg.message.contents.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 e1f165b6..48dc68e4 100644 --- a/AVM/Message/Base.lean +++ b/AVM/Message/Base.lean @@ -2,8 +2,7 @@ import AVM.Ecosystem.Data namespace AVM -/-- A message is a communication sent from one object to another in the AVM. -/ -structure Message (lab : Ecosystem.Label) : Type 1 where +structure MessageContents (lab : Ecosystem.Label) (id : lab.MemberId) : Type 1 where {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 @@ -13,24 +12,36 @@ structure Message (lab : Ecosystem.Label) : Type 1 where vals : Vals.type /-- Resource logic reference for the message logic. -/ logicRef : Anoma.LogicRef - /-- The message ID. -/ - id : lab.MemberId /-- The arguments of the message. -/ args : id.Args.type + /-- The signature of the arguments -/ + signatures : id.Signatures args /-- Extra data. -/ data : id.Data /-- The recipients of the message. -/ recipients : List.Vector ObjectId id.numObjectArgs +/-- 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 + /-- The data that the message carries. -/ + contents : MessageContents lab id + +instance MessageContents.hasBEq {lab : Ecosystem.Label} {id : lab.MemberId} : BEq (MessageContents lab id) where + beq a b := + a.vals === b.vals + && a.args == b.args + && a.recipients == b.recipients + instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) where rep := Rep.composite "AVM.Message" [Rep.atomic lab.name] instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where beq a b := - a.id == b.id - && a.vals === b.vals - && a.args === b.args - && a.recipients ≍? b.recipients + if h : a.id == b.id + then a.contents == eq_of_beq h ▸ b.contents + else false structure SomeMessage : Type 1 where {label : Ecosystem.Label} @@ -45,13 +56,15 @@ instance SomeMessage.hasBEq : BEq SomeMessage where instance : Inhabited SomeMessage where default := { label := Ecosystem.Label.dummy message := - { Vals := ⟨PUnit⟩ - vals := PUnit.unit - data := .unit - logicRef := default - id := .classMember (classId := .unit) (.constructorId PUnit.unit), - args := PUnit.unit - recipients := List.Vector.singleton 0 }} + { id := .classMember (classId := .unit) (.constructorId PUnit.unit), + contents := + { Vals := ⟨PUnit⟩ + vals := PUnit.unit + data := .unit + logicRef := default + args := PUnit.unit + signatures f := nomatch f + recipients := List.Vector.singleton 0 }}} def Message.toSomeMessage {lab : Ecosystem.Label} (msg : Message lab) : SomeMessage := { label := lab, message := msg } diff --git a/AVM/Object.lean b/AVM/Object.lean index d2776703..1630eaab 100644 --- a/AVM/Object.lean +++ b/AVM/Object.lean @@ -2,6 +2,7 @@ import Anoma.Resource import AVM.Ecosystem.Label.Base import AVM.Ecosystem.Data import AVM.Label +import AVM.Authorization namespace AVM @@ -13,7 +14,8 @@ structure ObjectData {lab : Ecosystem.Label} (c : lab.ClassId) where deriving BEq instance ObjectData.inhabited {lab : Ecosystem.Label} (c : lab.ClassId) : Inhabited (ObjectData c) where - default := {quantity := 0, privateFields := c.label.privateFieldsInhabited.default} + default := { quantity := 0 + privateFields := c.label.privateFieldsInhabited.default } instance ObjectData.hasTypeRep {lab : Ecosystem.Label} (c : lab.ClassId) : TypeRep (ObjectData c) where rep := Rep.composite "AVM.ObjectData" [Rep.atomic lab.name, Rep.atomic c.label.name] @@ -109,7 +111,8 @@ def SomeObject.toResource logicRef := label.logicRef, quantity := obj.data.quantity, Val := ⟨Object.Resource.Value classId⟩, - value := ⟨obj.uid, obj.data.privateFields⟩, + value := { uid := obj.uid + privateFields := obj.data.privateFields }, ephemeral := ephemeral, nonce := obj.nonce, nullifierKeyCommitment := default } @@ -128,8 +131,9 @@ def Object.fromResource check (objLab.label == lab) check (res.logicRef == lab.logicRef) let try value : Object.Resource.Value c := tryCast res.value - some { uid := value.uid, - data := ⟨res.quantity, value.privateFields⟩, + some { uid := value.uid + data := { quantity := res.quantity + privateFields := value.privateFields } nonce := res.nonce } def SomeObject.fromResource.{u, v} diff --git a/AVM/Program.lean b/AVM/Program.lean index 790579c9..6ea4c782 100644 --- a/AVM/Program.lean +++ b/AVM/Program.lean @@ -12,6 +12,7 @@ inductive Program.{u} (lab : Ecosystem.Label) (ReturnType : Type u) : Type (max (cid : lab.ClassId) (constrId : cid.label.ConstructorId) (args : constrId.Args.type) + (signatures : constrId.Signatures args) (next : ObjectId → Program lab ReturnType) : Program lab ReturnType | /-- Destructor call. -/ @@ -20,6 +21,7 @@ inductive Program.{u} (lab : Ecosystem.Label) (ReturnType : Type u) : Type (max (destrId : cid.label.DestructorId) (selfId : ObjectId) (args : destrId.Args.type) + (signatures : destrId.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | /-- Method call. -/ @@ -28,6 +30,7 @@ inductive Program.{u} (lab : Ecosystem.Label) (ReturnType : Type u) : Type (max (methodId : cid.label.MethodId) (selfId : ObjectId) (args : methodId.Args.type) + (signatures : methodId.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | /-- MultiMethod call. -/ @@ -64,9 +67,9 @@ def lift.{v, u} (prog : Program lab α) : Program.{max u v} lab (ULift α) := match prog with - | .constructor cid constr args next => .constructor cid constr args (fun a => (next a).lift) - | .destructor cid destrId selfId args next => .destructor cid destrId selfId args next.lift - | .method cid methodId selfId args next => .method cid methodId selfId args next.lift + | .constructor cid constr args signatures next => .constructor cid constr args signatures (fun a => (next a).lift) + | .destructor cid destrId selfId args signatures next => .destructor cid destrId selfId args signatures next.lift + | .method cid methodId selfId args signatures next => .method cid methodId selfId args signatures next.lift | .multiMethod mid selvesIds args next => .multiMethod mid selvesIds args next.lift | .upgrade cid selfId obj next => .upgrade cid selfId obj next.lift | .fetch objId next => .fetch objId (fun a => (next a).lift) @@ -80,12 +83,12 @@ def invoke (next : α → Program lab β) : Program lab β := match prog with - | .constructor cid constrId args cont => - .constructor cid constrId args (fun objId => Program.invoke (cont objId) next) - | .destructor cid destrId selfId args cont => - .destructor cid destrId selfId args (Program.invoke cont next) - | .method cid methodId selfId args cont => - .method cid methodId selfId args (Program.invoke cont next) + | .constructor cid constrId args signatures cont => + .constructor cid constrId args signatures (fun objId => Program.invoke (cont objId) next) + | .destructor cid destrId selfId args signatures cont => + .destructor cid destrId selfId args signatures (Program.invoke cont next) + | .method cid methodId selfId args signatures cont => + .method cid methodId selfId args signatures (Program.invoke cont next) | .multiMethod mid selvesId args cont => .multiMethod mid selvesId args (Program.invoke cont next) | .upgrade cid selfId obj cont => @@ -102,9 +105,9 @@ def invoke `Program.Parameters.Product`). -/ def params {lab : Ecosystem.Label} {α : Type u} (prog : Program lab α) : Parameters := match prog with - | .constructor _ _ _ next => .genId (fun newId => next newId |>.params) - | .destructor _ _ _ _ next => next.params - | .method _ _ _ _ next => next.params + | .constructor _ _ _ _ next => .genId (fun newId => next newId |>.params) + | .destructor _ _ _ _ _ next => next.params + | .method _ _ _ _ _ next => next.params | .multiMethod _ _ _ next => next.params | .upgrade _ _ _ next => next.params | .fetch objId next => .fetch objId (fun obj => next obj |>.params) @@ -114,12 +117,12 @@ def params {lab : Ecosystem.Label} {α : Type u} (prog : Program lab α) : Param `Program.Parameters.Product`). -/ def value {lab : Ecosystem.Label} {α : Type u} (prog : Program lab α) (vals : prog.params.Product) : α := match prog with - | .constructor _ _ _ next => + | .constructor _ _ _ _ next => let ⟨newId, vals'⟩ := vals next newId |>.value vals' - | .destructor _ _ _ _ next => + | .destructor _ _ _ _ _ next => next.value vals - | .method _ _ _ _ next => + | .method _ _ _ _ _ next => next.value vals | .multiMethod _ _ _ next => next.value vals diff --git a/Applib.lean b/Applib.lean index 5b3c7110..4d24a46a 100644 --- a/Applib.lean +++ b/Applib.lean @@ -1,3 +1,2 @@ import Applib.Surface -import Applib.Authorization import Applib.Translation diff --git a/Applib/Authorization.lean b/Applib/Authorization.lean deleted file mode 100644 index 74b06069..00000000 --- a/Applib/Authorization.lean +++ /dev/null @@ -1,18 +0,0 @@ -import Mathlib.Data.Fintype.Basic -import AVM - -namespace Applib - -structure PublicKey where - key : Nat - deriving Repr, BEq, Hashable, DecidableEq, Inhabited - -instance PublicKey.hasTypeRep : TypeRep PublicKey where - rep := Rep.atomic "PublicKey" - -structure PrivateKey where - key : Nat - deriving Repr, BEq, Hashable, DecidableEq - --- mock function -def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean index c08359d4..6410686c 100644 --- a/Applib/Surface/Member.lean +++ b/Applib/Surface/Member.lean @@ -9,9 +9,14 @@ macro "noConstructors" : term => `(fun x => Empty.elim x) macro "noDestructors" : term => `(fun x => Empty.elim x) macro "noMethods" : term => `(fun x => Empty.elim x) +def noSignatures + {Args SignatureId : Type} + {args : Args} + : SignatureId → Signature args := fun _ => Signature.sign args PrivateKey.universal + def defMethod (cl : Type) [i : IsObject cl] {methodId : i.classId.label.MethodId} (body : (self : cl) → methodId.Args.type → Program i.label cl) - (invariant : (self : cl) → methodId.Args.type → Bool := fun _ _ => true) + (invariant : (self : cl) → (args : methodId.Args.type) → methodId.Signatures args → Bool := fun _ _ _ => true) : Class.Method i.classId methodId where invariant (self : Object i.classId) (args : methodId.Args.type) := let self' : cl := i.fromObject self.data @@ -31,10 +36,10 @@ def defConstructor {cl : Type} [i : IsObject cl] {constrId : i.classId.label.Con def defDestructor {cl : Type} [i : IsObject cl] {destructorId : i.classId.label.DestructorId} (body : (self : cl) → destructorId.Args.type → Program i.label PUnit := fun _ _ => Program.return ()) - (invariant : (self : cl) -> destructorId.Args.type → Bool := fun _ _ => true) + (invariant : (self : cl) -> (args : destructorId.Args.type) → destructorId.Signatures args → Bool := fun _ _ _ => true) : Class.Destructor i.classId destructorId where - invariant (self : Object i.classId) (args : destructorId.Args.type) := + invariant (self : Object i.classId) (args : destructorId.Args.type) (signatures : destructorId.Signatures args) := let self' := i.fromObject self.data - invariant self' args + invariant self' args signatures body (self : Object i.classId) (args : destructorId.Args.type) := body (i.fromObject self.data) args |>.toAVM diff --git a/Applib/Surface/Program.lean b/Applib/Surface/Program.lean index 56edccb8..953fe6a4 100644 --- a/Applib/Surface/Program.lean +++ b/Applib/Surface/Program.lean @@ -13,6 +13,7 @@ inductive Program (lab : Ecosystem.Label) : (ReturnType : Type u) → Type (u + (cid : lab.ClassId) (constrId : cid.label.ConstructorId) (args : constrId.Args.type) + (signatures : constrId.Signatures args) (next : ObjectId → Program lab ReturnType) : Program lab ReturnType | destroy @@ -21,6 +22,7 @@ inductive Program (lab : Ecosystem.Label) : (ReturnType : Type u) → Type (u + (destrId : cid.label.DestructorId) (selfId : ObjectId) (args : destrId.Args.type) + (signatures : destrId.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | call @@ -29,6 +31,7 @@ inductive Program (lab : Ecosystem.Label) : (ReturnType : Type u) → Type (u + (methodId : cid.label.MethodId) (selfId : ObjectId) (args : methodId.Args.type) + (signatures : methodId.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | multiCall @@ -65,12 +68,12 @@ inductive Program (lab : Ecosystem.Label) : (ReturnType : Type u) → Type (u + def Program.toAVM {lab ReturnType} (prog : Program lab ReturnType) : AVM.Program lab ReturnType := match prog with - | .create _ cid constrId args next => - .constructor cid constrId args (fun objId => toAVM (next objId)) - | .destroy cid destrId selfId args next => - .destructor cid destrId selfId args (toAVM next) - | .call cid methodId selfId args next => - .method cid methodId selfId args (toAVM next) + | .create _ cid constrId args signatures next => + .constructor cid constrId args signatures (fun objId => toAVM (next objId)) + | .destroy cid destrId selfId args signatures next => + .destructor cid destrId selfId args signatures (toAVM next) + | .call cid methodId selfId args signatures next => + .method cid methodId selfId args signatures (toAVM next) | .multiCall multiId selves args next => .multiMethod multiId selves args (toAVM next) | .upgrade classId selfId obj next => @@ -84,12 +87,12 @@ def Program.toAVM {lab ReturnType} (prog : Program lab ReturnType) : AVM.Program def Program.map {lab : Ecosystem.Label} {A B : Type} (f : A → B) (prog : Program lab A) : Program lab B := match prog with - | .create C cid constrId args next => - .create C cid constrId args (fun x => map f (next x)) - | .destroy cid destrId selfId args next => - .destroy cid destrId selfId args (map f next) - | .call cid methodId selfId args next => - .call cid methodId selfId args (map f next) + | .create C cid constrId args signatures next => + .create C cid constrId args signatures (fun x => map f (next x)) + | .destroy cid destrId selfId args signatures next => + .destroy cid destrId selfId args signatures (map f next) + | .call cid methodId selfId args signatures next => + .call cid methodId selfId args signatures (map f next) | .multiCall multiId selvesIds args next => .multiCall multiId selvesIds args (map f next) | .upgrade classId selfId obj next => @@ -107,9 +110,10 @@ def Program.create' [i : IsObject C] (constrId : i.classId.label.ConstructorId) (args : constrId.Args.type) + (signatures : constrId.Signatures args) (next : Reference C → Program i.label ReturnType) : Program i.label ReturnType := - Program.create C i.classId constrId args (fun objId => next ⟨objId⟩) + Program.create C i.classId constrId args signatures (fun objId => next ⟨objId⟩) def Program.destroy' {ReturnType} @@ -118,9 +122,10 @@ def Program.destroy' [i : IsObject C] (destrId : i.classId.label.DestructorId) (args : destrId.Args.type) + (signatures : destrId.Signatures args) (next : Program i.label ReturnType) : Program i.label ReturnType := - Program.destroy i.classId destrId r.objId args next + Program.destroy i.classId destrId r.objId args signatures next def Program.call' {ReturnType} @@ -129,9 +134,10 @@ def Program.call' [i : IsObject C] (methodId : i.classId.label.MethodId) (args : methodId.Args.type) + (signatures : methodId.Signatures args) (next : Program i.label ReturnType) : Program i.label ReturnType := - Program.call i.classId methodId r.objId args next + Program.call i.classId methodId r.objId args signatures next def Program.upgrade' {ReturnType} diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index d3477fdc..ba4839dc 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -56,20 +56,20 @@ macro_rules `(if $cond then ⟪$thenProg⟫ else Program.return ()) | `(⟪if $cond:term then $thenProg:program ; $p:program⟫) => `(let next := fun () => ⟪$p⟫; if $cond then Program.invoke ⟪$thenProg⟫ next else next ()) - | `(⟪create $c:ident $m:ident $e:term⟫) => - `(Program.create' $c $m $e Program.return) - | `(⟪create $c:ident $m:ident $e:term ; $p:program⟫) => - `(Program.create' $c $m $e (fun _ => ⟪$p⟫)) - | `(⟪$x:ident := create $c:ident $m:ident $e:term ; $p:program⟫) => - `(Program.create' $c $m $e (fun $x => ⟪$p⟫)) - | `(⟪destroy $m:ident $e:term $args:term⟫) => - `(Program.destroy' $e $m $args (Program.return ())) - | `(⟪destroy $m:ident $e:term $args:term ; $p:program⟫) => - `(Program.destroy' $e $m $args (⟪$p⟫)) - | `(⟪call $m:ident $e:term $args:term⟫) => - `(Program.call' $e $m $args (Program.return ())) - | `(⟪call $m:ident $e:term $args:term ; $p:program⟫) => - `(Program.call' $e $m $args (⟪$p⟫)) + | `(⟪create $c:ident $m:ident $e:term $signatures:term⟫) => + `(Program.create' $c $m $e $signatures Program.return) + | `(⟪create $c:ident $m:ident $e:term $signatures:term; $p:program⟫) => + `(Program.create' $c $m $e $signatures (fun _ => ⟪$p⟫)) + | `(⟪$x:ident := create $c:ident $m:ident $e:term $signatures:term; $p:program⟫) => + `(Program.create' $c $m $e $signatures (fun $x => ⟪$p⟫)) + | `(⟪destroy $m:ident $e:term $args:term $signatures:term⟫) => + `(Program.destroy' $e $m $args $signatures (Program.return ())) + | `(⟪destroy $m:ident $e:term $args:term $signatures:term; $p:program⟫) => + `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) + | `(⟪call $m:ident $e:term $args:term $signatures:term⟫) => + `(Program.call' $e $m $args $signatures (Program.return ())) + | `(⟪call $m:ident $e:term $args:term $signatures:term; $p:program⟫) => + `(Program.call' $e $m $args $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term⟫) => `(Program.multiCall' $m $selves $args (Program.return ())) | `(⟪multiCall $m:ident $selves:term $args:term ; $p:program⟫) => diff --git a/Applib/Translation.lean b/Applib/Translation.lean index fb0bed89..dee6873b 100644 --- a/Applib/Translation.lean +++ b/Applib/Translation.lean @@ -1,4 +1,5 @@ import Applib.Surface.Program +import AVM.Authorization namespace Applib diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean index 25c41e47..2b537f84 100644 --- a/Apps/Kudos.lean +++ b/Apps/Kudos.lean @@ -30,6 +30,16 @@ inductive Methods where | Transfer : Methods deriving DecidableEq, Fintype, Repr +namespace Methods + +inductive Transfer.SignatureId : Type where + | owner + +def SignatureId : Methods → Type + | .Transfer => Transfer.SignatureId + +end Methods + inductive Constructors where | Mint : Constructors deriving DecidableEq, Fintype, Repr @@ -38,6 +48,16 @@ inductive Destructors where | Burn : Destructors deriving DecidableEq, Fintype, Repr +namespace Destructors + +inductive Burn.SignatureId : Type where + | owner + +def SignatureId : Destructors → Type + | .Burn => Burn.SignatureId + +end Destructors + inductive Classes where | Kudos : Classes deriving DecidableEq, FinEnum, Repr @@ -73,6 +93,7 @@ def clab : Class.Label where MethodId := Methods MethodArgs := fun | Methods.Transfer => ⟨TransferArgs⟩ + MethodSignatureId := Methods.SignatureId ConstructorId := Constructors ConstructorArgs := fun @@ -81,6 +102,7 @@ def clab : Class.Label where DestructorId := Destructors DestructorArgs := fun | Destructors.Burn => ⟨PUnit⟩ + DestructorSignatureId := Destructors.SignatureId def label : Ecosystem.Label := Ecosystem.Label.singleton clab @@ -112,9 +134,13 @@ def kudosMint : @Class.Constructor label .unit Constructors.Mint := defConstruct 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) def kudosBurn : @Class.Destructor label .unit Destructors.Burn := defDestructor - (invariant := fun (self : Kudos) (_args : PUnit) => self.originator == self.owner) + (invariant := fun (self : Kudos) (_args : PUnit) signatures => + checkSignature (signatures .owner) self.owner + && self.originator == self.owner) def kudosClass : @Class label .unit where constructors := fun diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean index 90c237f6..b5cb3459 100644 --- a/Apps/KudosBank.lean +++ b/Apps/KudosBank.lean @@ -78,7 +78,7 @@ instance hasTypeRep : TypeRep Check where inductive Methods where | Transfer - deriving Repr, BEq, Fintype + deriving Repr, BEq, Fintype, DecidableEq structure TransferArgs where newOwner : PublicKey @@ -159,6 +159,26 @@ inductive Methods where | Burn : Methods deriving DecidableEq, Fintype, Repr +namespace Methods + +inductive Transfer.SignatureId where + | owner + +inductive Mint.SignatureId where + | owner + +inductive Burn.SignatureId where + | owner + | originator + +def SignatureId (m : Methods) : Type := + match m with + | .Transfer => Transfer.SignatureId + | .Mint => Mint.SignatureId + | .Burn => Burn.SignatureId + +end Methods + inductive Constructors where | Open : Constructors deriving DecidableEq, Fintype, Repr @@ -167,6 +187,16 @@ inductive Destructors where | Close : Destructors deriving DecidableEq, Fintype, Repr +namespace Destructors + +inductive Close.SignatureId : Type where + | owner + +def SignatureId : Destructors → Type + | .Close => Close.SignatureId + +end Destructors + open AVM instance Balances.hasTypeRep : TypeRep Balances where @@ -204,8 +234,8 @@ instance TransferArgs.hasTypeRep : TypeRep TransferArgs where structure BurnArgs where denom : Denomination + owner : PublicKey quantity : Nat - key : PrivateKey deriving DecidableEq instance BurnArgs.hasTypeRep : TypeRep BurnArgs where @@ -220,6 +250,7 @@ def BankLabel : Class.Label where | Methods.Transfer => ⟨TransferArgs⟩ | Methods.Mint => ⟨MintArgs⟩ | Methods.Burn => ⟨BurnArgs⟩ + MethodSignatureId := Methods.SignatureId ConstructorId := Constructors ConstructorArgs := fun @@ -228,6 +259,7 @@ def BankLabel : Class.Label where DestructorId := Destructors DestructorArgs := fun | Destructors.Close => ⟨PUnit⟩ + DestructorSignatureId := Destructors.SignatureId inductive Classes where | Bank @@ -288,7 +320,6 @@ def kudosMint : @Class.Method label Classes.Bank Methods.Mint := defMethod Kudos return self.overBalances (fun b => b.addTokens args.denom.originator args.denom args.quantity) ⟫) - (invariant := fun (_self : KudosBank) (args : MintArgs) => checkKey args.denom.originator args.key) def kudosTransfer : @Class.Method label Classes.Bank Methods.Transfer := defMethod KudosBank (body := fun (self : KudosBank) (args : TransferArgs) => ⟪ @@ -297,9 +328,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) => - checkKey args.oldOwner args.key - && 0 < args.quantity + (invariant := fun (self : KudosBank) (args : TransferArgs) signatures => + 0 < args.quantity + && checkSignature (signatures .owner) args.oldOwner && args.quantity <= self.getBalance args.oldOwner args.denom) def kudosBurn : @Class.Method label Classes.Bank Methods.Burn := defMethod KudosBank @@ -308,13 +339,16 @@ 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) => - checkKey args.denom.originator args.key + (invariant := fun (self : KudosBank) (args : BurnArgs) signatures => + checkSignature (signatures .originator) args.denom.originator + && checkSignature (signatures .owner) 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) => self.balances.isEmpty) + (invariant := fun (self : KudosBank) (_args : PUnit) signatures => + checkSignature (signatures .owner) self.owner + && self.balances.isEmpty) def kudosClass : @Class label Classes.Bank where constructors := fun @@ -331,8 +365,6 @@ def checkTransfer : @Class.Method label Classes.Check .Transfer := defMethod Che return {self with owner := args.newOwner : Check} ⟫) - (invariant := fun (self : Check) (args : Check.TransferArgs) => - checkKey self.owner args.key) def checkClass : @Class label Classes.Check where constructors := noConstructors diff --git a/Apps/OwnedCounter.lean b/Apps/OwnedCounter.lean index 767ffa1c..cd52b05b 100644 --- a/Apps/OwnedCounter.lean +++ b/Apps/OwnedCounter.lean @@ -20,6 +20,20 @@ inductive Methods where | Transfer : Methods deriving DecidableEq, Fintype, Repr +namespace Methods + +inductive Transfer.SignatureId : Type where + | owner + +inductive Incr.SignatureId : Type where + | owner + +def SignatureId : Methods → Type + | .Incr => Transfer.SignatureId + | .Transfer => Transfer.SignatureId + +end Methods + inductive Constructors where | Zero : Constructors deriving DecidableEq, Fintype, Repr @@ -28,6 +42,16 @@ inductive Destructors where | Ten : Destructors deriving DecidableEq, Fintype, Repr +namespace Destructors + +inductive Ten.SignatureId : Type where + | owner + +def SignatureId : Destructors → Type + | .Ten => Ten.SignatureId + +end Destructors + open AVM def clab : Class.Label where @@ -37,10 +61,12 @@ 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 @@ -70,14 +96,20 @@ 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) 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) /-- 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) () => self.count >= 10) + (invariant := fun (self : OwnedCounter) () signatures => + checkSignature (signatures .owner) self.owner + && self.count >= 10) def counterClass : @Class label .unit where constructors := fun diff --git a/Apps/TwoCounter.lean b/Apps/TwoCounter.lean index bf125aad..60e5e925 100644 --- a/Apps/TwoCounter.lean +++ b/Apps/TwoCounter.lean @@ -152,8 +152,8 @@ def incrementBoth : @Class.Method Eco.label Eco.Classes.TwoCounter Methods.Incre (body := fun (self : TwoCounter) (n : Nat) => ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) noSignatures + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) noSignatures return self ⟫) diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean index 5b19c462..591e94fc 100644 --- a/Tests/Applib/Surface/Program/Syntax.lean +++ b/Tests/Applib/Surface/Program/Syntax.lean @@ -9,22 +9,22 @@ open Applib example (rx ry : Reference Counter) : Program Eco.label Counter := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * 2 + y.count) - call Counter.Methods.Incr ry (y.count * 2 + x.count) + call Counter.Methods.Incr rx (x.count * 2 + y.count) noSignatures + call Counter.Methods.Incr ry (y.count * 2 + x.count) noSignatures return {x with count := x.count + y.count} ⟫ def mutualIncrement (rx ry : Reference Counter) (n : Nat) : Program Eco.label Unit := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * n + y.count) - call Counter.Methods.Incr ry (y.count * n + x.count) + call Counter.Methods.Incr rx (x.count * n + y.count) noSignatures + call Counter.Methods.Incr ry (y.count * n + x.count) noSignatures return () ⟫ def createCounter : Program Eco.label (Reference Counter) := ⟪ - r := create Counter Counter.Constructors.Zero () - call Counter.Methods.Incr r (7 : Nat) + r := create Counter Counter.Constructors.Zero () noSignatures + call Counter.Methods.Incr r (7 : Nat) noSignatures return r ⟫ @@ -34,9 +34,9 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) + call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures else - call Counter.Methods.Incr self.c2 (2 : Nat) + call Counter.Methods.Incr self.c2 (2 : Nat) noSignatures return self ⟫ @@ -46,10 +46,10 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) - call Counter.Methods.Incr self.c2 (1 : Nat) + call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures + call Counter.Methods.Incr self.c2 (1 : Nat) noSignatures else - call Counter.Methods.Incr self.c2 (2 : Nat) + call Counter.Methods.Incr self.c2 (2 : Nat) noSignatures invoke mutualIncrement self.c2 self.c1 n invoke mutualIncrement self.c1 self.c1 n return self @@ -61,8 +61,8 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) - call Counter.Methods.Incr self.c2 (1 : Nat) + call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures + call Counter.Methods.Incr self.c2 (1 : Nat) noSignatures invoke mutualIncrement self.c1 self.c1 n return self ⟫ @@ -79,19 +79,19 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ ⟫ example : Program Eco.label (Reference TwoCounter) := ⟪ - rx := create Counter Counter.Constructors.Zero () - ry := create Counter Counter.Constructors.Zero () - call Counter.Methods.Incr rx (2 : Nat) - call Counter.Methods.Incr ry (7 : Nat) - tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) + rx := create Counter Counter.Constructors.Zero () noSignatures + ry := create Counter Counter.Constructors.Zero () noSignatures + call Counter.Methods.Incr rx (2 : Nat) noSignatures + call Counter.Methods.Incr ry (7 : Nat) noSignatures + tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) noSignatures return tc ⟫ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) noSignatures + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) noSignatures return self ⟫ @@ -104,7 +104,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ match c1.count with | 0 => return c2 | Nat.succ n' => - call Counter.Methods.Incr cRef (3 : Nat) + call Counter.Methods.Incr cRef (3 : Nat) noSignatures if c1.count > c2.count then c := fetch cRef invoke mutualIncrement self.c2 self.c1 (n' + c.count) @@ -126,9 +126,9 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Unit := ⟪ invoke mutualIncrement self.c2 self.c1 n' else invoke mutualIncrement self.c1 self.c2 n' - call Counter.Methods.Incr self.c2 n' - call Counter.Methods.Incr self.c1 n - call Counter.Methods.Incr self.c2 n + call Counter.Methods.Incr self.c2 n' noSignatures + call Counter.Methods.Incr self.c1 n noSignatures + call Counter.Methods.Incr self.c2 n noSignatures ⟫ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ @@ -217,18 +217,18 @@ open Applib example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program label (Reference OwnedCounter) := ⟪ c := fetch r - call OwnedCounter.Methods.Transfer r newOwner - r' := create OwnedCounter OwnedCounter.Constructors.Zero () - call OwnedCounter.Methods.Incr r' (c.count + 1) - destroy OwnedCounter.Destructors.Ten r () + call OwnedCounter.Methods.Transfer r newOwner noSignatures + r' := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + call OwnedCounter.Methods.Incr r' (c.count + 1) noSignatures + destroy OwnedCounter.Destructors.Ten r () noSignatures return r' ⟫ example (n : Nat) : Program label (Reference OwnedCounter) := ⟪ - r := create OwnedCounter OwnedCounter.Constructors.Zero () - call OwnedCounter.Methods.Incr r n - create OwnedCounter OwnedCounter.Constructors.Zero () - create OwnedCounter OwnedCounter.Constructors.Zero () + r := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + call OwnedCounter.Methods.Incr r n noSignatures + create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures return r ⟫ From 5950e486d82f32eee83d8c80b9da9c6b1ed3d981 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 23 Sep 2025 09:36:11 +0200 Subject: [PATCH 02/17] constructors --- AVM/Class/Label.lean | 3 ++- AVM/Class/Member.lean | 2 +- AVM/Class/Translation/Logics.lean | 32 +++++++++++++++++++------------ Applib/Surface/Member.lean | 2 +- Apps/Kudos.lean | 15 +++++++++++++-- 5 files changed, 37 insertions(+), 17 deletions(-) diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean index 0dc3d019..3c129d81 100644 --- a/AVM/Class/Label.lean +++ b/AVM/Class/Label.lean @@ -34,6 +34,7 @@ structure Label : Type 1 where ConstructorId : Type ConstructorArgs : ConstructorId -> SomeType + ConstructorSignatureId : ConstructorId → Type := fun _ => Empty [constructorsFinite : Fintype ConstructorId] [constructorsRepr : Repr ConstructorId] [constructorsBEq : BEq ConstructorId] @@ -77,7 +78,7 @@ inductive Label.MemberId (lab : Class.Label) : Type where abbrev Label.MemberId.SignatureId {lab : Class.Label} : Label.MemberId lab → Type | .methodId m => lab.MethodSignatureId m | .destructorId m => lab.DestructorSignatureId m - | .constructorId _ => Empty + | .constructorId m => lab.ConstructorSignatureId m | .upgradeId => Empty instance Label.MemberId.hasBEq {lab : Class.Label} : BEq (Class.Label.MemberId lab) where diff --git a/AVM/Class/Member.lean b/AVM/Class/Member.lean index 26ff7cb8..f52d619e 100644 --- a/AVM/Class/Member.lean +++ b/AVM/Class/Member.lean @@ -7,7 +7,7 @@ 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. -/ diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index f2b07ba2..f23874df 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -14,18 +14,26 @@ private def Constructor.Message.logicFun (args : Logic.Args) : Bool := let try msg : Message lab := Message.fromResource args.self - 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 - let! [newObjRes] := createdResObjs - let uid : ObjectId := newObjRes.nonce.value - Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs - && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs - && Logic.checkResourcesEphemeral consumedResObjs - && Logic.checkResourcesPersistent createdResObjs - && constr.invariant argsData + match msg with + | {id := id, contents := contents} => + -- TODO check syntax + if h : id == .classMember (Label.MemberId.constructorId constrId) + then + let contents : MessageContents lab (.classMember (Label.MemberId.constructorId constrId)) := eq_of_beq h ▸ contents + let argsData := contents.args + let try vals : (constr.body argsData).params.Product := tryCast contents.vals + let newObjData := constr.body argsData |>.value vals + let consumedResObjs := Logic.selectObjectResources args.consumed + let createdResObjs := Logic.selectObjectResources args.created + let signatures := contents.signatures + let! [newObjRes] := createdResObjs + let uid : ObjectId := newObjRes.nonce.value + Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs + && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs + && Logic.checkResourcesEphemeral consumedResObjs + && Logic.checkResourcesPersistent createdResObjs + && constr.invariant argsData signatures + else false /-- Creates a message logic function for a given destructor. -/ private def Destructor.Message.logicFun diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean index 6410686c..b170b1d1 100644 --- a/Applib/Surface/Member.lean +++ b/Applib/Surface/Member.lean @@ -29,7 +29,7 @@ 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 cl) - (invariant : constrId.Args.type → Bool := fun _ => true) + (invariant : (args : constrId.Args.type) → (signatures : constrId.Signatures args) → Bool := fun _ _ => true) : Class.Constructor i.classId constrId where invariant (args : constrId.Args.type) := invariant args body (args : constrId.Args.type) := body args |>.map i.toObject |>.toAVM diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean index 2b537f84..692e08bb 100644 --- a/Apps/Kudos.lean +++ b/Apps/Kudos.lean @@ -44,6 +44,17 @@ inductive Constructors where | Mint : Constructors deriving DecidableEq, Fintype, Repr +namespace Constructors + +inductive Mint.SignatureId where + | originator + +def SignatureId (m : Constructors) : Type := + match m with + | .Mint => Mint.SignatureId + +end Constructors + inductive Destructors where | Burn : Destructors deriving DecidableEq, Fintype, Repr @@ -71,7 +82,6 @@ instance hasTypeRep : TypeRep Kudos where rep := Rep.atomic "Kudos" structure MintArgs where - key : PrivateKey originator : PublicKey quantity : Nat deriving BEq @@ -98,6 +108,7 @@ def clab : Class.Label where ConstructorId := Constructors ConstructorArgs := fun | Constructors.Mint => ⟨MintArgs⟩ + ConstructorSignatureId := Constructors.SignatureId DestructorId := Destructors DestructorArgs := fun @@ -129,7 +140,7 @@ def kudosMint : @Class.Constructor label .unit Constructors.Mint := defConstruct owner := args.originator originator := args.originator : Kudos} ⟫) - (invariant := fun (args : MintArgs) => checkKey args.originator args.key) + (invariant := fun (args : MintArgs) signatures => checkSignature (signatures .originator) args.originator) def kudosTransfer : @Class.Method label .unit Methods.Transfer := defMethod Kudos (body := fun (self : Kudos) (args : TransferArgs) => From fae01c41ae9232b2a6eb2d3dce81e387dca9f971 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Tue, 23 Sep 2025 09:58:21 +0200 Subject: [PATCH 03/17] multi methods --- AVM/Class/Translation/Logics.lean | 84 +++++++++++++++-------------- AVM/Class/Translation/Messages.lean | 3 +- AVM/Class/Translation/Tasks.lean | 7 +-- AVM/Ecosystem/Label/Base.lean | 9 ++-- AVM/Ecosystem/Member.lean | 2 +- AVM/Program.lean | 11 ++-- Applib/Surface/Program.lean | 12 +++-- Applib/Surface/Program/Syntax.lean | 8 +-- Apps/UniversalCounter.lean | 4 +- 9 files changed, 77 insertions(+), 63 deletions(-) diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index f23874df..2d04d99d 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -179,46 +179,52 @@ 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.contents.args - let consumedResObjs := Logic.selectObjectResources args.consumed - let createdResObjs := Logic.selectObjectResources args.created - let try (argsConsumedSelves, argsConstructedEph, argsDestroyed, .unit) := - consumedResObjs - |> Logic.filterOutDummy - |>.splitsExact [multiId.numObjectArgs, data.numConstructed, data.numDestroyed] - 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.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⟩ - let reassembled : List ObjectValue := res.assembled.withOldUidList.map (fun x => mkObjectValue x.arg x.objectData) - let destroyedObjects : List ObjectValue := res.destroyed.map (fun x => x.toSomeObject.toObjectValue) - 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, argsDestroyedEph, argsSelvesDestroyedEph, .unit) := - createdResObjs + match msg with + | {id := id, contents := contents} => + if h : id == .multiMethodId multiId + then + let contents : MessageContents lab (.multiMethodId multiId) := eq_of_beq h ▸ contents + let fargs : multiId.Args.type := contents.args + let consumedResObjs := Logic.selectObjectResources args.consumed + let createdResObjs := Logic.selectObjectResources args.created + let try (argsConsumedSelves, argsConstructedEph, argsDestroyed, .unit) := + consumedResObjs |> Logic.filterOutDummy - |>.splitsExact [reassembled.length, data.numConstructed, data.numDestroyed, data.numSelvesDestroyed] - Logic.checkResourceValues reassembled argsCreated.toList - && Logic.checkResourceValues destroyedObjects argsDestroyed.toList - && Logic.checkResourceValues destroyedObjects argsDestroyedEph.toList - && Logic.checkResourceValues constructedObjects argsConstructed.toList - && Logic.checkResourceValues constructedObjects argsConstructedEph.toList - && Logic.checkResourceValues consumedDestroyedObjects argsSelvesDestroyedEph.toList - && Logic.checkResourcesPersistent argsConsumedSelves.toList - && Logic.checkResourcesPersistent argsDestroyed.toList - && Logic.checkResourcesPersistent argsCreated.toList - && Logic.checkResourcesPersistent argsConstructed.toList - && Logic.checkResourcesEphemeral argsConstructedEph.toList - && Logic.checkResourcesEphemeral argsDestroyedEph.toList - && Logic.checkResourcesEphemeral argsSelvesDestroyedEph.toList + |>.splitsExact [multiId.numObjectArgs, data.numConstructed, data.numDestroyed] + let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves.toList + let prog := method.body argsConsumedObjects fargs + method.invariant argsConsumedObjects fargs contents.signatures + && 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⟩ + let reassembled : List ObjectValue := res.assembled.withOldUidList.map (fun x => mkObjectValue x.arg x.objectData) + let destroyedObjects : List ObjectValue := res.destroyed.map (fun x => x.toSomeObject.toObjectValue) + 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, argsDestroyedEph, argsSelvesDestroyedEph, .unit) := + createdResObjs + |> Logic.filterOutDummy + |>.splitsExact [reassembled.length, data.numConstructed, data.numDestroyed, data.numSelvesDestroyed] + Logic.checkResourceValues reassembled argsCreated.toList + && Logic.checkResourceValues destroyedObjects argsDestroyed.toList + && Logic.checkResourceValues destroyedObjects argsDestroyedEph.toList + && Logic.checkResourceValues constructedObjects argsConstructed.toList + && Logic.checkResourceValues constructedObjects argsConstructedEph.toList + && Logic.checkResourceValues consumedDestroyedObjects argsSelvesDestroyedEph.toList + && Logic.checkResourcesPersistent argsConsumedSelves.toList + && Logic.checkResourcesPersistent argsDestroyed.toList + && Logic.checkResourcesPersistent argsCreated.toList + && Logic.checkResourcesPersistent argsConstructed.toList + && Logic.checkResourcesEphemeral argsConstructedEph.toList + && Logic.checkResourcesEphemeral argsDestroyedEph.toList + && Logic.checkResourcesEphemeral argsSelvesDestroyedEph.toList + else false def MultiMethod.Message.logic {lab : Ecosystem.Label} diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean index fe1c9f49..e15d6cf2 100644 --- a/AVM/Class/Translation/Messages.lean +++ b/AVM/Class/Translation/Messages.lean @@ -90,6 +90,7 @@ def MultiMethod.message (method : MultiMethod multiId) (selves : multiId.Selves) (args : multiId.Args.type) + (signatures : multiId.Signatures args) (vals : (method.body selves args).params.Product) : Message lab := let res : MultiMethodResult multiId := method.body selves args |>.value vals @@ -101,5 +102,5 @@ def MultiMethod.message Vals := ⟨(method.body selves args).params.Product⟩ vals args - signatures := .unit + signatures recipients := Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) }} diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean index 33036372..8ffb697c 100644 --- a/AVM/Class/Translation/Tasks.lean +++ b/AVM/Class/Translation/Tasks.lean @@ -81,9 +81,9 @@ private partial def Body.tasks' let task := method.task' adjust eco r (adjust self) args signatures Tasks.task task.task fun vals => Body.tasks' (task.adjust vals) eco next cont - | .multiMethod multiId selvesIds args next => + | .multiMethod multiId selvesIds args signatures next => Tasks.fetchSelves selvesIds fun selves => - let task := multiId.task' adjust eco (fun x => adjust (selves x)) args + let task := multiId.task' adjust eco (fun x => adjust (selves x)) args signatures Tasks.task task.task fun vals => Body.tasks' (task.adjust vals) eco next cont | .upgrade classId selfId objData next => @@ -245,6 +245,7 @@ partial def Ecosystem.Label.MultiMethodId.task' {multiId : lab.MultiMethodId} (selves : multiId.Selves) (args : multiId.Args.type) + (signatures : multiId.Signatures args) : Task' := let method := eco.multiMethods multiId let body := method.body selves args @@ -306,7 +307,7 @@ partial def Ecosystem.Label.MultiMethodId.task' ensureUnique := rands.reassembledNewUidNonces.toList } let mkMessage (vals : body.params.Product) : SomeMessage := - ⟨(eco.multiMethods multiId).message selves args vals⟩ + ⟨(eco.multiMethods multiId).message selves args signatures vals⟩ Body.task' adjust eco body mkResult mkActionData mkMessage diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean index 511c77b3..2838edd9 100644 --- a/AVM/Ecosystem/Label/Base.lean +++ b/AVM/Ecosystem/Label/Base.lean @@ -20,6 +20,7 @@ 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 [ObjectArgNamesEnum (f : MultiMethodId) : FinEnum (MultiMethodObjectArgNames f)] [ObjectArgNamesBEq (f : MultiMethodId) : BEq (MultiMethodObjectArgNames f)] [multiMethodsFinite : FinEnum MultiMethodId] @@ -99,8 +100,10 @@ namespace MultiMethodId def Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType := lab.MultiMethodArgs multiId -def Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) (_args : multiId.Args.type) : Type := - Unit +def SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId + +def 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 @@ -175,7 +178,7 @@ instance instLawfulBEq {lab : Ecosystem.Label} : LawfulBEq lab.MemberId where abbrev SignatureId (lab : Ecosystem.Label) : MemberId lab → Type | .classMember m => m.SignatureId - | _ => Empty + | .multiMethodId m => m.SignatureId abbrev Args {lab : Ecosystem.Label} (memberId : MemberId lab) : SomeType.{0} := match memberId with diff --git a/AVM/Ecosystem/Member.lean b/AVM/Ecosystem/Member.lean index d77e91a9..d22d328c 100644 --- a/AVM/Ecosystem/Member.lean +++ b/AVM/Ecosystem/Member.lean @@ -101,4 +101,4 @@ structure Ecosystem.MultiMethod {lab : Ecosystem.Label} (multiId : lab.MultiMeth /-- Computes the result of a multiMethod call. See `MultiMethodResult`. -/ body (selves : multiId.Selves) (args : multiId.Args.type) : Program.{1} lab (MultiMethodResult multiId) /-- Extra multiMethod logic. -/ - invariant (selves : multiId.Selves) (args : multiId.Args.type) : Bool + invariant (selves : multiId.Selves) (args : multiId.Args.type) (signatures : multiId.Signatures args) : Bool diff --git a/AVM/Program.lean b/AVM/Program.lean index 6ea4c782..e9c59085 100644 --- a/AVM/Program.lean +++ b/AVM/Program.lean @@ -38,6 +38,7 @@ inductive Program.{u} (lab : Ecosystem.Label) (ReturnType : Type u) : Type (max (mid : lab.MultiMethodId) (selvesIds : mid.SelvesIds) (args : mid.Args.type) + (signatures : mid.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | /-- Object upgrade -/ @@ -70,7 +71,7 @@ def lift.{v, u} | .constructor cid constr args signatures next => .constructor cid constr args signatures (fun a => (next a).lift) | .destructor cid destrId selfId args signatures next => .destructor cid destrId selfId args signatures next.lift | .method cid methodId selfId args signatures next => .method cid methodId selfId args signatures next.lift - | .multiMethod mid selvesIds args next => .multiMethod mid selvesIds args next.lift + | .multiMethod mid selvesIds args signatures next => .multiMethod mid selvesIds args signatures next.lift | .upgrade cid selfId obj next => .upgrade cid selfId obj next.lift | .fetch objId next => .fetch objId (fun a => (next a).lift) | .return val => .return (ULift.up val) @@ -89,8 +90,8 @@ def invoke .destructor cid destrId selfId args signatures (Program.invoke cont next) | .method cid methodId selfId args signatures cont => .method cid methodId selfId args signatures (Program.invoke cont next) - | .multiMethod mid selvesId args cont => - .multiMethod mid selvesId args (Program.invoke cont next) + | .multiMethod mid selvesId args signatures cont => + .multiMethod mid selvesId args signatures (Program.invoke cont next) | .upgrade cid selfId obj cont => .upgrade cid selfId obj (Program.invoke cont next) | .fetch objId cont => @@ -108,7 +109,7 @@ def params {lab : Ecosystem.Label} {α : Type u} (prog : Program lab α) : Param | .constructor _ _ _ _ next => .genId (fun newId => next newId |>.params) | .destructor _ _ _ _ _ next => next.params | .method _ _ _ _ _ next => next.params - | .multiMethod _ _ _ next => next.params + | .multiMethod _ _ _ _ next => next.params | .upgrade _ _ _ next => next.params | .fetch objId next => .fetch objId (fun obj => next obj |>.params) | .return _ => .empty @@ -124,7 +125,7 @@ def value {lab : Ecosystem.Label} {α : Type u} (prog : Program lab α) (vals : next.value vals | .method _ _ _ _ _ next => next.value vals - | .multiMethod _ _ _ next => + | .multiMethod _ _ _ _ next => next.value vals | .upgrade _ _ _ next => next.value vals diff --git a/Applib/Surface/Program.lean b/Applib/Surface/Program.lean index 953fe6a4..b474f421 100644 --- a/Applib/Surface/Program.lean +++ b/Applib/Surface/Program.lean @@ -39,6 +39,7 @@ inductive Program (lab : Ecosystem.Label) : (ReturnType : Type u) → Type (u + (multiId : lab.MultiMethodId) (selves : multiId.SelvesIds) (args : multiId.Args.type) + (signatures : multiId.Signatures args) (next : Program lab ReturnType) : Program lab ReturnType | upgrade @@ -74,8 +75,8 @@ def Program.toAVM {lab ReturnType} (prog : Program lab ReturnType) : AVM.Program .destructor cid destrId selfId args signatures (toAVM next) | .call cid methodId selfId args signatures next => .method cid methodId selfId args signatures (toAVM next) - | .multiCall multiId selves args next => - .multiMethod multiId selves args (toAVM next) + | .multiCall multiId selves args signatures next => + .multiMethod multiId selves args signatures (toAVM next) | .upgrade classId selfId obj next => .upgrade classId selfId obj (toAVM next) | @fetch _ _ _ i objId next => @@ -93,8 +94,8 @@ def Program.map {lab : Ecosystem.Label} {A B : Type} (f : A → B) (prog : Progr .destroy cid destrId selfId args signatures (map f next) | .call cid methodId selfId args signatures next => .call cid methodId selfId args signatures (map f next) - | .multiCall multiId selvesIds args next => - .multiCall multiId selvesIds args (map f next) + | .multiCall multiId selvesIds args signatures next => + .multiCall multiId selvesIds args signatures (map f next) | .upgrade classId selfId obj next => .upgrade classId selfId obj (map f next) | @fetch _ _ C _ objId next => @@ -156,10 +157,11 @@ def Program.multiCall' (multiId : lab.MultiMethodId) (selves : multiId.SelvesReferences) (args : multiId.Args.type) + (signatures : multiId.Signatures args) (next : Program lab α) : Program lab α := let selves' : multiId.SelvesIds := fun x => selves x |>.ref.objId - multiCall multiId selves' args next + multiCall multiId selves' args signatures next def Program.fetch' {ReturnType} {lab : Ecosystem.Label} {C : Type} (r : Reference C) [i : IsObject C] (next : C → Program lab ReturnType) : Program lab ReturnType := Program.fetch C r.objId next diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index ba4839dc..9ce275f4 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -70,10 +70,10 @@ macro_rules `(Program.call' $e $m $args $signatures (Program.return ())) | `(⟪call $m:ident $e:term $args:term $signatures:term; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) - | `(⟪multiCall $m:ident $selves:term $args:term⟫) => - `(Program.multiCall' $m $selves $args (Program.return ())) - | `(⟪multiCall $m:ident $selves:term $args:term ; $p:program⟫) => - `(Program.multiCall' $m $selves $args (⟪$p⟫)) + | `(⟪multiCall $m:ident $selves:term $args:term $signatures:term⟫) => + `(Program.multiCall' $m $selves $args $signatures (Program.return ())) + | `(⟪multiCall $m:ident $selves:term $args:term $signatures; $p:program⟫) => + `(Program.multiCall' $m $selves $args $signatures (⟪$p⟫)) | `(⟪upgrade $e:term to $e':term⟫) => `(Program.upgrade' $e $e' Program.return) | `(⟪upgrade $e:term to $e':term ; $p:program⟫) => diff --git a/Apps/UniversalCounter.lean b/Apps/UniversalCounter.lean index 26692cab..a23ef1b6 100644 --- a/Apps/UniversalCounter.lean +++ b/Apps/UniversalCounter.lean @@ -110,7 +110,7 @@ def counterClass : @Class label .unit where destructors := noDestructors def mergeMethod : @Ecosystem.MultiMethod label .Merge where - invariant _ _ := true + invariant _ _ _ := true body selves (_args : Unit) := let prog : _ := ⟪ let c1 : Counter := selves .Counter1 |>.data |> fromObject @@ -147,5 +147,5 @@ example (rx ry : Reference Counter) : Applib.Program label Unit := ⟪ unfold label infer_instance ref := ry } - multiCall Counter.MultiMethods.Merge selves .unit + multiCall Counter.MultiMethods.Merge selves .unit noSignatures ⟫ From fcf71cfbab617f23ce3c183885606cc884cb65d3 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 09:28:03 +0200 Subject: [PATCH 04/17] add signed keyword --- Applib/Surface/Program/Syntax.lean | 11 +++--- Apps/TwoCounter.lean | 4 +-- Tests/Applib/Surface/Program/Syntax.lean | 46 ++++++++++++------------ 3 files changed, 32 insertions(+), 29 deletions(-) diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index 9ce275f4..8f464f46 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -1,4 +1,5 @@ import Applib.Surface.Program +import Applib.Surface.Member namespace Applib @@ -24,7 +25,7 @@ syntax colGe withPosition(ident " := " " create " ident ident term) optSemicolon syntax colGe "destroy " ident term : program syntax colGe withPosition("destroy " ident term) optSemicolon(program) : program syntax colGe "call " ident term : program -syntax colGe withPosition("call " ident term) optSemicolon(program) : program +syntax colGe withPosition("call " ident term (" signed " term)?) optSemicolon(program) : program syntax colGe "multiCall " ident term : program syntax colGe withPosition("multiCall " ident term) optSemicolon(program) : program syntax colGe "upgrade " term " to " term : program @@ -66,9 +67,11 @@ macro_rules `(Program.destroy' $e $m $args $signatures (Program.return ())) | `(⟪destroy $m:ident $e:term $args:term $signatures:term; $p:program⟫) => `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) - | `(⟪call $m:ident $e:term $args:term $signatures:term⟫) => - `(Program.call' $e $m $args $signatures (Program.return ())) - | `(⟪call $m:ident $e:term $args:term $signatures:term; $p:program⟫) => + | `(⟪call $m:ident $e:term $args:term⟫) => + `(Program.call' $e $m $args noSignatures (Program.return ())) + | `(⟪call $m:ident $e:term $args:term ; $p:program⟫) => + `(Program.call' $e $m $args noSignatures (⟪$p⟫)) + | `(⟪call $m:ident $e:term $args:term signed $signatures; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term $signatures:term⟫) => `(Program.multiCall' $m $selves $args $signatures (Program.return ())) diff --git a/Apps/TwoCounter.lean b/Apps/TwoCounter.lean index 60e5e925..f80330be 100644 --- a/Apps/TwoCounter.lean +++ b/Apps/TwoCounter.lean @@ -152,8 +152,8 @@ def incrementBoth : @Class.Method Eco.label Eco.Classes.TwoCounter Methods.Incre (body := fun (self : TwoCounter) (n : Nat) => ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) noSignatures - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) noSignatures + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count); + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) signed noSignatures return self ⟫) diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean index 591e94fc..b5536c03 100644 --- a/Tests/Applib/Surface/Program/Syntax.lean +++ b/Tests/Applib/Surface/Program/Syntax.lean @@ -9,22 +9,22 @@ open Applib example (rx ry : Reference Counter) : Program Eco.label Counter := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * 2 + y.count) noSignatures - call Counter.Methods.Incr ry (y.count * 2 + x.count) noSignatures + call Counter.Methods.Incr rx (x.count * 2 + y.count); + call Counter.Methods.Incr ry (y.count * 2 + x.count); return {x with count := x.count + y.count} ⟫ def mutualIncrement (rx ry : Reference Counter) (n : Nat) : Program Eco.label Unit := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * n + y.count) noSignatures - call Counter.Methods.Incr ry (y.count * n + x.count) noSignatures + call Counter.Methods.Incr rx (x.count * n + y.count); + call Counter.Methods.Incr ry (y.count * n + x.count); return () ⟫ def createCounter : Program Eco.label (Reference Counter) := ⟪ r := create Counter Counter.Constructors.Zero () noSignatures - call Counter.Methods.Incr r (7 : Nat) noSignatures + call Counter.Methods.Incr r (7 : Nat); return r ⟫ @@ -34,9 +34,9 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures + call Counter.Methods.Incr self.c1 (2 : Nat) else - call Counter.Methods.Incr self.c2 (2 : Nat) noSignatures + call Counter.Methods.Incr self.c2 (2 : Nat) return self ⟫ @@ -46,10 +46,10 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures - call Counter.Methods.Incr self.c2 (1 : Nat) noSignatures + call Counter.Methods.Incr self.c1 (2 : Nat); + call Counter.Methods.Incr self.c2 (1 : Nat) else - call Counter.Methods.Incr self.c2 (2 : Nat) noSignatures + call Counter.Methods.Incr self.c2 (2 : Nat) invoke mutualIncrement self.c2 self.c1 n invoke mutualIncrement self.c1 self.c1 n return self @@ -61,8 +61,8 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat) noSignatures - call Counter.Methods.Incr self.c2 (1 : Nat) noSignatures + call Counter.Methods.Incr self.c1 (2 : Nat); + call Counter.Methods.Incr self.c2 (1 : Nat) invoke mutualIncrement self.c1 self.c1 n return self ⟫ @@ -81,8 +81,8 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ example : Program Eco.label (Reference TwoCounter) := ⟪ rx := create Counter Counter.Constructors.Zero () noSignatures ry := create Counter Counter.Constructors.Zero () noSignatures - call Counter.Methods.Incr rx (2 : Nat) noSignatures - call Counter.Methods.Incr ry (7 : Nat) noSignatures + call Counter.Methods.Incr rx (2 : Nat); + call Counter.Methods.Incr ry (7 : Nat); tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) noSignatures return tc ⟫ @@ -90,8 +90,8 @@ example : Program Eco.label (Reference TwoCounter) := ⟪ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) noSignatures - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) noSignatures + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count); + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count); return self ⟫ @@ -104,7 +104,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ match c1.count with | 0 => return c2 | Nat.succ n' => - call Counter.Methods.Incr cRef (3 : Nat) noSignatures + call Counter.Methods.Incr cRef (3 : Nat); if c1.count > c2.count then c := fetch cRef invoke mutualIncrement self.c2 self.c1 (n' + c.count) @@ -126,9 +126,9 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Unit := ⟪ invoke mutualIncrement self.c2 self.c1 n' else invoke mutualIncrement self.c1 self.c2 n' - call Counter.Methods.Incr self.c2 n' noSignatures - call Counter.Methods.Incr self.c1 n noSignatures - call Counter.Methods.Incr self.c2 n noSignatures + call Counter.Methods.Incr self.c2 n' + call Counter.Methods.Incr self.c1 n; + call Counter.Methods.Incr self.c2 n ⟫ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ @@ -217,16 +217,16 @@ open Applib example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program label (Reference OwnedCounter) := ⟪ c := fetch r - call OwnedCounter.Methods.Transfer r newOwner noSignatures + call OwnedCounter.Methods.Transfer r newOwner; r' := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures - call OwnedCounter.Methods.Incr r' (c.count + 1) noSignatures + call OwnedCounter.Methods.Incr r' (c.count + 1); destroy OwnedCounter.Destructors.Ten r () noSignatures return r' ⟫ example (n : Nat) : Program label (Reference OwnedCounter) := ⟪ r := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures - call OwnedCounter.Methods.Incr r n noSignatures + call OwnedCounter.Methods.Incr r n; create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures return r From 9bbc0804d4887207a8f82efd3f81846c8cf9e6a3 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Sep 2025 10:40:19 +0200 Subject: [PATCH 05/17] signed syntax --- Applib/Surface/Program/Syntax.lean | 8 +++++--- Apps/TwoCounter.lean | 4 ++-- Tests/Applib/Surface/Program/Syntax.lean | 20 ++++++++++---------- 3 files changed, 17 insertions(+), 15 deletions(-) diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index 8f464f46..592dc3ce 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -24,8 +24,8 @@ syntax colGe withPosition("create " ident ident term) optSemicolon(program) : pr syntax colGe withPosition(ident " := " " create " ident ident term) optSemicolon(program) : program syntax colGe "destroy " ident term : program syntax colGe withPosition("destroy " ident term) optSemicolon(program) : program -syntax colGe "call " ident term : program -syntax colGe withPosition("call " ident term (" signed " term)?) optSemicolon(program) : program +syntax colGe "call " ("signed " "(" term ")")? ident term : program +syntax colGe withPosition("call " ("signed " "(" term ")")? ident term) optSemicolon(program) : program syntax colGe "multiCall " ident term : program syntax colGe withPosition("multiCall " ident term) optSemicolon(program) : program syntax colGe "upgrade " term " to " term : program @@ -69,9 +69,11 @@ macro_rules `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term⟫) => `(Program.call' $e $m $args noSignatures (Program.return ())) + | `(⟪call signed ($signatures) $m:ident $e:term $args:term⟫) => + `(Program.call' $e $m $args $signatures (Program.return ())) | `(⟪call $m:ident $e:term $args:term ; $p:program⟫) => `(Program.call' $e $m $args noSignatures (⟪$p⟫)) - | `(⟪call $m:ident $e:term $args:term signed $signatures; $p:program⟫) => + | `(⟪call signed ($signatures) $m:ident $e:term $args:term ; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term $signatures:term⟫) => `(Program.multiCall' $m $selves $args $signatures (Program.return ())) diff --git a/Apps/TwoCounter.lean b/Apps/TwoCounter.lean index f80330be..60596862 100644 --- a/Apps/TwoCounter.lean +++ b/Apps/TwoCounter.lean @@ -152,8 +152,8 @@ def incrementBoth : @Class.Method Eco.label Eco.Classes.TwoCounter Methods.Incre (body := fun (self : TwoCounter) (n : Nat) => ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count); - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) signed noSignatures + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) + call signed (noSignatures) Counter.Methods.Incr self.c2 (c1.count * n + c2.count) return self ⟫) diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean index b5536c03..20be42be 100644 --- a/Tests/Applib/Surface/Program/Syntax.lean +++ b/Tests/Applib/Surface/Program/Syntax.lean @@ -9,16 +9,16 @@ open Applib example (rx ry : Reference Counter) : Program Eco.label Counter := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * 2 + y.count); - call Counter.Methods.Incr ry (y.count * 2 + x.count); + call Counter.Methods.Incr rx (x.count * 2 + y.count) + call Counter.Methods.Incr ry (y.count * 2 + x.count) return {x with count := x.count + y.count} ⟫ def mutualIncrement (rx ry : Reference Counter) (n : Nat) : Program Eco.label Unit := ⟪ x := fetch rx y := fetch ry - call Counter.Methods.Incr rx (x.count * n + y.count); - call Counter.Methods.Incr ry (y.count * n + x.count); + call Counter.Methods.Incr rx (x.count * n + y.count) + call Counter.Methods.Incr ry (y.count * n + x.count) return () ⟫ @@ -46,7 +46,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat); + call Counter.Methods.Incr self.c1 (2 : Nat) call Counter.Methods.Incr self.c2 (1 : Nat) else call Counter.Methods.Incr self.c2 (2 : Nat) @@ -61,7 +61,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 if c1.count > c2.count then - call Counter.Methods.Incr self.c1 (2 : Nat); + call Counter.Methods.Incr self.c1 (2 : Nat) call Counter.Methods.Incr self.c2 (1 : Nat) invoke mutualIncrement self.c1 self.c1 n return self @@ -81,8 +81,8 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ example : Program Eco.label (Reference TwoCounter) := ⟪ rx := create Counter Counter.Constructors.Zero () noSignatures ry := create Counter Counter.Constructors.Zero () noSignatures - call Counter.Methods.Incr rx (2 : Nat); - call Counter.Methods.Incr ry (7 : Nat); + call Counter.Methods.Incr rx (2 : Nat) + call Counter.Methods.Incr ry (7 : Nat) tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) noSignatures return tc ⟫ @@ -90,8 +90,8 @@ example : Program Eco.label (Reference TwoCounter) := ⟪ example (self : TwoCounter) (n : Nat) : Program Eco.label TwoCounter := ⟪ c1 := fetch self.c1 c2 := fetch self.c2 - call Counter.Methods.Incr self.c1 (c2.count * n + c1.count); - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count); + call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) return self ⟫ From 13c70d40567927fe119659acd949a8ce57669047 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Sep 2025 10:56:15 +0200 Subject: [PATCH 06/17] signed syntax --- Applib/Surface/Program/Syntax.lean | 10 ++++++---- Apps/TwoCounter.lean | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index 592dc3ce..28193d50 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -24,8 +24,10 @@ syntax colGe withPosition("create " ident ident term) optSemicolon(program) : pr syntax colGe withPosition(ident " := " " create " ident ident term) optSemicolon(program) : program syntax colGe "destroy " ident term : program syntax colGe withPosition("destroy " ident term) optSemicolon(program) : program -syntax colGe "call " ("signed " "(" term ")")? ident term : program -syntax colGe withPosition("call " ("signed " "(" term ")")? ident term) optSemicolon(program) : program +syntax colGe "call " ident term : program +syntax colGe "call " ident term " signed " term : program +syntax colGe withPosition("call " ident term) optSemicolon(program) : program +syntax colGe withPosition("call " ident term " signed " term optSemicolon(program)) : program syntax colGe "multiCall " ident term : program syntax colGe withPosition("multiCall " ident term) optSemicolon(program) : program syntax colGe "upgrade " term " to " term : program @@ -69,11 +71,11 @@ macro_rules `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term⟫) => `(Program.call' $e $m $args noSignatures (Program.return ())) - | `(⟪call signed ($signatures) $m:ident $e:term $args:term⟫) => + | `(⟪call $m:ident $e:term $args:term signed $signatures⟫) => `(Program.call' $e $m $args $signatures (Program.return ())) | `(⟪call $m:ident $e:term $args:term ; $p:program⟫) => `(Program.call' $e $m $args noSignatures (⟪$p⟫)) - | `(⟪call signed ($signatures) $m:ident $e:term $args:term ; $p:program⟫) => + | `(⟪call $m:ident $e:term $args:term signed $signatures ; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term $signatures:term⟫) => `(Program.multiCall' $m $selves $args $signatures (Program.return ())) diff --git a/Apps/TwoCounter.lean b/Apps/TwoCounter.lean index 60596862..be2914d1 100644 --- a/Apps/TwoCounter.lean +++ b/Apps/TwoCounter.lean @@ -153,7 +153,7 @@ def incrementBoth : @Class.Method Eco.label Eco.Classes.TwoCounter Methods.Incre c1 := fetch self.c1 c2 := fetch self.c2 call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) - call signed (noSignatures) Counter.Methods.Incr self.c2 (c1.count * n + c2.count) + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) signed noSignatures return self ⟫) From 7c1823da7e5acbcb16abc3e53dc17c9c57b93d4d Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 11:39:59 +0200 Subject: [PATCH 07/17] add signed variation for the rest of statements --- Applib/Surface/Program/Syntax.lean | 39 ++++++++++++++++++------ Apps/TwoCounter.lean | 2 +- Apps/UniversalCounter.lean | 2 +- Tests/Applib/Surface/Program/Syntax.lean | 18 +++++------ 4 files changed, 41 insertions(+), 20 deletions(-) diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index 28193d50..bfcb6215 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -20,16 +20,23 @@ syntax colGe withPosition("if " term " then " colGt withPosition(program)) colGe syntax colGe withPosition("if " term " then " colGt withPosition(program)) : program syntax colGe withPosition("if " term " then " colGt withPosition(program)) optSemicolon(program) : program syntax colGe "create " ident ident term : program +syntax colGe "create " ident ident term " signed " term : program syntax colGe withPosition("create " ident ident term) optSemicolon(program) : program +syntax colGe withPosition("create " ident ident term " signed " term) optSemicolon(program) : program syntax colGe withPosition(ident " := " " create " ident ident term) optSemicolon(program) : program +syntax colGe withPosition(ident " := " " create " ident ident term " signed " term) optSemicolon(program) : program syntax colGe "destroy " ident term : program +syntax colGe "destroy " ident term " signed " term : program syntax colGe withPosition("destroy " ident term) optSemicolon(program) : program +syntax colGe withPosition("destroy " ident term " signed " term) optSemicolon(program) : program syntax colGe "call " ident term : program syntax colGe "call " ident term " signed " term : program syntax colGe withPosition("call " ident term) optSemicolon(program) : program -syntax colGe withPosition("call " ident term " signed " term optSemicolon(program)) : program +syntax colGe withPosition("call " ident term " signed " term) optSemicolon(program) : program syntax colGe "multiCall " ident term : program +syntax colGe "multiCall " ident term " signed " term : program syntax colGe withPosition("multiCall " ident term) optSemicolon(program) : program +syntax colGe withPosition("multiCall " ident term " signed " term) optSemicolon(program) : program syntax colGe "upgrade " term " to " term : program syntax colGe withPosition("upgrade " term " to " term) optSemicolon(program) : program syntax colGe "invoke " term : program @@ -59,15 +66,25 @@ macro_rules `(if $cond then ⟪$thenProg⟫ else Program.return ()) | `(⟪if $cond:term then $thenProg:program ; $p:program⟫) => `(let next := fun () => ⟪$p⟫; if $cond then Program.invoke ⟪$thenProg⟫ next else next ()) - | `(⟪create $c:ident $m:ident $e:term $signatures:term⟫) => + | `(⟪create $c:ident $m:ident $e:term ⟫) => + `(Program.create' $c $m $e noSignatures Program.return) + | `(⟪create $c:ident $m:ident $e:term signed $signatures:term⟫) => `(Program.create' $c $m $e $signatures Program.return) - | `(⟪create $c:ident $m:ident $e:term $signatures:term; $p:program⟫) => + | `(⟪create $c:ident $m:ident $e:term; $p:program⟫) => + `(Program.create' $c $m $e noSignatures (fun _ => ⟪$p⟫)) + | `(⟪create $c:ident $m:ident $e:term signed $signatures:term; $p:program⟫) => `(Program.create' $c $m $e $signatures (fun _ => ⟪$p⟫)) - | `(⟪$x:ident := create $c:ident $m:ident $e:term $signatures:term; $p:program⟫) => + | `(⟪$x:ident := create $c:ident $m:ident $e:term; $p:program⟫) => + `(Program.create' $c $m $e noSignatures (fun $x => ⟪$p⟫)) + | `(⟪$x:ident := create $c:ident $m:ident $e:term signed $signatures:term; $p:program⟫) => `(Program.create' $c $m $e $signatures (fun $x => ⟪$p⟫)) - | `(⟪destroy $m:ident $e:term $args:term $signatures:term⟫) => + | `(⟪destroy $m:ident $e:term $args:term⟫) => + `(Program.destroy' $e $m $args noSignatures (Program.return ())) + | `(⟪destroy $m:ident $e:term $args:term signed $signatures:term⟫) => `(Program.destroy' $e $m $args $signatures (Program.return ())) - | `(⟪destroy $m:ident $e:term $args:term $signatures:term; $p:program⟫) => + | `(⟪destroy $m:ident $e:term $args:term; $p:program⟫) => + `(Program.destroy' $e $m $args noSignatures (⟪$p⟫)) + | `(⟪destroy $m:ident $e:term $args:term signed $signatures:term; $p:program⟫) => `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term⟫) => `(Program.call' $e $m $args noSignatures (Program.return ())) @@ -77,10 +94,14 @@ macro_rules `(Program.call' $e $m $args noSignatures (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term signed $signatures ; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) - | `(⟪multiCall $m:ident $selves:term $args:term $signatures:term⟫) => + | `(⟪multiCall $m:ident $selves:term $args:term⟫) => + `(Program.multiCall' $m $selves $args noSignatures (Program.return ())) + | `(⟪multiCall $m:ident $selves:term $args:term signed $signatures:term; $p:program⟫) => + `(Program.multiCall' $m $selves $args $signatures $signatures (⟪$p⟫)) + | `(⟪multiCall $m:ident $selves:term $args:term; $p:program⟫) => + `(Program.multiCall' $m $selves $args noSignatures (⟪$p⟫)) + | `(⟪multiCall $m:ident $selves:term $args:term signed $signatures:term⟫) => `(Program.multiCall' $m $selves $args $signatures (Program.return ())) - | `(⟪multiCall $m:ident $selves:term $args:term $signatures; $p:program⟫) => - `(Program.multiCall' $m $selves $args $signatures (⟪$p⟫)) | `(⟪upgrade $e:term to $e':term⟫) => `(Program.upgrade' $e $e' Program.return) | `(⟪upgrade $e:term to $e':term ; $p:program⟫) => diff --git a/Apps/TwoCounter.lean b/Apps/TwoCounter.lean index be2914d1..bf125aad 100644 --- a/Apps/TwoCounter.lean +++ b/Apps/TwoCounter.lean @@ -153,7 +153,7 @@ def incrementBoth : @Class.Method Eco.label Eco.Classes.TwoCounter Methods.Incre c1 := fetch self.c1 c2 := fetch self.c2 call Counter.Methods.Incr self.c1 (c2.count * n + c1.count) - call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) signed noSignatures + call Counter.Methods.Incr self.c2 (c1.count * n + c2.count) return self ⟫) diff --git a/Apps/UniversalCounter.lean b/Apps/UniversalCounter.lean index a23ef1b6..36300d55 100644 --- a/Apps/UniversalCounter.lean +++ b/Apps/UniversalCounter.lean @@ -147,5 +147,5 @@ example (rx ry : Reference Counter) : Applib.Program label Unit := ⟪ unfold label infer_instance ref := ry } - multiCall Counter.MultiMethods.Merge selves .unit noSignatures + multiCall Counter.MultiMethods.Merge selves .unit ⟫ diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean index 20be42be..50673e85 100644 --- a/Tests/Applib/Surface/Program/Syntax.lean +++ b/Tests/Applib/Surface/Program/Syntax.lean @@ -23,7 +23,7 @@ def mutualIncrement (rx ry : Reference Counter) (n : Nat) : Program Eco.label Un ⟫ def createCounter : Program Eco.label (Reference Counter) := ⟪ - r := create Counter Counter.Constructors.Zero () noSignatures + r := create Counter Counter.Constructors.Zero () call Counter.Methods.Incr r (7 : Nat); return r ⟫ @@ -79,11 +79,11 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ ⟫ example : Program Eco.label (Reference TwoCounter) := ⟪ - rx := create Counter Counter.Constructors.Zero () noSignatures - ry := create Counter Counter.Constructors.Zero () noSignatures + rx := create Counter Counter.Constructors.Zero () + ry := create Counter Counter.Constructors.Zero () call Counter.Methods.Incr rx (2 : Nat) call Counter.Methods.Incr ry (7 : Nat) - tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) noSignatures + tc := create TwoCounter TwoCounter.Constructors.Zero (rx, ry) return tc ⟫ @@ -218,17 +218,17 @@ open Applib example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program label (Reference OwnedCounter) := ⟪ c := fetch r call OwnedCounter.Methods.Transfer r newOwner; - r' := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + r' := create OwnedCounter OwnedCounter.Constructors.Zero () call OwnedCounter.Methods.Incr r' (c.count + 1); - destroy OwnedCounter.Destructors.Ten r () noSignatures + destroy OwnedCounter.Destructors.Ten r () return r' ⟫ example (n : Nat) : Program label (Reference OwnedCounter) := ⟪ - r := create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + r := create OwnedCounter OwnedCounter.Constructors.Zero () call OwnedCounter.Methods.Incr r n; - create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures - create OwnedCounter OwnedCounter.Constructors.Zero () noSignatures + create OwnedCounter OwnedCounter.Constructors.Zero () + create OwnedCounter OwnedCounter.Constructors.Zero () return r ⟫ From ca3a6511fd66fe60ef905ed8b1de3e4d7d3f28ec Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 13:08:40 +0200 Subject: [PATCH 08/17] remove import --- AVM/Class/Translation/Tasks.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/AVM/Class/Translation/Tasks.lean b/AVM/Class/Translation/Tasks.lean index 4f36d351..4ddd20e9 100644 --- a/AVM/Class/Translation/Tasks.lean +++ b/AVM/Class/Translation/Tasks.lean @@ -5,9 +5,6 @@ import AVM.Ecosystem import AVM.Class.Translation.Messages import AVM.Action --- TODO needed? -import AVM.Class.Label - namespace AVM /-- Type of functions which adjust object values by modifications that occurred From 65b6e3b4fcaef1d669b8233659a43a2467733870 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 13:26:36 +0200 Subject: [PATCH 09/17] add check syntax --- AVM/Class/Translation/Logics.lean | 60 ++++++++++++++----------------- Prelude/Check.lean | 7 ++++ 2 files changed, 34 insertions(+), 33 deletions(-) diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index 05b1452a..3a6ad0ec 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -16,24 +16,21 @@ private def Constructor.Message.logicFun let try msg : Message lab := Message.fromResource args.self match msg with | {id := id, contents := contents} => - -- TODO check syntax - if h : id == .classMember (Label.MemberId.constructorId constrId) - then - let contents : MessageContents lab (.classMember (Label.MemberId.constructorId constrId)) := eq_of_beq h ▸ contents - let argsData := contents.args - let try vals : (constr.body argsData).params.Product := tryCast contents.vals - let newObjData := constr.body argsData |>.value vals - let consumedResObjs := Logic.selectObjectResources args.consumed - let createdResObjs := Logic.selectObjectResources args.created - let signatures := contents.signatures - let! [newObjRes] := createdResObjs - let uid : ObjectId := newObjRes.nonce.value - Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs - && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs - && Logic.checkResourcesEphemeral consumedResObjs - && Logic.checkResourcesPersistent createdResObjs - && constr.invariant argsData signatures - else false + check h : id == .classMember (Label.MemberId.constructorId constrId) + let contents : MessageContents lab (.classMember (Label.MemberId.constructorId constrId)) := eq_of_beq h ▸ contents + let argsData := contents.args + let try vals : (constr.body argsData).params.Product := tryCast contents.vals + let newObjData := constr.body argsData |>.value vals + let consumedResObjs := Logic.selectObjectResources args.consumed + let createdResObjs := Logic.selectObjectResources args.created + let signatures := contents.signatures + let! [newObjRes] := createdResObjs + let uid : ObjectId := newObjRes.nonce.value + Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs + && Logic.checkResourceValues [newObjData.toObjectValue uid] createdResObjs + && Logic.checkResourcesEphemeral consumedResObjs + && Logic.checkResourcesPersistent createdResObjs + && constr.invariant argsData signatures /-- Creates a message logic function for a given destructor. -/ private def Destructor.Message.logicFun @@ -46,21 +43,18 @@ private def Destructor.Message.logicFun let try msg : Message lab := Message.fromResource args.self 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 + check h : id == .classMember (Label.MemberId.destructorId destructorId) + 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 private def Method.Message.logicFun {lab : Ecosystem.Label} diff --git a/Prelude/Check.lean b/Prelude/Check.lean index a8e0a8ad..9bd68a50 100644 --- a/Prelude/Check.lean +++ b/Prelude/Check.lean @@ -1,4 +1,9 @@ +import Lean.Parser.Term + +open Lean.Parser.Term + syntax withPosition("check" term) optSemicolon(term)? : term +syntax withPosition("check " binderIdent " : " term) optSemicolon(term) : term syntax withPosition("check" term) optSemicolon(doSeq) : doElem /-- The `check a; b` macro returns `b` if `a` evaluates to `true`, or `default` @@ -6,6 +11,8 @@ syntax withPosition("check" term) optSemicolon(doSeq) : doElem macro_rules | `(check $cond:term ; $body:term) => `(if $cond then $body else default) +| `(check $h:ident : $cond:term ; $body:term) => + `(if $h:ident : $cond then $body else default) | `(check $cond:term) => `($cond) | `(doElem| check $cond:term ; $body:doSeq) => From c420db120ae4a798e12b03ac5f0f6a5e4482b271 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 13:26:43 +0200 Subject: [PATCH 10/17] rename noSignatures -> unsigned --- Applib/Surface/Member.lean | 2 +- Applib/Surface/Program/Syntax.lean | 18 +++++++++--------- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/Applib/Surface/Member.lean b/Applib/Surface/Member.lean index b170b1d1..b5ac26dd 100644 --- a/Applib/Surface/Member.lean +++ b/Applib/Surface/Member.lean @@ -9,7 +9,7 @@ macro "noConstructors" : term => `(fun x => Empty.elim x) macro "noDestructors" : term => `(fun x => Empty.elim x) macro "noMethods" : term => `(fun x => Empty.elim x) -def noSignatures +def unsigned {Args SignatureId : Type} {args : Args} : SignatureId → Signature args := fun _ => Signature.sign args PrivateKey.universal diff --git a/Applib/Surface/Program/Syntax.lean b/Applib/Surface/Program/Syntax.lean index bfcb6215..2017b789 100644 --- a/Applib/Surface/Program/Syntax.lean +++ b/Applib/Surface/Program/Syntax.lean @@ -67,39 +67,39 @@ macro_rules | `(⟪if $cond:term then $thenProg:program ; $p:program⟫) => `(let next := fun () => ⟪$p⟫; if $cond then Program.invoke ⟪$thenProg⟫ next else next ()) | `(⟪create $c:ident $m:ident $e:term ⟫) => - `(Program.create' $c $m $e noSignatures Program.return) + `(Program.create' $c $m $e unsigned Program.return) | `(⟪create $c:ident $m:ident $e:term signed $signatures:term⟫) => `(Program.create' $c $m $e $signatures Program.return) | `(⟪create $c:ident $m:ident $e:term; $p:program⟫) => - `(Program.create' $c $m $e noSignatures (fun _ => ⟪$p⟫)) + `(Program.create' $c $m $e unsigned (fun _ => ⟪$p⟫)) | `(⟪create $c:ident $m:ident $e:term signed $signatures:term; $p:program⟫) => `(Program.create' $c $m $e $signatures (fun _ => ⟪$p⟫)) | `(⟪$x:ident := create $c:ident $m:ident $e:term; $p:program⟫) => - `(Program.create' $c $m $e noSignatures (fun $x => ⟪$p⟫)) + `(Program.create' $c $m $e unsigned (fun $x => ⟪$p⟫)) | `(⟪$x:ident := create $c:ident $m:ident $e:term signed $signatures:term; $p:program⟫) => `(Program.create' $c $m $e $signatures (fun $x => ⟪$p⟫)) | `(⟪destroy $m:ident $e:term $args:term⟫) => - `(Program.destroy' $e $m $args noSignatures (Program.return ())) + `(Program.destroy' $e $m $args unsigned (Program.return ())) | `(⟪destroy $m:ident $e:term $args:term signed $signatures:term⟫) => `(Program.destroy' $e $m $args $signatures (Program.return ())) | `(⟪destroy $m:ident $e:term $args:term; $p:program⟫) => - `(Program.destroy' $e $m $args noSignatures (⟪$p⟫)) + `(Program.destroy' $e $m $args unsigned (⟪$p⟫)) | `(⟪destroy $m:ident $e:term $args:term signed $signatures:term; $p:program⟫) => `(Program.destroy' $e $m $args $signatures (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term⟫) => - `(Program.call' $e $m $args noSignatures (Program.return ())) + `(Program.call' $e $m $args unsigned (Program.return ())) | `(⟪call $m:ident $e:term $args:term signed $signatures⟫) => `(Program.call' $e $m $args $signatures (Program.return ())) | `(⟪call $m:ident $e:term $args:term ; $p:program⟫) => - `(Program.call' $e $m $args noSignatures (⟪$p⟫)) + `(Program.call' $e $m $args unsigned (⟪$p⟫)) | `(⟪call $m:ident $e:term $args:term signed $signatures ; $p:program⟫) => `(Program.call' $e $m $args $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term⟫) => - `(Program.multiCall' $m $selves $args noSignatures (Program.return ())) + `(Program.multiCall' $m $selves $args unsigned (Program.return ())) | `(⟪multiCall $m:ident $selves:term $args:term signed $signatures:term; $p:program⟫) => `(Program.multiCall' $m $selves $args $signatures $signatures (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term; $p:program⟫) => - `(Program.multiCall' $m $selves $args noSignatures (⟪$p⟫)) + `(Program.multiCall' $m $selves $args unsigned (⟪$p⟫)) | `(⟪multiCall $m:ident $selves:term $args:term signed $signatures:term⟫) => `(Program.multiCall' $m $selves $args $signatures (Program.return ())) | `(⟪upgrade $e:term to $e':term⟫) => From 8a793bd27256c38cc67a4e0b5c8e68c984f268c0 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 13:30:42 +0200 Subject: [PATCH 11/17] remove semicolons --- Tests/Applib/Surface/Program/Syntax.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Tests/Applib/Surface/Program/Syntax.lean b/Tests/Applib/Surface/Program/Syntax.lean index 50673e85..5b19c462 100644 --- a/Tests/Applib/Surface/Program/Syntax.lean +++ b/Tests/Applib/Surface/Program/Syntax.lean @@ -24,7 +24,7 @@ def mutualIncrement (rx ry : Reference Counter) (n : Nat) : Program Eco.label Un def createCounter : Program Eco.label (Reference Counter) := ⟪ r := create Counter Counter.Constructors.Zero () - call Counter.Methods.Incr r (7 : Nat); + call Counter.Methods.Incr r (7 : Nat) return r ⟫ @@ -104,7 +104,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Counter := ⟪ match c1.count with | 0 => return c2 | Nat.succ n' => - call Counter.Methods.Incr cRef (3 : Nat); + call Counter.Methods.Incr cRef (3 : Nat) if c1.count > c2.count then c := fetch cRef invoke mutualIncrement self.c2 self.c1 (n' + c.count) @@ -127,7 +127,7 @@ example (self : TwoCounter) (n : Nat) : Program Eco.label Unit := ⟪ else invoke mutualIncrement self.c1 self.c2 n' call Counter.Methods.Incr self.c2 n' - call Counter.Methods.Incr self.c1 n; + call Counter.Methods.Incr self.c1 n call Counter.Methods.Incr self.c2 n ⟫ @@ -217,16 +217,16 @@ open Applib example (r : Reference OwnedCounter) (newOwner : PublicKey) : Program label (Reference OwnedCounter) := ⟪ c := fetch r - call OwnedCounter.Methods.Transfer r newOwner; + call OwnedCounter.Methods.Transfer r newOwner r' := create OwnedCounter OwnedCounter.Constructors.Zero () - call OwnedCounter.Methods.Incr r' (c.count + 1); + call OwnedCounter.Methods.Incr r' (c.count + 1) destroy OwnedCounter.Destructors.Ten r () return r' ⟫ example (n : Nat) : Program label (Reference OwnedCounter) := ⟪ r := create OwnedCounter OwnedCounter.Constructors.Zero () - call OwnedCounter.Methods.Incr r n; + call OwnedCounter.Methods.Incr r n create OwnedCounter OwnedCounter.Constructors.Zero () create OwnedCounter OwnedCounter.Constructors.Zero () return r From 0eb871622b0c777cd389729369e53a63f5bd21f5 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 15:41:35 +0200 Subject: [PATCH 12/17] revert refactor of Message --- AVM/Class/Label.lean | 6 +-- AVM/Class/Translation/Logics.lean | 43 +++++++++++----------- AVM/Class/Translation/Messages.lean | 57 +++++++++++++---------------- AVM/Ecosystem/Label/Base.lean | 6 +-- AVM/Message.lean | 4 +- AVM/Message/Base.lean | 31 +++++++--------- 6 files changed, 69 insertions(+), 78 deletions(-) diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean index 6cfff19c..96d840b8 100644 --- a/AVM/Class/Label.lean +++ b/AVM/Class/Label.lean @@ -122,13 +122,13 @@ instance Label.MemberId.instLawfulBEq {lab : Class.Label} : LawfulBEq (Class.Lab 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 := diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index c1173833..a751f201 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -15,15 +15,15 @@ private def Constructor.Message.logicFun : Bool := let try msg : Message lab := Message.fromResource args.self match msg with - | {id := id, contents := contents} => + | {id := id, args := argsData', signatures := signatures', vals := vals, ..} => check h : id == .classMember (Label.MemberId.constructorId constrId) - let contents : MessageContents lab (.classMember (Label.MemberId.constructorId constrId)) := eq_of_beq h ▸ contents - let argsData := contents.args - let try vals : (constr.body argsData).params.Product := tryCast contents.vals + have h' := eq_of_beq h + let argsData := cast (by simp! [h']) argsData' + let signatures := cast (by grind) signatures' + let try vals : (constr.body (argsData)).params.Product := tryCast vals let newObjData := constr.body argsData |>.value vals let consumedResObjs := Logic.selectObjectResources args.consumed let createdResObjs := Logic.selectObjectResources args.created - let signatures := contents.signatures let! [newObjRes] := createdResObjs let uid : ObjectId := newObjRes.nonce.value Logic.checkResourceValues [newObjData.toObjectValue uid] consumedResObjs @@ -42,11 +42,11 @@ private def Destructor.Message.logicFun : Bool := let try msg : Message lab := Message.fromResource args.self match msg with - | {id := id, contents := contents} => + | {id := id, args := args', signatures := signatures', ..} => check h : id == .classMember (Label.MemberId.destructorId destructorId) - 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 + have h' := eq_of_beq h + let argsData := cast (by simp! [h']) args' + let signatures : destructorId.Signatures argsData := cast (by grind) signatures' let consumedResObjs := Logic.selectObjectResources args.consumed let createdResObjs := Logic.selectObjectResources args.created let! [selfRes] := consumedResObjs @@ -65,18 +65,18 @@ private def Method.Message.logicFun : Bool := let try msg : Message lab := Message.fromResource args.self match msg with - | {id := id, contents := contents} => + | {id := id, args := args', signatures := signatures', vals := vals', ..} => 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 + have h' := eq_of_beq h + let argsData : methodId.Args.type := cast (by simp! [h']) 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 + let try vals : body.params.Product := tryCast vals' + let signatures : methodId.Signatures argsData := cast (by grind) signatures' check method.invariant selfObj argsData signatures let createdObject : Object classId := body |>.value vals Logic.checkResourceValues [createdObject.toObjectValue] createdResObjs @@ -121,8 +121,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.contents.recipients - && msg.contents.recipients.length == consumedObjectResources.length + self.uid ∈ msg.recipients + && msg.recipients.length == consumedObjectResources.length -- Note that the message logics already check if the consumed object -- resources have the right form, i.e., correspond to the self / selves. We -- only need to check that the number of recipients is equal to the number @@ -188,11 +188,11 @@ def MultiMethod.Message.logicFun : Bool := let try msg : Message lab := Message.fromResource args.self match msg with - | {id := id, contents := contents} => + | {id := id, args := args', signatures := signatures', ..} => if h : id == .multiMethodId multiId then - let contents : MessageContents lab (.multiMethodId multiId) := eq_of_beq h ▸ contents - let fargs : multiId.Args.type := contents.args + have h' := eq_of_beq h + let fargs : multiId.Args.type := cast (by simp! [h']) args' let consumedResObjs := Logic.selectObjectResources args.consumed let createdResObjs := Logic.selectObjectResources args.created let try (argsConsumedSelves, argsConstructedEph, .unit) := @@ -201,8 +201,9 @@ 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 contents.signatures - && let try vals : prog.params.Product := tryCast msg.contents.vals + let signatures := cast (by grind) signatures' + 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⟩ diff --git a/AVM/Class/Translation/Messages.lean b/AVM/Class/Translation/Messages.lean index d8a800de..c597104f 100644 --- a/AVM/Class/Translation/Messages.lean +++ b/AVM/Class/Translation/Messages.lean @@ -17,13 +17,12 @@ def Constructor.message (signatures : Class.Label.MemberId.constructorId constrId |>.Signatures args) : Message lab := { id := .classMember (.constructorId constrId) - contents := - { data := .unit - logicRef := Constructor.Message.logic.{0, 0} constr |>.reference - vals - args - signatures - recipients := [newId] }} + data := .unit + logicRef := Constructor.Message.logic.{0, 0} constr |>.reference + vals + args + signatures + recipients := [newId] } def Destructor.message {lab : Ecosystem.Label} @@ -37,13 +36,12 @@ def Destructor.message (signatures : Class.Label.MemberId.destructorId destrId |>.Signatures args) : Message lab := { id := .classMember (.destructorId destrId) - contents := - { data := .unit - logicRef := Destructor.Message.logic.{0, 0} destr |>.reference - vals - args - signatures - recipients := [selfId] }} + data := .unit + logicRef := Destructor.Message.logic.{0, 0} destr |>.reference + vals + args + signatures + recipients := [selfId] } def Method.message {lab : Ecosystem.Label} @@ -57,13 +55,12 @@ def Method.message (signatures : Class.Label.MemberId.methodId methodId |>.Signatures args) : Message lab := { id := .classMember (.methodId methodId) - contents := - { data := .unit - logicRef := Method.Message.logic.{0, 0} method |>.reference - vals - args - signatures - recipients := [selfId] }} + data := .unit + logicRef := Method.Message.logic.{0, 0} method |>.reference + vals + args + signatures + recipients := [selfId] } def Upgrade.message {lab : Ecosystem.Label} @@ -71,14 +68,13 @@ def Upgrade.message (selfId : ObjectId) : Message lab := { id := .classMember (classId := classId) .upgradeId - contents := - { data := .unit - logicRef := Upgrade.Message.logic.{0, 0} classId |>.reference - Vals := ⟨PUnit⟩ - vals := PUnit.unit - args := .unit - signatures f := nomatch f - recipients := [selfId] }} + data := .unit + logicRef := Upgrade.Message.logic.{0, 0} classId |>.reference + Vals := ⟨PUnit⟩ + vals := PUnit.unit + args := .unit + signatures f := nomatch f + recipients := [selfId] } end AVM.Class @@ -96,7 +92,6 @@ def MultiMethod.message (rands : MultiMethodRandoms data) : Message lab := { id := .multiMethodId multiId - contents := { logicRef := MultiMethod.Message.logic.{0, 0} method data |>.reference data Vals := ⟨(method.body selves args).params.Product⟩ @@ -105,4 +100,4 @@ def MultiMethod.message signatures recipients := (Label.MultiMethodId.SelvesToVector selves (fun obj => obj.uid) |>.toList) - ++ rands.constructedNonces.toList.map (·.value) }} + ++ rands.constructedNonces.toList.map (·.value) } diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean index 133dc8e5..8cc8d957 100644 --- a/AVM/Ecosystem/Label/Base.lean +++ b/AVM/Ecosystem/Label/Base.lean @@ -94,12 +94,12 @@ instance {lab : Ecosystem.Label} {classId : lab.ClassId} namespace MultiMethodId -def Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType := +abbrev Args {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : SomeType := lab.MultiMethodArgs multiId -def SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId +abbrev SignatureId {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) : Type := lab.MultiMethodSignatureId multiId -def Signatures {lab : Ecosystem.Label} (multiId : lab.MultiMethodId) (args : multiId.Args.type) : Type := +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 := diff --git a/AVM/Message.lean b/AVM/Message.lean index 78c08ddf..f323e663 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.contents.logicRef, + logicRef := msg.message.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.{u, v}) : Option SomeMessage := let try msg : SomeMessage := tryCast res.label - check (msg.message.contents.logicRef == res.logicRef) + check (msg.message.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 299ba35c..93bba704 100644 --- a/AVM/Message/Base.lean +++ b/AVM/Message/Base.lean @@ -3,6 +3,11 @@ import AVM.Ecosystem.Data namespace AVM structure MessageContents (lab : Ecosystem.Label) (id : lab.MemberId) : Type 1 where + +/-- 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 @@ -21,27 +26,18 @@ structure MessageContents (lab : Ecosystem.Label) (id : lab.MemberId) : Type 1 w /-- The recipients of the message. -/ recipients : List ObjectId -/-- 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 - /-- The data that the message carries. -/ - contents : MessageContents lab id - -instance MessageContents.hasBEq {lab : Ecosystem.Label} {id : lab.MemberId} : BEq (MessageContents lab id) where - beq a b := - a.vals === b.vals - && a.args == b.args - && a.recipients == b.recipients - instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) where rep := Rep.composite "AVM.Message" [Rep.atomic lab.name] instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where beq a b := - if h : a.id == b.id - then a.contents == eq_of_beq h ▸ b.contents - else false + match a, b with + | {id := aid, args := aargs, ..}, {id := bid, args := bargs, ..} => + check h : aid == bid + let h' := eq_of_beq h + check a.vals === b.vals + check aargs == h' ▸ bargs + check a.recipients == b.recipients structure SomeMessage : Type 1 where {label : Ecosystem.Label} @@ -57,14 +53,13 @@ instance : Inhabited SomeMessage where default := { label := Ecosystem.Label.dummy message := { id := .classMember (classId := .unit) (.constructorId PUnit.unit) - contents := { Vals := ⟨PUnit⟩ vals := PUnit.unit data := .unit logicRef := default signatures f := nomatch f args := PUnit.unit - recipients := [] }}} + recipients := [] }} def Message.toSomeMessage {lab : Ecosystem.Label} (msg : Message lab) : SomeMessage := { label := lab, message := msg } From 97105101c5eb297ea8096cab14f2c93bd77d83d7 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 15:45:38 +0200 Subject: [PATCH 13/17] todo --- AVM/Message/Base.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean index 93bba704..d587d1aa 100644 --- a/AVM/Message/Base.lean +++ b/AVM/Message/Base.lean @@ -38,6 +38,7 @@ instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where check a.vals === b.vals check aargs == h' ▸ bargs check a.recipients == b.recipients + sorry -- TODO check equality of signatures structure SomeMessage : Type 1 where {label : Ecosystem.Label} From 1947a3c5b185d035b84402f90bc819c227f4cd29 Mon Sep 17 00:00:00 2001 From: Jan Mas Rovira Date: Wed, 24 Sep 2025 18:09:06 +0200 Subject: [PATCH 14/17] compare signatures --- AVM/Authorization.lean | 10 +++++++++- AVM/Class/Label.lean | 6 ++++++ AVM/Ecosystem/Label/Base.lean | 2 ++ AVM/Message/Base.lean | 18 +++++++++++++++--- Apps/Kudos.lean | 9 ++++++--- Apps/KudosBank.lean | 8 ++++++-- Apps/OwnedCounter.lean | 9 ++++++--- 7 files changed, 50 insertions(+), 12 deletions(-) diff --git a/AVM/Authorization.lean b/AVM/Authorization.lean index de293247..17892157 100644 --- a/AVM/Authorization.lean +++ b/AVM/Authorization.lean @@ -21,11 +21,19 @@ def PrivateKey.universal : PrivateKey where -- mock function def checkKey (pub : PublicKey) (priv : PrivateKey) : Bool := pub.key == priv.key -structure Signature {A : Type u} (msg : A) : Type where +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 diff --git a/AVM/Class/Label.lean b/AVM/Class/Label.lean index 96d840b8..3ae1333d 100644 --- a/AVM/Class/Label.lean +++ b/AVM/Class/Label.lean @@ -35,6 +35,8 @@ 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] @@ -43,6 +45,8 @@ 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 [destructorsFinite : Fintype DestructorId] [destructorsRepr : Repr DestructorId] [destructorsBEq : BEq DestructorId] @@ -51,6 +55,8 @@ 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 [methodsFinite : Fintype MethodId] [methodsRepr : Repr MethodId] [methodsBEq : BEq MethodId] diff --git a/AVM/Ecosystem/Label/Base.lean b/AVM/Ecosystem/Label/Base.lean index 8cc8d957..259d99dd 100644 --- a/AVM/Ecosystem/Label/Base.lean +++ b/AVM/Ecosystem/Label/Base.lean @@ -21,6 +21,8 @@ structure Label : Type 1 where /-- 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] diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean index d587d1aa..f32f6b08 100644 --- a/AVM/Message/Base.lean +++ b/AVM/Message/Base.lean @@ -26,19 +26,31 @@ structure Message (lab : Ecosystem.Label) : Type 1 where /-- The recipients of the message. -/ recipients : List ObjectId +def Message.rawSignatures {lab : Ecosystem.Label} (msg : Message lab) : List Nat := + match msg with + | {id := id, signatures := signatures, ..} => + 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 => [] + instance Message.hasTypeRep (lab : Ecosystem.Label) : TypeRep (Message lab) where rep := Rep.composite "AVM.Message" [Rep.atomic lab.name] instance Message.hasBEq {lab : Ecosystem.Label} : BEq (Message lab) where beq a b := match a, b with - | {id := aid, args := aargs, ..}, {id := bid, args := bargs, ..} => + | {id := aid, args := aargs, signatures := asigs, ..}, + {id := bid, args := bargs, signatures := bsigs, ..} => check h : aid == bid let h' := eq_of_beq h check a.vals === b.vals - check aargs == h' ▸ bargs + check s : aargs == cast (by simp! [h']) bargs check a.recipients == b.recipients - sorry -- TODO check equality of signatures + check a.rawSignatures == b.rawSignatures structure SomeMessage : Type 1 where {label : Ecosystem.Label} diff --git a/Apps/Kudos.lean b/Apps/Kudos.lean index 692e08bb..b92b7df5 100644 --- a/Apps/Kudos.lean +++ b/Apps/Kudos.lean @@ -34,8 +34,9 @@ namespace Methods inductive Transfer.SignatureId : Type where | owner + deriving DecidableEq, FinEnum -def SignatureId : Methods → Type +abbrev SignatureId : Methods → Type | .Transfer => Transfer.SignatureId end Methods @@ -48,8 +49,9 @@ namespace Constructors inductive Mint.SignatureId where | originator + deriving DecidableEq, FinEnum -def SignatureId (m : Constructors) : Type := +abbrev SignatureId (m : Constructors) : Type := match m with | .Mint => Mint.SignatureId @@ -63,8 +65,9 @@ namespace Destructors inductive Burn.SignatureId : Type where | owner + deriving DecidableEq, FinEnum -def SignatureId : Destructors → Type +abbrev SignatureId : Destructors → Type | .Burn => Burn.SignatureId end Destructors diff --git a/Apps/KudosBank.lean b/Apps/KudosBank.lean index b5cb3459..edb2b1b6 100644 --- a/Apps/KudosBank.lean +++ b/Apps/KudosBank.lean @@ -163,15 +163,18 @@ namespace Methods inductive Transfer.SignatureId where | owner + deriving DecidableEq, FinEnum inductive Mint.SignatureId where | owner + deriving DecidableEq, FinEnum inductive Burn.SignatureId where | owner | originator + deriving DecidableEq, FinEnum -def SignatureId (m : Methods) : Type := +abbrev SignatureId (m : Methods) : Type := match m with | .Transfer => Transfer.SignatureId | .Mint => Mint.SignatureId @@ -191,8 +194,9 @@ namespace Destructors inductive Close.SignatureId : Type where | owner + deriving DecidableEq, FinEnum -def SignatureId : Destructors → Type +abbrev SignatureId : Destructors → Type | .Close => Close.SignatureId end Destructors diff --git a/Apps/OwnedCounter.lean b/Apps/OwnedCounter.lean index cd52b05b..1df7d357 100644 --- a/Apps/OwnedCounter.lean +++ b/Apps/OwnedCounter.lean @@ -24,12 +24,14 @@ namespace Methods inductive Transfer.SignatureId : Type where | owner + deriving DecidableEq, FinEnum inductive Incr.SignatureId : Type where | owner + deriving DecidableEq, FinEnum -def SignatureId : Methods → Type - | .Incr => Transfer.SignatureId +abbrev SignatureId : Methods → Type + | .Incr => Incr.SignatureId | .Transfer => Transfer.SignatureId end Methods @@ -46,8 +48,9 @@ namespace Destructors inductive Ten.SignatureId : Type where | owner + deriving DecidableEq, FinEnum -def SignatureId : Destructors → Type +abbrev SignatureId : Destructors → Type | .Ten => Ten.SignatureId end Destructors From 456142fa2ce1abcfccfed07d4199ad9cb9aae241 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Sep 2025 18:41:48 +0200 Subject: [PATCH 15/17] refactor logics --- AVM/Class/Translation/Logics.lean | 53 ++++++++++++------------------- Prelude/Check.lean | 3 ++ 2 files changed, 24 insertions(+), 32 deletions(-) diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index a751f201..c5ea1eff 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -14,13 +14,10 @@ private def Constructor.Message.logicFun (args : Logic.Args) : Bool := let try msg : Message lab := Message.fromResource args.self - match msg with - | {id := id, args := argsData', signatures := signatures', vals := vals, ..} => - check h : id == .classMember (Label.MemberId.constructorId constrId) - have h' := eq_of_beq h - let argsData := cast (by simp! [h']) argsData' - let signatures := cast (by grind) signatures' - let try vals : (constr.body (argsData)).params.Product := tryCast vals + 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 let createdResObjs := Logic.selectObjectResources args.created @@ -41,12 +38,9 @@ private def Destructor.Message.logicFun (args : Logic.Args) : Bool := let try msg : Message lab := Message.fromResource args.self - match msg with - | {id := id, args := args', signatures := signatures', ..} => - check h : id == .classMember (Label.MemberId.destructorId destructorId) - have h' := eq_of_beq h - let argsData := cast (by simp! [h']) args' - let signatures : destructorId.Signatures argsData := cast (by grind) signatures' + 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 @@ -64,25 +58,20 @@ private def Method.Message.logicFun (args : Logic.Args) : Bool := let try msg : Message lab := Message.fromResource args.self - match msg with - | {id := id, args := args', signatures := signatures', vals := vals', ..} => - if h : id == .classMember (Label.MemberId.methodId methodId) - then - have h' := eq_of_beq h - let argsData : methodId.Args.type := cast (by simp! [h']) 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 vals' - let signatures : methodId.Signatures argsData := cast (by grind) 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 + 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 + 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 + && Logic.checkResourcesPersistent createdResObjs private def Upgrade.Message.logicFun {lab : Ecosystem.Label} diff --git a/Prelude/Check.lean b/Prelude/Check.lean index 9bd68a50..345b7cd8 100644 --- a/Prelude/Check.lean +++ b/Prelude/Check.lean @@ -5,6 +5,7 @@ open Lean.Parser.Term syntax withPosition("check" term) optSemicolon(term)? : term syntax withPosition("check " binderIdent " : " term) optSemicolon(term) : term syntax withPosition("check" term) optSemicolon(doSeq) : doElem +syntax withPosition("check " binderIdent " : " term) optSemicolon(doSeq) : doElem /-- The `check a; b` macro returns `b` if `a` evaluates to `true`, or `default` otherwise. -/ @@ -17,3 +18,5 @@ macro_rules `($cond) | `(doElem| check $cond:term ; $body:doSeq) => `(doElem| if $cond then $body else pure default) +| `(doElem| check $h:ident : $cond:term ; $body:doSeq) => + `(doElem| if $h : $cond then $body else pure default) From 3da682be686c07cbd1f3f8ee82cf60f4bd177ead Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Sep 2025 18:46:46 +0200 Subject: [PATCH 16/17] refactor multi-method message logic --- AVM/Class/Translation/Logics.lean | 82 +++++++++++++++---------------- 1 file changed, 39 insertions(+), 43 deletions(-) diff --git a/AVM/Class/Translation/Logics.lean b/AVM/Class/Translation/Logics.lean index c5ea1eff..44db2cc8 100644 --- a/AVM/Class/Translation/Logics.lean +++ b/AVM/Class/Translation/Logics.lean @@ -17,7 +17,7 @@ private def Constructor.Message.logicFun 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 try vals : (constr.body argsData).params.Product := tryCast msg.vals let newObjData := constr.body argsData |>.value vals let consumedResObjs := Logic.selectObjectResources args.consumed let createdResObjs := Logic.selectObjectResources args.created @@ -176,48 +176,44 @@ def MultiMethod.Message.logicFun (data : MultiMethodData) : Bool := let try msg : Message lab := Message.fromResource args.self - match msg with - | {id := id, args := args', signatures := signatures', ..} => - if h : id == .multiMethodId multiId - then - have h' := eq_of_beq h - let fargs : multiId.Args.type := cast (by simp! [h']) args' - let consumedResObjs := Logic.selectObjectResources args.consumed - let createdResObjs := Logic.selectObjectResources args.created - let try (argsConsumedSelves, argsConstructedEph, .unit) := - consumedResObjs - |> Logic.filterOutDummy - |>.splitsExact [multiId.numObjectArgs, data.numConstructed] - let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves.toList - let prog := method.body argsConsumedObjects fargs - let signatures := cast (by grind) signatures' - 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 - else false + 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) := + consumedResObjs + |> Logic.filterOutDummy + |>.splitsExact [multiId.numObjectArgs, data.numConstructed] + let try argsConsumedObjects : multiId.Selves := Label.MultiMethodId.ConsumedToSelves argsConsumedSelves.toList + 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 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 def MultiMethod.Message.logic {lab : Ecosystem.Label} From bba5b72f80c38c712b2146259b527fa14ef4b071 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Wed, 24 Sep 2025 18:51:22 +0200 Subject: [PATCH 17/17] remove MessageContents --- AVM/Message/Base.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/AVM/Message/Base.lean b/AVM/Message/Base.lean index f32f6b08..0979c478 100644 --- a/AVM/Message/Base.lean +++ b/AVM/Message/Base.lean @@ -2,8 +2,6 @@ import AVM.Ecosystem.Data namespace AVM -structure MessageContents (lab : Ecosystem.Label) (id : lab.MemberId) : Type 1 where - /-- 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. -/