From ce95fd809c060ea66ecaabbd8b261d7a369f937d Mon Sep 17 00:00:00 2001 From: Michael Heuer Date: Thu, 4 Jul 2024 15:05:55 +0200 Subject: [PATCH] feat: implement initial version --- .gitignore | 4 + AnomaHelpers.juvix | 63 ++++++++++++ Authorization/Owner.juvix | 58 +++++++++++ Intent/DSL.juvix | 76 ++++++++++++++ Package.juvix | 12 +++ README.md | 4 +- Token/Label.juvix | 23 +++++ Token/Logic.juvix | 16 +++ Token/Resource.juvix | 25 +++++ Token/Transaction.juvix | 211 ++++++++++++++++++++++++++++++++++++++ juvix.lock.yaml | 31 ++++++ 11 files changed, 521 insertions(+), 2 deletions(-) create mode 100644 .gitignore create mode 100644 AnomaHelpers.juvix create mode 100644 Authorization/Owner.juvix create mode 100644 Intent/DSL.juvix create mode 100644 Package.juvix create mode 100644 Token/Label.juvix create mode 100644 Token/Logic.juvix create mode 100644 Token/Resource.juvix create mode 100644 Token/Transaction.juvix create mode 100644 juvix.lock.yaml diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..33dafc2 --- /dev/null +++ b/.gitignore @@ -0,0 +1,4 @@ +.juvix-build +.history +*.nockma +.DS_Store diff --git a/AnomaHelpers.juvix b/AnomaHelpers.juvix new file mode 100644 index 0000000..18847b2 --- /dev/null +++ b/AnomaHelpers.juvix @@ -0,0 +1,63 @@ +module AnomaHelpers; + +import Stdlib.Prelude open; +import Data.Map open; +import Data.Set open; +import Anoma open; + + +-- TODO all these helpers should be in `juvix-anoma-stdlib` + +syntax alias Bytes32 := Nat; +syntax alias Bytes := Nat; + +isCreated (r : Resource) (tx : Transaction) : Bool := + elem (==) r (ResourcePartition.created (partitionResources tx)); + +isConsumed (r : Resource) (tx : Transaction) : Bool := + elem (==) r (ResourcePartition.consumed (partitionResources tx)); + + +isPresent (cms : List Helper.Commitment) (cm : Helper.Commitment) : Bool := + elem (==) cm cms; + +isSublist (sub sup : List Helper.Commitment) : Bool := + all (isPresent sup) sub; + +isSubset {A} {{Ord A}} (sub sup : Set A) : Bool := + all (x in Data.Set.toList sub) + member? x sup; + + +isSubsetOfCreatedResources (sub : Set Helper.Commitment) (tx : Transaction) : Bool := + let + sup : Set Helper.Commitment := Data.Set.fromList (map commitment (ResourcePartition.created (partitionResources tx))); + in + isSubset sub sup; + +lookupExtraData {Value : Type} (key : Bytes32) (tx : Transaction) : Maybe Value := + let + keyValueMap : Map Bytes32 Value := anomaDecode (Transaction.extra tx); + in + lookup key keyValueMap; + + +-- This helper replicates the private key to compute the nullifiers. TODO +mkTransaction + (self : PrivateKey) + (consumed : List Resource) + (created : List Resource) + (extraData : Map Bytes32 Bytes) + : Transaction := + let + replicatedPrivKey : List PrivateKey := replicate (length consumed) self; + in + Transaction.mk@{ + roots := []; + commitments := map commitment created; + nullifiers := zipWith nullifier consumed replicatedPrivKey; + proofs := consumed ++ created; + delta := []; + extra := anomaEncode (extraData); + preference := 0 + }; diff --git a/Authorization/Owner.juvix b/Authorization/Owner.juvix new file mode 100644 index 0000000..4f8ecfc --- /dev/null +++ b/Authorization/Owner.juvix @@ -0,0 +1,58 @@ +module Authorization.Owner; + +import Stdlib.Prelude open; +import Data.Map open; +import Data.Set open; +import Anoma open; + +import AnomaHelpers open; + +type Owner := + mkOwner { + owner : PublicKey; + }; + +instance +Owner-Eq : Eq Owner := + mkEq@{ + eq (d1 d2 : Owner) : Bool := + Owner.owner d1 == Owner.owner d2 + }; + +getOwner (r : Resource) : PublicKey := + Owner.owner (anomaDecode (Resource.data r)); + +type AuthMessage := + mkAuthMessage { + consumed : Helper.Nullifier; + mustBeCreated : Set Helper.Commitment; + }; + + mkAuthExtraDataMapEntry (self : PrivateKey) (created : List Resource) (consumed : Resource) : Pair Bytes32 Bytes := + let + consumedNk : Helper.Nullifier := nullifier consumed self; + createdCms : Set Helper.Commitment := Data.Set.fromList (map commitment created); + msg : AuthMessage := mkAuthMessage@{consumed := consumedNk; mustBeCreated := createdCms;}; + + k := consumedNk; + v := anomaEncode(msg, anomaSignDetached msg self); + in + (k, v); + + mkAuthExtraData (self : PrivateKey) (consumed : List Resource) (created : List Resource) : Map Bytes32 Bytes := + Data.Map.fromList (map (mkAuthExtraDataMapEntry self created) consumed); + + +isAuthorizedByOwner (self : Resource) (tx : Transaction) : Bool := + let + owner : PublicKey := getOwner self; + selfNk : Helper.Commitment := commitment self; + lookupResult : Maybe (Pair AuthMessage Signature) := lookupExtraData selfNk tx ; + in + case lookupResult of + | nothing := false + | just (msg, sig) := + AuthMessage.consumed msg == selfNk + && anomaVerifyDetached sig msg owner + && isSubsetOfCreatedResources (AuthMessage.mustBeCreated msg) tx + ; diff --git a/Intent/DSL.juvix b/Intent/DSL.juvix new file mode 100644 index 0000000..66d569e --- /dev/null +++ b/Intent/DSL.juvix @@ -0,0 +1,76 @@ +--- A DSL for constructing intents +module Intent.DSL; + +import Stdlib.Prelude open hiding {for; any; all}; +import Anoma open public; + +type Asset := + mkAsset { + quantity : Nat; + kind : Kind + }; + +type Quantifier := + | Any + | All; + +type QuantifiedAssets := + mkAssets { + quantifier : Quantifier; + assets : List Asset + }; + +syntax operator of_ additive; +syntax alias of_ := mkAsset; + +type Intention := + | Want + | Give; + +type Clause := + mkClause { + lhs : Pair Intention QuantifiedAssets; + rhs : QuantifiedAssets + }; + +any (as : List Asset) : QuantifiedAssets := + mkAssets@{ + quantifier := Any; + assets := as + }; + +all (as : List Asset) : QuantifiedAssets := + mkAssets@{ + quantifier := All; + assets := as + }; + +exactly (a : Asset) : QuantifiedAssets := + mkAssets@{ + quantifier := All; + assets := [a] + }; + +want + (a : QuantifiedAssets) : Pair Intention QuantifiedAssets := + Want, a; + +give + (a : QuantifiedAssets) : Pair Intention QuantifiedAssets := + Give, a; + +syntax operator for pair; + +for + (l : Pair Intention QuantifiedAssets) + (qs : QuantifiedAssets) + : Clause := + mkClause@{ + lhs := l; + rhs := qs + }; + +intent (clauses : List Clause) : Resource := + mkIntent clauses; + +axiom mkIntent : List Clause -> Resource; diff --git a/Package.juvix b/Package.juvix new file mode 100644 index 0000000..9a9629a --- /dev/null +++ b/Package.juvix @@ -0,0 +1,12 @@ +module Package; + +import PackageDescription.V2 open; + +package : Package := + defaultPackage + {name := "anoma-app-patterns"; + version := mkVersion 0 0 1; + dependencies := [ github "anoma" "juvix-anoma-stdlib" "v0.1.0" + ; github "anoma" "juvix-stdlib" "v0.4.0" + ; github "anoma" "juvix-containers" "v0.12.1" + ]}; diff --git a/README.md b/README.md index 921aa14..8543859 100644 --- a/README.md +++ b/README.md @@ -1,3 +1,3 @@ -# Nomine +# Anoma App Patterns -Nomine is a library for intent-centric application development. +A library for intent-centric application development. diff --git a/Token/Label.juvix b/Token/Label.juvix new file mode 100644 index 0000000..c9eb95c --- /dev/null +++ b/Token/Label.juvix @@ -0,0 +1,23 @@ +module Token.Label; + +import Stdlib.Prelude open; +import Anoma open; + +type Label := + mkLabel { + name : Nat; + symbol : String; + decimals : Nat + }; + +instance +Label-Eq : Eq Label := + mkEq@{ + eq (d1 d2 : Label) : Bool := + Label.name d1 == Label.name d2 + && Label.symbol d1 == Label.symbol d2 + && Label.decimals d1 == Label.decimals d2 + }; + +getLabel (r : Resource) : Label := + anomaDecode (Resource.label r); diff --git a/Token/Logic.juvix b/Token/Logic.juvix new file mode 100644 index 0000000..30e42bd --- /dev/null +++ b/Token/Logic.juvix @@ -0,0 +1,16 @@ +module Token.Logic; + +import Stdlib.Prelude open; +import Anoma open; +import AnomaHelpers open; + +import Authorization.Owner open; + +tokenLogic (self : Resource) (tx : Transaction) : Bool := + if + | isConsumed self tx := isAuthorizedByOwner self tx + | isCreated self tx := true + | else := false; + + +-- TODO Implement fixed supply diff --git a/Token/Resource.juvix b/Token/Resource.juvix new file mode 100644 index 0000000..8f17df5 --- /dev/null +++ b/Token/Resource.juvix @@ -0,0 +1,25 @@ +module Token.Resource; + +import Stdlib.Prelude open; +import Anoma open; + +import Token.Label open; +import Token.Logic open; +import Authorization.Owner open; + +mkToken + (ephemeral : Bool) + (amount : Nat) + (tokenLabel : Label) + (ownerData : Owner) + : Resource := + Resource.mk@{ + logic := tokenLogic; + label := anomaEncode tokenLabel; + quantity := amount; + data := anomaEncode ownerData; + eph := ephemeral; + npk := Owner.owner ownerData; + nonce := 0; + rseed := 0 + }; diff --git a/Token/Transaction.juvix b/Token/Transaction.juvix new file mode 100644 index 0000000..00a542c --- /dev/null +++ b/Token/Transaction.juvix @@ -0,0 +1,211 @@ +module Token.Transaction; + +import Stdlib.Prelude open; +import Data.Map open; +import Anoma open; +import AnomaHelpers open; + +import Token.Resource open; +import Token.Label open; +import Token.Logic open; +import Authorization.Owner open; + +--- Mints a token ;Resource; owned by an receiver ;PublicKey;. +--- This requires an ephemeral resource to be consumed. +mint + (self : KeyPair) + (label : Label) + (amount : Nat) + (receiver : PublicKey) + : Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + mySecret : PrivateKey := KeyPair.privKey self; + + ephToken : Resource := + mkToken + true + amount + label + mkOwner@{ + owner := myself + }; + newToken : Resource := + mkToken + false + amount + label + mkOwner@{ + owner := receiver + }; + + consumedRs : List Resource := [ephToken]; + createdRs : List Resource := [newToken]; + extraData : Map Bytes32 Bytes := + mkAuthExtraData mySecret consumedRs createdRs; + in mkTransaction mySecret consumedRs createdRs extraData; + +--- Burns a token ;Resource;, if the calling ;KeyPair; is the owner. +--- This requires an ephemeral resource to be created. +--- If the calling ;KeyPair; is not the owner, this function returns nothing. +burn + (self : KeyPair) (token : Resource) : Maybe Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + mySecret : PrivateKey := KeyPair.privKey self; + + -- This ephemeral resource is needed for the total balance check. + ephToken := + mkToken + true + (Resource.quantity token) + (getLabel token) + mkOwner@{ + owner := 0 + }; + + consumedRs : List Resource := [token]; + createdRs : List Resource := [ephToken]; + extraData : Map Bytes32 Bytes := + mkAuthExtraData mySecret consumedRs createdRs; + in if + | getOwner (token) /= myself := nothing + | else := + just + (mkTransaction mySecret consumedRs createdRs extraData); + +--- Sends an amount of token ;Resource; to receiver, if the calling ;KeyPair; is the owner. +--- If the calling ;KeyPair; is not the owner, this function returns nothing. +--- If the amount exceeds the quantity available in the resource, the function returns nothing. +send + (self : KeyPair) + (token : Resource) + (amount : Nat) + (receiver : PublicKey) + : Maybe Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + availableAmount : Nat := Resource.quantity token; + in if + | getOwner (token) /= myself := nothing + | availableAmount < amount := nothing + | availableAmount == amount := transfer self token receiver + | availableAmount > amount := + let + remainder : Nat := + toNat (intSubNat availableAmount amount); + in split self token (amount, receiver) (remainder, myself) + | else := nothing; + +--- Transfers the token ;Resource; to a receiver, if the calling ;KeyPair; is the owner. +--- If the calling ;KeyPair; is not the owner, this function returns nothing. +transfer + (self : KeyPair) + (token : Resource) + (receiver : PublicKey) + : Maybe Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + mySecret : PrivateKey := KeyPair.privKey self; + + newToken := + mkToken + false + (Resource.quantity token) + (getLabel token) + mkOwner@{ + owner := receiver + }; + + consumedRs : List Resource := [token]; + createdRs : List Resource := [newToken]; + extraData : Map Bytes32 Bytes := + mkAuthExtraData mySecret consumedRs createdRs; + in if + | getOwner token == myself := + just + (mkTransaction mySecret consumedRs createdRs extraData) + | else := nothing; + +--- Splits a token ;Resource;, if the calling ;KeyPair; is the owner. +--- If the calling ;KeyPair; is not the owner or if the amounts do not balance, this function returns nothing. +split + (self : KeyPair) + (token : Resource) + (amountAndReceiverA amountAndReceiverB : Pair Nat PublicKey) + : Maybe Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + mySecret : PrivateKey := KeyPair.privKey self; + + label : Label := anomaDecode (Resource.label token); + sum : Nat := + fst amountAndReceiverA + fst amountAndReceiverB; + + outA : Resource := + mkToken + false + (fst amountAndReceiverA) + label + mkOwner@{ + owner := snd amountAndReceiverA + }; + outB : Resource := + mkToken + false + (fst amountAndReceiverB) + label + mkOwner@{ + owner := snd amountAndReceiverB + }; + + consumedRs : List Resource := [token]; + createdRs : List Resource := outA :: outB :: nil; + extraData : Map Bytes32 Bytes := + mkAuthExtraData mySecret consumedRs createdRs; + in if + | getOwner token == myself + && Resource.quantity token == sum := + just + (mkTransaction mySecret consumedRs createdRs extraData) + | else := nothing; + +--- Merges two token ;Resource;s, if the calling ;KeyPair; is the owner of both. +--- If the calling ;KeyPair; is not the owner, this function returns nothing. +merge + (self : KeyPair) + (tokenA tokenB : Resource) + (receiver : PublicKey) + : Maybe Transaction := + let + myself : PublicKey := KeyPair.pubKey self; + mySecret : PrivateKey := KeyPair.privKey self; + + ownerA : PublicKey := getOwner tokenA; + ownerB : PublicKey := getOwner tokenB; + + labelA : Label := anomaDecode (Resource.label tokenA); + labelB : Label := anomaDecode (Resource.label tokenB); + + sum : Nat := + Resource.quantity tokenA + Resource.quantity tokenB; + merged : Resource := + mkToken + false + sum + labelA + mkOwner@{ + owner := myself + }; + + consumedRs : List Resource := tokenA :: tokenB :: nil; + createdRs : List Resource := [merged]; + extraData : Map Bytes32 Bytes := + mkAuthExtraData mySecret consumedRs createdRs; + in if + | labelA == labelB + && ownerA == myself + && ownerB == myself := + just + (mkTransaction mySecret consumedRs createdRs extraData) + | else := nothing; diff --git a/juvix.lock.yaml b/juvix.lock.yaml new file mode 100644 index 0000000..be25465 --- /dev/null +++ b/juvix.lock.yaml @@ -0,0 +1,31 @@ +# This file was autogenerated by Juvix version 0.6.3. +# Do not edit this file manually. + +version: 2 +checksum: b42848b886785561d154b016f2b4e6d9d88742c2e73469b0dec2967f952ad8c6 +dependencies: +- git: + name: anoma_juvix-anoma-stdlib + ref: 835ce837e75c35319ab7e362953f23f1bc5fd3e5 + url: https://github.com/anoma/juvix-anoma-stdlib + dependencies: + - git: + name: anoma_juvix-stdlib + ref: 89a5960fb8a29291e9271986b98ca7b1edf4031b + url: https://github.com/anoma/juvix-stdlib + dependencies: [] +- git: + name: anoma_juvix-stdlib + ref: 89a5960fb8a29291e9271986b98ca7b1edf4031b + url: https://github.com/anoma/juvix-stdlib + dependencies: [] +- git: + name: anoma_juvix-containers + ref: c4c7af9bdf36aa9d2dbdc7e0372dd9278f60ff26 + url: https://github.com/anoma/juvix-containers + dependencies: + - git: + name: anoma_juvix-stdlib + ref: 89a5960fb8a29291e9271986b98ca7b1edf4031b + url: https://github.com/anoma/juvix-stdlib + dependencies: []