-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
* use mtl * update to mtl 0.1.0 * update mtl to v0.1.1 and stdlib to v0.10.0 * wip * bug * add trait Tx * export Tx module * use Tx instead of Reader
- Loading branch information
1 parent
4f4b17e
commit 59e2a36
Showing
7 changed files
with
128 additions
and
17 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,13 @@ | ||
module Applib.Data.StandardInputs; | ||
|
||
import Stdlib.Prelude open; | ||
import Anoma.State open; | ||
import Anoma open; | ||
import Applib.Identities open; | ||
|
||
--- Standard inputs for Anoma transaction functions | ||
type StandardInputs := | ||
mkStandardInputs@{ | ||
caller : Identity; | ||
currentRoot : CommitmentTree.Root; | ||
}; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,23 @@ | ||
module Applib.Trait.Random; | ||
|
||
import Stdlib.Prelude open; | ||
import Anoma.Builtin.System as Builtin; | ||
import Anoma open; | ||
import Mtl open; | ||
|
||
mkPrng (seed : Nat) : PRNG := Builtin.pseudoRandomNumberGeneratorInit seed; | ||
|
||
--- An environment capable of generating random ;ByteArray;s | ||
trait | ||
type Random (M : Type -> Type) := | ||
mkRandom@{ | ||
--- Returns a random ;ByteArray; of the given size | ||
genRandomBytes (numBytes : Nat) : M ByteArray; | ||
}; | ||
|
||
instance | ||
StateT-Random {M : Type -> Type} {{Monad M}} : Random (StateT PRNG M) := | ||
mkRandom@{ | ||
genRandomBytes (n : Nat) : StateT PRNG M ByteArray := | ||
mkStateT (pseudoRandomNumberGeneratorNextBytes n >> pure); | ||
}; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,60 @@ | ||
module Applib.Trait.Tx; | ||
|
||
import Stdlib.Prelude open; | ||
import Anoma open; | ||
import Applib.Data.StandardInputs open; | ||
import BaseLayer.ResourceMachine open; | ||
import Applib.Trait.Random open; | ||
import Mtl open; | ||
|
||
--- An environment used to create Anoma transactions | ||
trait | ||
type Tx (M : Type -> Type) := | ||
mkTx@{ | ||
--- Generates a random ;Nonce; | ||
genRandomNonce : M Nonce; | ||
getStandardInputs : M StandardInputs; | ||
}; | ||
|
||
open Tx public; | ||
|
||
module Private; | ||
--- Concrete implementation of the ;Tx; trait | ||
StandardTx (A : Type) : Type := | ||
StateT PRNG (ReaderT StandardInputs Mtl.Identity) A; | ||
|
||
instance | ||
StandardTx-MonadReaderI | ||
: Reader | ||
StandardInputs | ||
(StateT PRNG (ReaderT StandardInputs Mtl.Identity)) := | ||
mkReader@{ | ||
ask : StandardTx StandardInputs := lift Reader.ask; | ||
local | ||
{A} | ||
(f : StandardInputs -> StandardInputs) | ||
: StandardTx A -> StandardTx A | ||
| (mkStateT st) := mkStateT (st >> Reader.local f); | ||
}; | ||
|
||
instance | ||
StandardTx-Tx : Tx (StateT PRNG (ReaderT StandardInputs Mtl.Identity)) := | ||
mkTx@{ | ||
getStandardInputs : StandardTx StandardInputs := ask; | ||
genRandomNonce : StandardTx Nonce := | ||
do { | ||
bytes <- Random.genRandomBytes 32; | ||
pure (Nonce.from32SizedByteArray bytes); | ||
}; | ||
}; | ||
|
||
runStandardTx' {A} (seed : Nat) (si : StandardInputs) : StandardTx A -> A := | ||
evalState (mkPrng seed) >> runReader si >> Mtl.run; | ||
end; | ||
|
||
open Private using {StandardTx} public; | ||
|
||
--- Run the transaction builder | ||
runTx | ||
(seed : Nat) (si : StandardInputs) : StandardTx Transaction -> Transaction := | ||
evalState (mkPrng seed) >> runReader si >> Mtl.run; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters