lorentz 0.12.1 → 0.13.0

raw patch · 50 files changed

+1687/−558 lines, 50 filesdep +cryptonitedep −interpolatePVP ok

version bump matches the API change (PVP)

Dependencies added: cryptonite

Dependencies removed: interpolate

API changes (from Hackage documentation)

Files

• CHANGES.md +40/−3
• README.md +4/−4
• lorentz.cabal +52/−4
• src/Lorentz.hs +1/−0
• src/Lorentz/ADT.hs +9/−12
• src/Lorentz/Address.hs +34/−13
• src/Lorentz/Annotation.hs +10/−10
• src/Lorentz/Arith.hs +214/−97
• src/Lorentz/Base.hs +19/−18
• src/Lorentz/Bytes.hs +9/−11
• src/Lorentz/Coercions.hs +30/−17
• src/Lorentz/Common.hs +1/−1
• src/Lorentz/Constraints/Derivative.hs +2/−2
• src/Lorentz/Constraints/Scopes.hs +12/−10
• src/Lorentz/ContractRegistry.hs +5/−5
• src/Lorentz/Default.hs +4/−4
• src/Lorentz/Doc.hs +6/−6
• src/Lorentz/Empty.hs +1/−1
• src/Lorentz/Entrypoints/Core.hs +5/−5
• src/Lorentz/Entrypoints/Doc.hs +13/−13
• src/Lorentz/Entrypoints/Helpers.hs +6/−6
• src/Lorentz/Entrypoints/Impl.hs +7/−7
• src/Lorentz/Entrypoints/Manual.hs +3/−3
• src/Lorentz/Errors.hs +65/−26
• src/Lorentz/Errors/Numeric/Contract.hs +5/−5
• src/Lorentz/Errors/Numeric/Doc.hs +4/−4
• src/Lorentz/Expr.hs +64/−22
• src/Lorentz/Ext.hs +35/−13
• src/Lorentz/Extensible.hs +7/−7
• src/Lorentz/FixedArith.hs +264/−0
• src/Lorentz/Instr.hs +61/−85
• src/Lorentz/Iso.hs +3/−3
• src/Lorentz/Macro.hs +48/−23
• src/Lorentz/OpSize.hs +4/−4
• src/Lorentz/Pack.hs +6/−6
• src/Lorentz/Polymorphic.hs +37/−4
• src/Lorentz/Print.hs +4/−4
• src/Lorentz/Rebinded.hs +3/−4
• src/Lorentz/Referenced.hs +2/−2
• src/Lorentz/ReferencedByName.hs +8/−8
• src/Lorentz/Run.hs +12/−12
• src/Lorentz/Run/Simple.hs +11/−9
• src/Lorentz/StoreClass.hs +7/−16
• src/Lorentz/StoreClass/Extra.hs +1/−1
• src/Lorentz/Tickets.hs +411/−0
• src/Lorentz/UParam.hs +8/−8
• src/Lorentz/Util/TH.hs +2/−2
• src/Lorentz/Value.hs +81/−19
• src/Lorentz/Wrappable.hs +45/−17
• src/Lorentz/Zip.hs +2/−2

@@ -1,8 +1,44 @@-Unreleased-==========-<!-- Append new entries here -->+<!-- Unreleased: append new entries here -->  +0.13.0+======+* [!915](https://gitlab.com/morley-framework/morley/-/merge_requests/915)+  + Add Fixedpoint arithmetics to lorentz+  + Add additional `NFixed` datatype for natural fixedpoint values+  + Add typeclasses for rounding and casting fixedpoint values+  + Change behavior of lorentz arithmetic operations -+    now type of the result is specified by user.+  + Add `ArithOpHs` instance for `EDiv` instruction+* [!989](https://gitlab.com/morley-framework/morley/-/merge_requests/989)+  Switch from interpolate to home-grown string interpolation module+  + Note this changes the syntax of slices in `md` quasiquoter. Before+  we could use expressions `#{expression}`, now we can only use variable+  names `#{name}`.+* [!909](https://gitlab.com/morley-framework/morley/-/merge_requests/909)+  + Update all instances of `Named` functions with patterns from `Morley.Util.Named`+* [!1000](https://gitlab.com/morley-framework/morley/-/merge_requests/1000)+  Modify the `cloneX` macro to only use `dup`s.+* [!937](https://gitlab.com/morley-framework/morley/-/merge_requests/937)+  Attach source code location to interpreter error messages+  + Changed morley interpreter error type from `MichelsonFailed` to `MichelsonFailureWithStack`+* [!945](https://gitlab.com/morley-framework/morley/-/merge_requests/945)+  + Bump Stackage LTS version from 17.9 to 18.10.+* [!835](https://gitlab.com/morley-framework/morley/-/merge_requests/835)+  + Added `Lorentz.Tickets` module with tickets arithmetics and common helpers.+  + Added `Impossible` error.+  + Added `transferTokensE` and `pairE`.+  + Moved `NonZero` to `Lorentz.Macro`.+  + Updated `Wrappable`:+    + Make separate `Wrappable` and `Unwrappable` typeclasses.+    + Old `Unwrappable` type family renamed to `Unwrappabled`.+    + Weaked permissions to perform some actions for some types.+      May now require `unsafeCoerceWrap` instead of `coerceWrap`.+* [!922](https://gitlab.com/morley-framework/morley/-/merge_requests/922)+  Replace lSignEd22519 with generic lSign+* [!881](https://gitlab.com/morley-framework/morley/-/merge_requests/881)+  + Rename `PrintedValScope` to `UntypedValScope` with related types and functions.+ 0.12.1 ====== * [!879](https://gitlab.com/morley-framework/morley/-/merge_requests/879)@@ -25,6 +61,7 @@   + Add tickets feature.   + Add dupable restriction to `dup`-like instructions and some high-level helpers.     See `dup`'s documentation for notes on how to live in this brand new world.+  + Make `parseNoEnv`, `readValue` and other similar functions accept `MichelsonSource` instead of `FilePath`. * [!838](https://gitlab.com/morley-framework/morley/-/merge_requests/838)   + All unsafe functions and data constructors now contain "unsafe" word     at prefix position. E.g `UnsafeMText`, `unsafeMkAnnotation`.

@@ -15,10 +15,10 @@  Haskell's type checker and automatic type inference facilitate contracts implementation and reduce boilerplate related to types. Adoption of Algebraic Data Types makes work with complex objects safe and convenient.-Later Lorentz contract can be dumped as a plain textual Michelson contract using functions from [`Michelson.Printer`](http://hackage.haskell.org/package/morley/docs/Michelson-Printer.html).+Later Lorentz contract can be dumped as a plain textual Michelson contract using functions from [`Morley.Michelson.Printer`](http://hackage.haskell.org/package/morley/docs/Michelson-Printer.html).  As an addition, you can optimize the transpiled Michelson contract before printing-using functions from [`Michelson.Optimizer`](http://hackage.haskell.org/package/morley/docs/Michelson-Optimizer.html).+using functions from [`Morley.Michelson.Optimizer`](http://hackage.haskell.org/package/morley/docs/Michelson-Optimizer.html). E.g. this optimizer will replace `IF {} {}` with `DROP`. For more possible optimizations please refer to the module mentioned earlier. @@ -109,7 +109,7 @@    Lorentz provides primitives for embedding documentation in the contract code and   functions to produce documentation in Markdown, they can be found in-  [`Lorentz.Doc`](http://hackage.haskell.org/package/lorentz/docs/Lorentz-Doc.html) and [`Michelson.Doc`](http://hackage.haskell.org/package/morley/docs/Michelson-Doc.html) modules.+  [`Lorentz.Doc`](http://hackage.haskell.org/package/lorentz/docs/Lorentz-Doc.html) and [`Morley.Michelson.Doc`](http://hackage.haskell.org/package/morley/docs/Michelson-Doc.html) modules.   Documentation examples can be found [here](https://gitlab.com/morley-framework/morley/-/tree/autodoc/master/autodoc).  <a name="lorentz-example"></a>@@ -200,7 +200,7 @@ <!-- This question should be removed once https://gitlab.com/morley-framework/morley/issues/79 is resolved --> * Q: I added a new parameter case to contract and GHC went mad. -  A: Ensure that your number of entry points does not exceed the limit set in [`Util.TypeTuple.Instances`](http://hackage.haskell.org/package/morley/docs/Util-TypeTuple-Instances.html).+  A: Ensure that your number of entry points does not exceed the limit set in [`Morley.Util.TypeTuple.Instances`](http://hackage.haskell.org/package/morley/docs/Util-TypeTuple-Instances.html).  * Q: I added one more datatype that is used in the contract and GHC reports with errors related      to `Rep` type family.

@@ -1,11 +1,11 @@ cabal-version: 2.0 --- This file has been generated from package.yaml by hpack version 0.34.3.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack  name:           lorentz-version:        0.12.1+version:        0.13.0 synopsis:       EDSL for the Michelson Language description:    Lorentz is a powerful meta-programming tool which allows one to write Michelson contracts directly in Haskell. It has the same instructions as Michelson, but operates on Haskell values and allows one to use Haskell features. category:       Language@@ -57,6 +57,7 @@       Lorentz.Expr       Lorentz.Ext       Lorentz.Extensible+      Lorentz.FixedArith       Lorentz.Instr       Lorentz.Iso       Lorentz.Macro@@ -72,6 +73,7 @@       Lorentz.Run.Simple       Lorentz.StoreClass       Lorentz.StoreClass.Extra+      Lorentz.Tickets       Lorentz.UParam       Lorentz.Util.TH       Lorentz.Value@@ -83,7 +85,53 @@       Paths_lorentz   hs-source-dirs:       src-  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns+  default-extensions:+      AllowAmbiguousTypes+      ApplicativeDo+      BangPatterns+      BlockArguments+      ConstraintKinds+      DataKinds+      DefaultSignatures+      DeriveAnyClass+      DeriveDataTypeable+      DeriveFoldable+      DeriveFunctor+      DeriveGeneric+      DeriveTraversable+      DerivingStrategies+      DerivingVia+      EmptyCase+      FlexibleContexts+      FlexibleInstances+      GADTs+      GeneralizedNewtypeDeriving+      LambdaCase+      MultiParamTypeClasses+      MultiWayIf+      NamedFieldPuns+      NegativeLiterals+      NumericUnderscores+      NumDecimals+      OverloadedLabels+      OverloadedStrings+      PatternSynonyms+      PolyKinds+      QuasiQuotes+      RankNTypes+      RecordWildCards+      RecursiveDo+      ScopedTypeVariables+      StandaloneDeriving+      StrictData+      TemplateHaskell+      TupleSections+      TypeApplications+      TypeFamilies+      TypeOperators+      UndecidableInstances+      UndecidableSuperClasses+      ViewPatterns   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages   build-depends:       aeson-pretty@@ -92,10 +140,10 @@     , bytestring     , constraints >=0.11     , containers+    , cryptonite     , data-default     , first-class-families >=0.5.0.0     , fmt-    , interpolate     , lens     , morley     , morley-prelude >=0.3.0

@@ -23,6 +23,7 @@ import Lorentz.Errors.Numeric as Exports import Lorentz.Expr as Exports import Lorentz.Ext as Exports+import Lorentz.FixedArith as Exports import Lorentz.Instr as Exports import Lorentz.Iso as Exports import Lorentz.Macro as Exports

@@ -37,25 +37,22 @@   , Rec (..)   , (:!)   , (:?)-  , arg-  , argDef-  , argF   ) where  import Data.Constraint ((\\)) import Data.Vinyl.Core (RMap(..), Rec(..)) import GHC.TypeLits (AppendSymbol, Symbol)-import Named (arg, argDef, argF, (:!), (:?))  import Lorentz.Base import Lorentz.Coercions import Lorentz.Constraints-import Michelson.Typed.Haskell.Instr-import Michelson.Typed.Haskell.Value-import Michelson.Typed.Instr-import Util.Label (Label)-import Util.Type (KnownList, type (++))-import Util.TypeTuple+import Morley.Michelson.Typed.Haskell.Instr+import Morley.Michelson.Typed.Haskell.Value+import Morley.Michelson.Typed.Instr+import Morley.Util.Label (Label)+import Morley.Util.Named+import Morley.Util.Type (KnownList, type (++))+import Morley.Util.TypeTuple  -- | Allows field access and modification. type HasField dt fname =@@ -97,7 +94,7 @@   :: forall dt name st.      InstrGetFieldC dt name   => Label name -> dt : st :-> (name :! GetFieldType dt name) : st-toFieldNamed l = toField l # forcedCoerce_+toFieldNamed l = toField l # toNamed l  -- | Extract a field of a datatype, leaving the original datatype on stack. --@@ -264,7 +261,7 @@ -- | Like 'case_', accepts a tuple of clauses, which may be more convenient. -- -- If user is experiencing problems with wierd errors about tuples while using--- this function, he should take look at `Util.TypeTuple.Instances` and ensure+-- this function, he should take look at "Morley.Util.TypeTuple.Instances" and ensure -- that his tuple isn't bigger than generated instances, if so, he should probably -- extend number of generated instances. caseT

@@ -33,6 +33,8 @@   , FutureContract (..)      -- ** Conversions+  , callingAddress+  , callingDefAddress   , callingTAddress   , callingDefTAddress   , ToAddress (..)@@ -57,19 +59,19 @@ import Lorentz.Base import Lorentz.Constraints import qualified Lorentz.Entrypoints.Core as Ep-import Michelson.Typed (ContractRef(..), IsoValue(..))-import qualified Michelson.Typed as M-import Michelson.Typed.Entrypoints (EpAddress(..))-import Tezos.Address (Address)-import Util.Type-import Util.TypeLits+import Morley.Michelson.Typed (ContractRef(..), IsoValue(..))+import qualified Morley.Michelson.Typed as M+import Morley.Michelson.Typed.Entrypoints (EpAddress(..))+import Morley.Tezos.Address (Address)+import Morley.Util.Type+import Morley.Util.TypeLits  -- | Address which remembers the parameter type of the contract it refers to. -- -- It differs from Michelson's @contract@ type because it cannot contain -- entrypoint, and it always refers to entire contract parameter even if this -- contract has explicit default entrypoint.-newtype TAddress p = TAddress { unTAddress :: Address }+newtype TAddress (p :: Type) = TAddress { unTAddress :: Address }   deriving stock (Generic, Show)   deriving newtype (Eq, Ord, Buildable)   deriving anyclass (IsoValue, HasAnnotation)@@ -84,19 +86,38 @@   => TAddress cp   -> Ep.EntrypointRef mname   -> ContractRef (Ep.GetEntrypointArgCustom cp mname)-callingTAddress (TAddress addr) epRef =-  withDict (niceParameterEvi @cp) $-  case Ep.parameterEntrypointCallCustom @cp epRef of-    epc@M.EntrypointCall{} -> ContractRef addr (M.SomeEpc epc)+callingTAddress = callingAddress+{-# DEPRECATED callingTAddress "Use `callingAddress`" #-} --- | Specification of 'callTAddress' to call the default entrypoint.+-- | Specification of 'callingTAddress' to call the default entrypoint. callingDefTAddress   :: forall cp.      (NiceParameterFull cp)   => TAddress cp   -> ContractRef (Ep.GetDefaultEntrypointArg cp) callingDefTAddress taddr = callingTAddress taddr Ep.CallDefault+{-# DEPRECATED callingDefTAddress "Use `callingDefAddress`" #-} +-- | Generalization of 'callingTAddress' to any typed address.+callingAddress+  :: forall cp addr mname.+     (ToTAddress cp addr, NiceParameterFull cp)+  => addr+  -> Ep.EntrypointRef mname+  -> ContractRef (Ep.GetEntrypointArgCustom cp mname)+callingAddress (toTAddress @cp -> TAddress addr) epRef =+  withDict (niceParameterEvi @cp) $+  case Ep.parameterEntrypointCallCustom @cp epRef of+    epc@M.EntrypointCall{} -> ContractRef addr (M.SomeEpc epc)++-- | Generalization of 'callingDefTAddress' to any typed address.+callingDefAddress+  :: forall cp addr.+     (ToTAddress cp addr, NiceParameterFull cp)+  => addr+  -> ContractRef (Ep.GetDefaultEntrypointArg cp)+callingDefAddress addr = callingAddress @cp addr Ep.CallDefault+ -- | Something coercible to 'TAddress cp'. type ToTAddress_ cp addr = (ToTAddress cp addr, ToT addr ~ ToT Address) @@ -193,7 +214,7 @@          ToContractRef arg (TAddress cp) where   toContractRef = callingDefTAddress --- | Convert something from 'ContractAddr' in /Haskell/ world.+-- | Convert something from 'ContractRef' in /Haskell/ world. class FromContractRef (cp :: Type) (contract :: Type) where   fromContractRef :: ContractRef cp -> contract 

@@ -28,19 +28,19 @@ import qualified Data.Text as T import Data.Text.Manipulate (toCamel, toPascal, toSnake) import qualified GHC.Generics as G-import Named (NamedF) -import Michelson.Text-import Michelson.Typed+import Morley.Michelson.Text+import Morley.Michelson.Typed   (BigMap, BigMapId, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, Ticket, ToT,   insertTypeAnn, starNotes)-import Michelson.Typed.Haskell.Value (GValueType)-import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, noAnn, unsafeMkAnnotation)-import Tezos.Address-import Tezos.Core-import Tezos.Crypto-import Util.Text-import Util.TypeLits+import Morley.Michelson.Typed.Haskell.Value (GValueType)+import Morley.Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, noAnn, unsafeMkAnnotation)+import Morley.Tezos.Address+import Morley.Tezos.Core+import Morley.Tezos.Crypto+import Morley.Util.Named+import Morley.Util.Text+import Morley.Util.TypeLits  ---------------------------------------------------------------------------- -- Annotation Customization

@@ -2,101 +2,203 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ --- | Type families from 'Michelson.Typed.Arith' lifted to Haskell types.+-- | Type families from "Morley.Michelson.Typed.Arith" lifted to Haskell types. module Lorentz.Arith   ( ArithOpHs (..)+  , DefArithOp (..)   , UnaryArithOpHs (..)-  , ToIntegerArithOpHs+  , DefUnaryArithOp (..)+  , ToIntegerArithOpHs (..)   ) where +import GHC.TypeLits hiding (Div)+import Prelude hiding (natVal)++import Lorentz.Base import Lorentz.Value-import Michelson.Typed.Arith+import Morley.Michelson.Typed.Arith+import qualified Morley.Michelson.Typed.Instr as M  -- | Lifted 'ArithOp'.-class ( ArithOp aop (ToT n) (ToT m)-      , ToT (ArithResHs aop n m) ~ ArithRes aop (ToT n) (ToT m)-      ) => ArithOpHs (aop :: Type) (n :: Type) (m :: Type) where-  type ArithResHs aop n m :: Type+class ArithOpHs (aop :: Type) (n :: Type) (m :: Type) (r :: Type) where+  evalArithOpHs :: n : m : s :-> r : s+  default evalArithOpHs+    :: ( DefArithOp aop+       , ArithOp aop (ToT n) (ToT m)+       , ToT r ~ ArithRes aop (ToT n) (ToT m)+       )+    => n : m : s :-> r : s+  evalArithOpHs = I (defEvalOpHs @aop) +-- | Helper typeclass that provides default definition of 'evalArithOpHs'.+class DefArithOp aop where+  defEvalOpHs+    :: ( ArithOp aop n m+       , r ~ ArithRes aop n m+       )+    => M.Instr (n : m : s) (r : s)+ -- | Lifted 'UnaryArithOp'.-class ( UnaryArithOp aop (ToT n)-      , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)-      ) => UnaryArithOpHs (aop :: Type) (n :: Type) where+class UnaryArithOpHs (aop :: Type) (n :: Type) where   type UnaryArithResHs aop n :: Type+  evalUnaryArithOpHs :: n : s :-> UnaryArithResHs aop n : s+  default evalUnaryArithOpHs+    :: ( DefUnaryArithOp aop+       , UnaryArithOp aop (ToT n)+       , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)+       )+    => n : s :-> UnaryArithResHs aop n : s+  evalUnaryArithOpHs = I (defUnaryArithOpHs @aop) -class ( ToIntArithOp (ToT n)-      ) =>-      ToIntegerArithOpHs (n :: Type)+-- | Helper typeclass that provides default definition of 'evalUnaryArithOpHs'.+class DefUnaryArithOp aop where+  defUnaryArithOpHs+    :: ( UnaryArithOp aop n+       , r ~ UnaryArithRes aop n+       )+    => M.Instr (n : s) (r : s) -instance ArithOpHs Add Natural Integer where-  type ArithResHs Add Natural Integer = Integer-instance ArithOpHs Add Integer Natural where-  type ArithResHs Add Integer Natural = Integer-instance ArithOpHs Add Natural Natural where-  type ArithResHs Add Natural Natural = Natural-instance ArithOpHs Add Integer Integer where-  type ArithResHs Add Integer Integer = Integer-instance ArithOpHs Add Timestamp Integer where-  type ArithResHs Add Timestamp Integer = Timestamp-instance ArithOpHs Add Integer Timestamp where-  type ArithResHs Add Integer Timestamp = Timestamp-instance ArithOpHs Add Mutez Mutez where-  type ArithResHs Add Mutez Mutez = Mutez-instance ArithOpHs Add Bls12381Fr Bls12381Fr where-  type ArithResHs Add Bls12381Fr Bls12381Fr = Bls12381Fr-instance ArithOpHs Add Bls12381G1 Bls12381G1 where-  type ArithResHs Add Bls12381G1 Bls12381G1 = Bls12381G1-instance ArithOpHs Add Bls12381G2 Bls12381G2 where-  type ArithResHs Add Bls12381G2 Bls12381G2 = Bls12381G2+class ToIntegerArithOpHs (n :: Type) where+  evalToIntOpHs :: n : s :-> Integer : s+  default evalToIntOpHs+    :: (ToIntArithOp (ToT n))+    => n : s :-> Integer : s+  evalToIntOpHs = I M.INT -instance ArithOpHs Sub Natural Integer where-  type ArithResHs Sub Natural Integer = Integer-instance ArithOpHs Sub Integer Natural where-  type ArithResHs Sub Integer Natural = Integer-instance ArithOpHs Sub Natural Natural where-  type ArithResHs Sub Natural Natural = Integer-instance ArithOpHs Sub Integer Integer where-  type ArithResHs Sub Integer Integer = Integer-instance ArithOpHs Sub Timestamp Integer where-  type ArithResHs Sub Timestamp Integer = Timestamp-instance ArithOpHs Sub Timestamp Timestamp where-  type ArithResHs Sub Timestamp Timestamp = Integer-instance ArithOpHs Sub Mutez Mutez where-  type ArithResHs Sub Mutez Mutez = Mutez+instance DefArithOp Add where+  defEvalOpHs = M.ADD+instance DefArithOp Sub where+  defEvalOpHs = M.SUB+instance DefArithOp Mul where+  defEvalOpHs = M.MUL+instance DefArithOp And where+  defEvalOpHs = M.AND+instance DefArithOp Or where+  defEvalOpHs = M.OR+instance DefArithOp Xor where+  defEvalOpHs = M.XOR+instance DefArithOp Lsl where+  defEvalOpHs = M.LSL+instance DefArithOp Lsr where+  defEvalOpHs = M.LSR+instance DefArithOp EDiv where+  defEvalOpHs = M.EDIV+instance DefUnaryArithOp Not where+  defUnaryArithOpHs = M.NOT+instance DefUnaryArithOp Abs where+  defUnaryArithOpHs = M.ABS+instance DefUnaryArithOp Eq' where+  defUnaryArithOpHs = M.EQ+instance DefUnaryArithOp Neq where+  defUnaryArithOpHs = M.NEQ+instance DefUnaryArithOp Lt where+  defUnaryArithOpHs = M.LT+instance DefUnaryArithOp Le where+  defUnaryArithOpHs = M.LE+instance DefUnaryArithOp Gt where+  defUnaryArithOpHs = M.GT+instance DefUnaryArithOp Ge where+  defUnaryArithOpHs = M.GE+instance DefUnaryArithOp Neg where+  defUnaryArithOpHs = M.NEG -instance ArithOpHs Mul Natural Integer where-  type ArithResHs Mul Natural Integer = Integer-instance ArithOpHs Mul Integer Natural where-  type ArithResHs Mul Integer Natural = Integer-instance ArithOpHs Mul Natural Natural where-  type ArithResHs Mul Natural Natural = Natural-instance ArithOpHs Mul Integer Integer where-  type ArithResHs Mul Integer Integer = Integer-instance ArithOpHs Mul Natural Mutez where-  type ArithResHs Mul Natural Mutez = Mutez-instance ArithOpHs Mul Mutez Natural where-  type ArithResHs Mul Mutez Natural = Mutez-instance ArithOpHs Mul Integer Bls12381Fr where-  type ArithResHs Mul Integer Bls12381Fr = Bls12381Fr-instance ArithOpHs Mul Natural Bls12381Fr where-  type ArithResHs Mul Natural Bls12381Fr = Bls12381Fr-instance ArithOpHs Mul Bls12381Fr Integer where-  type ArithResHs Mul Bls12381Fr Integer = Bls12381Fr-instance ArithOpHs Mul Bls12381Fr Natural where-  type ArithResHs Mul Bls12381Fr Natural = Bls12381Fr-instance ArithOpHs Mul Bls12381Fr Bls12381Fr where-  type ArithResHs Mul Bls12381Fr Bls12381Fr = Bls12381Fr-instance ArithOpHs Mul Bls12381G1 Bls12381Fr where-  type ArithResHs Mul Bls12381G1 Bls12381Fr = Bls12381G1-instance ArithOpHs Mul Bls12381G2 Bls12381Fr where-  type ArithResHs Mul Bls12381G2 Bls12381Fr = Bls12381G2-instance Bls12381MulBadOrder Bls12381Fr Bls12381G1 =>-         ArithOpHs Mul Bls12381Fr Bls12381G1 where-  type ArithResHs Mul Bls12381Fr Bls12381G1 = Bls12381G1-instance Bls12381MulBadOrder Bls12381Fr Bls12381G2 =>-         ArithOpHs Mul Bls12381Fr Bls12381G2 where-  type ArithResHs Mul Bls12381Fr Bls12381G2 = Bls12381G2+instance (r ~ Integer) => ArithOpHs Add Natural Integer r+instance (r ~ Integer) => ArithOpHs Add Integer Natural r+instance (r ~ Natural) => ArithOpHs Add Natural Natural r+instance (r ~ Integer) => ArithOpHs Add Integer Integer r+instance (r ~ Timestamp) => ArithOpHs Add Timestamp Integer r+instance (r ~ Timestamp) => ArithOpHs Add Integer Timestamp r+instance (r ~ Mutez) => ArithOpHs Add Mutez Mutez r+instance (r ~ Bls12381Fr) => ArithOpHs Add Bls12381Fr Bls12381Fr r+instance (r ~ Bls12381G1) => ArithOpHs Add Bls12381G1 Bls12381G1 r+instance (r ~ Bls12381G2) => ArithOpHs Add Bls12381G2 Bls12381G2 r +instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Add Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add Natural (Fixed p) r++instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) Integer r+instance (r ~ (NFixed p)) => ArithOpHs Add (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Add Integer (NFixed p) r+instance (r ~ (NFixed p)) => ArithOpHs Add Natural (NFixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Add (NFixed p) (Fixed p) r++instance (r ~ Integer) => ArithOpHs Sub Natural Integer r+instance (r ~ Integer) => ArithOpHs Sub Integer Natural r+instance (r ~ Integer) => ArithOpHs Sub Natural Natural r+instance (r ~ Integer) => ArithOpHs Sub Integer Integer r+instance (r ~ Timestamp) => ArithOpHs Sub Timestamp Integer r+instance (r ~ Integer) => ArithOpHs Sub Timestamp Timestamp r+instance (r ~ Mutez) => ArithOpHs Sub Mutez Mutez r++instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (Fixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Sub Integer (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub Natural (NFixed p) r++instance (r ~ (Fixed p)) => ArithOpHs Sub (Fixed p) (NFixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) r++instance (r ~ Integer) => ArithOpHs Mul Natural Integer r+instance (r ~ Integer) => ArithOpHs Mul Integer Natural r+instance (r ~ Natural) => ArithOpHs Mul Natural Natural r+instance (r ~ Integer) => ArithOpHs Mul Integer Integer r+instance (r ~ Mutez) => ArithOpHs Mul Natural Mutez r+instance (r ~ Mutez) => ArithOpHs Mul Mutez Natural r+instance (r ~ Bls12381Fr) => ArithOpHs Mul Integer Bls12381Fr r+instance (r ~ Bls12381Fr) => ArithOpHs Mul Natural Bls12381Fr r+instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Integer r+instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Natural r+instance (r ~ Bls12381Fr) => ArithOpHs Mul Bls12381Fr Bls12381Fr r+instance (r ~ Bls12381G1) => ArithOpHs Mul Bls12381G1 Bls12381Fr r+instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381G2 Bls12381Fr r+instance (r ~ Bls12381G1) => ArithOpHs Mul Bls12381Fr Bls12381G1 r where+  evalArithOpHs = I (M.SWAP `M.Seq` M.MUL)+instance (r ~ Bls12381G2) => ArithOpHs Mul Bls12381Fr Bls12381G2 r where+  evalArithOpHs = I (M.SWAP `M.Seq` M.MUL)++instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))+instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r+instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r+instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r++instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))+instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))+instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r+instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r+instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r+instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r++instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))+instance (r ~ (a + b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))+instance (r ~ (a + b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))++instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Natural Integer r+instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Integer Natural r+instance (r ~ Maybe (Natural, Natural)) => ArithOpHs EDiv Natural Natural r+instance (r ~ Maybe (Integer, Natural)) => ArithOpHs EDiv Integer Integer r+instance (r ~ Maybe (Natural, Mutez)) => ArithOpHs EDiv Mutez Mutez r+instance (r ~ Maybe (Mutez, Mutez)) => ArithOpHs EDiv Mutez Natural r+++instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r+instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r+ instance UnaryArithOpHs Neg Integer where   type UnaryArithResHs Neg Integer = Integer instance UnaryArithOpHs Neg Natural where@@ -107,30 +209,26 @@   type UnaryArithResHs Neg Bls12381G1 = Bls12381G1 instance UnaryArithOpHs Neg Bls12381G2 where   type UnaryArithResHs Neg Bls12381G2 = Bls12381G2+instance UnaryArithOpHs Neg (Fixed p) where+  type UnaryArithResHs Neg (Fixed p) = (Fixed p)+instance UnaryArithOpHs Neg (NFixed p) where+  type UnaryArithResHs Neg (NFixed p) = (Fixed p) -instance ArithOpHs Or Natural Natural where-  type ArithResHs Or Natural Natural = Natural-instance ArithOpHs Or Bool Bool where-  type ArithResHs Or Bool Bool = Bool -instance ArithOpHs And Integer Natural where-  type ArithResHs And Integer Natural = Natural-instance ArithOpHs And Natural Natural where-  type ArithResHs And Natural Natural = Natural-instance ArithOpHs And Bool Bool where-  type ArithResHs And Bool Bool = Bool+instance (r ~ Natural) => ArithOpHs Or Natural Natural r+instance (r ~ Bool) => ArithOpHs Or Bool Bool r -instance ArithOpHs Xor Natural Natural where-  type ArithResHs Xor Natural Natural = Natural-instance ArithOpHs Xor Bool Bool where-  type ArithResHs Xor Bool Bool = Bool+instance (r ~ Natural) => ArithOpHs And Integer Natural r+instance (r ~ Natural) => ArithOpHs And Natural Natural r+instance (r ~ Bool) => ArithOpHs And Bool Bool r -instance ArithOpHs Lsl Natural Natural where-  type ArithResHs Lsl Natural Natural = Natural+instance (r ~ Natural) => ArithOpHs Xor Natural Natural r+instance (r ~ Bool) => ArithOpHs Xor Bool Bool r -instance ArithOpHs Lsr Natural Natural where-  type ArithResHs Lsr Natural Natural = Natural+instance (r ~ Natural) => ArithOpHs Lsl Natural Natural r where +instance (r ~ Natural) => ArithOpHs Lsr Natural Natural r+ instance UnaryArithOpHs Abs Integer where   type UnaryArithResHs Abs Integer = Natural @@ -143,21 +241,40 @@  instance UnaryArithOpHs Eq' Integer where   type UnaryArithResHs Eq' Integer = Bool+instance UnaryArithOpHs Eq' Natural where+  type UnaryArithResHs Eq' Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Eq'  instance UnaryArithOpHs Neq Integer where   type UnaryArithResHs Neq Integer = Bool+instance UnaryArithOpHs Neq Natural where+  type UnaryArithResHs Neq Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Neq  instance UnaryArithOpHs Lt Integer where   type UnaryArithResHs Lt Integer = Bool+instance UnaryArithOpHs Lt Natural where+  type UnaryArithResHs Lt Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Lt  instance UnaryArithOpHs Gt Integer where   type UnaryArithResHs Gt Integer = Bool+instance UnaryArithOpHs Gt Natural where+  type UnaryArithResHs Gt Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Gt  instance UnaryArithOpHs Le Integer where   type UnaryArithResHs Le Integer = Bool+instance UnaryArithOpHs Le Natural where+  type UnaryArithResHs Le Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Le  instance UnaryArithOpHs Ge Integer where   type UnaryArithResHs Ge Integer = Bool+instance UnaryArithOpHs Ge Natural where+  type UnaryArithResHs Ge Natural = Bool+  evalUnaryArithOpHs = evalToIntOpHs # evalUnaryArithOpHs @Ge  instance ToIntegerArithOpHs Natural+instance ToIntegerArithOpHs (NFixed a) instance ToIntegerArithOpHs Bls12381Fr

@@ -39,21 +39,21 @@ import Fmt (Buildable(..))  import Lorentz.Constraints-import Michelson.ErrorPos (InstrCallStack)-import Michelson.Optimizer (OptimizerConf, optimizeWithConf)-import Michelson.Parser (ParserException, parseExpandValue)-import Michelson.Preprocess (transformBytes, transformStrings)-import Michelson.Text (MText)-import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue, typeCheckingWith)-import Michelson.Typed+import Morley.Micheline (ToExpression(..))+import Morley.Michelson.ErrorPos (InstrCallStack)+import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf)+import Morley.Michelson.Parser (MichelsonSource, ParserException, parseExpandValue)+import Morley.Michelson.Preprocess (transformBytes, transformStrings)+import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended)+import Morley.Michelson.Text (MText)+import Morley.Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue, typeCheckingWith)+import Morley.Michelson.Typed   (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,   rfMerge)-import qualified Michelson.Typed as M (Contract(..))-import qualified Michelson.Untyped as U-import Michelson.Printer.Util (RenderDoc (..), buildRenderDocExtended)-import Morley.Micheline (ToExpression(..))+import qualified Morley.Michelson.Typed as M (Contract(..))+import qualified Morley.Michelson.Untyped as U --- | Alias for instruction which hides inner types representation via 'T'.+-- | Alias for instruction which hides inner types representation via @T@. newtype (inp :: [Type]) :-> (out :: [Type]) = LorentzInstr   { unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)   } deriving newtype (Show, Eq)@@ -140,7 +140,7 @@     --     -- We have to keep it separately, since optimizer is free to destroy     -- documentation blocks.-    -- Also, it is not 'ContractDoc' but Lorentz code because the latter is+    -- Also, it is not 'Lorentz.Doc.ContractDoc' but Lorentz code because the latter is     -- easier to modify.   , cDocumentedCode :: ~(ContractCode cp st)   }@@ -157,7 +157,7 @@ toMichelsonContract :: Contract cp st -> M.Contract (ToT cp) (ToT st) toMichelsonContract = cMichelsonContract --- | An alias for ':'.+-- | An alias for @':@. -- -- We discourage its use as this hinders reading error messages -- (the compiler inserts unnecessary parentheses and indentation).@@ -166,7 +166,7 @@  -- | Function composition for instructions. ----- Note that, unlike Morley's '(:#)' operator, '(#)' is left-associative.+-- Note that, unlike Morley's 'Morley.Michelson.Typed.Instr.:#' operator, '(#)' is left-associative. (#) :: (a :-> b) -> (b :-> c) -> a :-> c I l # I r = I (l `Seq` r) I l # FI r = FI (l `Seq` r)@@ -197,10 +197,11 @@ -- is no such contract at all). parseLorentzValue   :: forall v. KnownValue v-  => Text+  => MichelsonSource+  -> Text   -> Either ParseLorentzError v-parseLorentzValue =-  fmap fromVal . (toTyped <=< first ParseLorentzParseError . parseExpandValue)+parseLorentzValue src =+  fmap fromVal . (toTyped <=< first ParseLorentzParseError . parseExpandValue src)   where     toTyped :: U.Value -> Either ParseLorentzError (Value (ToT v))     toTyped =

@@ -11,7 +11,7 @@   , Packed (..)    , TSignature (..)-  , lSignEd22519+  , lSign    , Hash (..)   , DHashAlgorithm@@ -24,19 +24,19 @@   , Keccak   ) where +import Crypto.Random (MonadRandom) import Fmt (Buildable(..))+import Morley.Util.Markdown import qualified Type.Reflection as Refl-import Util.Markdown  import Lorentz.Annotation import Lorentz.Base import Lorentz.Constraints.Scopes import Lorentz.Doc import Lorentz.Value-import qualified Michelson.Typed as T-import Tezos.Crypto-import qualified Tezos.Crypto.Ed25519 as Ed22519-import qualified Tezos.Crypto.Hash as Crypto+import qualified Morley.Michelson.Typed as T+import Morley.Tezos.Crypto+import qualified Morley.Tezos.Crypto.Hash as Crypto  -- | Everything which is represented as bytes inside. class (KnownValue bs, ToT bs ~ ToT ByteString) => BytesLike bs where@@ -105,11 +105,9 @@   typeDocHaskellRep = concreteTypeDocHaskellRep @(TSignature (MText, Integer))   typeDocMichelsonRep = concreteTypeDocMichelsonRep @(TSignature (MText, Integer)) --- | Sign data using Ed25519 curve.--- TODO [#456]: handle other methods, either all at once (if viable) or each one separately-lSignEd22519 :: BytesLike a => Ed22519.SecretKey -> a -> TSignature a-lSignEd22519 sk (toBytes -> bs) =-  TSignature . SignatureEd25519 $ Ed22519.sign sk bs+-- | Sign data using 'SecretKey'+lSign :: (MonadRandom m, BytesLike a) => SecretKey -> a -> m (TSignature a)+lSign sk (toBytes -> bs) = TSignature <$> sign sk bs  ---------------------------------------------------------------------------- -- Hashes

@@ -17,6 +17,7 @@   , allowCheckedCoerceTo   , allowCheckedCoerce   , coerceUnwrap+  , unsafeCoerceWrap   , coerceWrap   , toNamed   , fromNamed@@ -30,30 +31,32 @@   , fakeCoercing      -- * Re-exports-  , Wrappable (..)+  , Unwrappable (..)+  , Wrappable   ) where  import qualified Data.Coerce as Coerce import Data.Constraint ((\\)) import qualified GHC.Generics as G-import Named (NamedF) import Unsafe.Coerce (unsafeCoerce)  import Lorentz.Address import Lorentz.Base import Lorentz.Bytes import Lorentz.Value-import Lorentz.Wrappable (Wrappable(..))+import Lorentz.Wrappable import Lorentz.Zip-import Michelson.Typed+import Morley.Michelson.Typed+import Morley.Util.Named + ---------------------------------------------------------------------------- -- Unsafe coercions ----------------------------------------------------------------------------  -- | Coercion for Haskell world. ----- We discourage using this function on Lorentz types, consider using 'coerce'+-- We discourage using this function on Lorentz types, consider using 'Data.Coerce.coerce' -- instead. -- One of the reasons forthat is that in Lorentz it's common to declare types as -- newtypes consisting of existing primitives, and @forcedCoerce@ tends to ignore@@ -92,24 +95,34 @@ -- Safe coercions ---------------------------------------------------------------------------- --- | Specialized version of 'coerce_' to wrap into a haskell newtype.+-- | Specialized version of 'forcedCoerce_' to unwrap a haskell newtype.+coerceUnwrap+  :: forall a s. Unwrappable a+  => a : s :-> Unwrappabled a : s+coerceUnwrap = forcedCoerce_++-- | Specialized version of 'forcedCoerce_' to wrap a haskell newtype.+--+-- Works under 'Unwrappable' constraint, thus is not safe.+unsafeCoerceWrap+  :: forall a s. Unwrappable a+  => Unwrappabled a : s :-> a : s+unsafeCoerceWrap = forcedCoerce_++-- | Specialized version of 'forcedCoerce_' to wrap into a haskell newtype.+--+-- Requires 'Wrappable' constraint. coerceWrap   :: forall a s. Wrappable a-  => Unwrappable a : s :-> a : s+  => Unwrappabled a : s :-> a : s coerceWrap = forcedCoerce_ --- | Specialized version of 'coerce_' to unwrap a haskell newtype.-coerceUnwrap-  :: forall a s. Wrappable a-  => a : s :-> Unwrappable a : s-coerceUnwrap = forcedCoerce_- -- | Lift given value to a named value.-toNamed :: Label name -> a : s :-> NamedF Identity a name : s+toNamed :: Label name -> a : s :-> (name :! a) : s toNamed _ = coerceWrap  -- | Unpack named value.-fromNamed :: Label name -> NamedF Identity a name : s :-> a : s+fromNamed :: Label name -> (name :! a) : s :-> a : s fromNamed _ = coerceUnwrap  -- Arbitrary coercions@@ -127,7 +140,7 @@ -- -- For cases when a cast from @a@ to @b@ requires some validation, consider -- rather making a dedicated function which performs the necessary checks and--- then calls @forcedCoerce@.+-- then calls 'forcedCoerce'. class a `CanCastTo` b where   -- | An optional method which helps passing -Wredundant-constraints check.   -- Also, you can set specific implementation for it with specific sanity checks.@@ -193,7 +206,7 @@ instance (CanCastTo a1 a2) =>          CanCastTo (ContractRef a1) (ContractRef a2) -instance (CanCastTo a b, f ~ g) => CanCastTo (NamedF f a n) (NamedF g b m)+instance CanCastTo (f a) (g b) => CanCastTo (NamedF f a n) (NamedF g b m)  instance (CanCastTo a1 a2, CanCastTo b1 b2) =>          CanCastTo (a1, b1) (a2, b2)

@@ -14,7 +14,7 @@ -- -- Note that we cannot make it return @[[Operation], store]@ because -- such entrypoint should've been followed by @pair@, and this is not--- possible if entrypoint implementation ends with 'failWith'.+-- possible if entrypoint implementation ends with 'Lorentz.Instr.failWith'. type Entrypoint param store = '[ param, store ] :-> ContractOut store  -- | Version of 'Entrypoint' which accepts no argument.

@@ -14,8 +14,8 @@  import Lorentz.Constraints.Scopes import Lorentz.Entrypoints.Core-import Michelson.Typed.Haskell.Value-import Michelson.Typed.Scope+import Morley.Michelson.Typed.Haskell.Value+import Morley.Michelson.Typed.Scope  -- | Constraint applied to a whole parameter type. type NiceParameterFull cp = (Typeable cp, ParameterDeclaresEntrypoints cp)

@@ -6,7 +6,7 @@  -- | Scope-related constraints used in Lorentz. ----- This contains constraints from 'Michelson.Typed.Scope' modified for use+-- This contains constraints from "Morley.Michelson.Typed.Scope" modified for use -- in Lorentz. module Lorentz.Constraints.Scopes   ( -- * Grouped constraints@@ -16,7 +16,7 @@   , NiceFullPackedValue   , NicePackedValue   , NiceParameter-  , NicePrintedValue+  , NiceUntypedValue   , NiceStorage   , NiceUnpackedValue   , NiceNoBigMap@@ -27,7 +27,7 @@   , dupableEvi   , nicePackedValueEvi   , niceUnpackedValueEvi-  , nicePrintedValueEvi+  , niceUntypedValueEvi      -- * Individual constraints (internals)   , CanHaveBigMap@@ -43,7 +43,7 @@ import Data.Constraint (evidence, trans, weaken1)  import Lorentz.Annotation (HasAnnotation)-import Michelson.Typed+import Morley.Michelson.Typed  -- We write these constraints as class + instance, rather than -- type aliases, in order to allow their partial application.@@ -68,7 +68,7 @@ -- | Constraint applied to any part of parameter type. -- -- Note that you don't usually apply this constraint to the whole parameter,--- consider using 'Lorentz.Constraints.Derivative.NiceParameterFull' in such case.+-- consider using t'Lorentz.Constraints.Derivative.NiceParameterFull' in such case. -- -- Using this type is justified e.g. when calling another contract, there -- you usually supply an entrypoint argument, not the whole parameter.@@ -87,9 +87,11 @@  type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a) -type NicePrintedValue a = (ProperPrintedValBetterErrors (ToT a), KnownValue a)+type NiceUntypedValue a = (ProperUntypedValBetterErrors (ToT a), KnownValue a) -type NiceComparable n = (Comparable (ToT n), KnownValue n)+-- | Constraint applied to any type, to check if Michelson representation (if exists) of this+-- type is Comparable. In case it is not prints human-readable error message+type NiceComparable n = (ProperNonComparableValBetterErrors (ToT n), KnownValue n, Comparable (ToT n))  type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n)) @@ -117,6 +119,6 @@ niceUnpackedValueEvi =   properUnpackedValEvi @(ToT a) `trans` weaken1 -nicePrintedValueEvi :: forall a. NicePrintedValue a :- PrintedValScope (ToT a)-nicePrintedValueEvi =-  properPrintedValEvi @(ToT a) `trans` weaken1+niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)+niceUntypedValueEvi =+  properUntypedValEvi @(ToT a) `trans` weaken1

@@ -34,12 +34,12 @@ import Lorentz.Doc import Lorentz.Print import Lorentz.Run-import Michelson.Analyzer (analyze)-import Michelson.Printer (printTypedContract)-import Michelson.Typed (IsoValue(..), Notes)-import qualified Michelson.Typed as M (Contract(..)) import Morley.Micheline-import Util.CLI (mkCommandParser)+import Morley.Michelson.Analyzer (analyze)+import Morley.Michelson.Printer (printTypedContract)+import Morley.Michelson.Typed (IsoValue(..), Notes)+import qualified Morley.Michelson.Typed as M (Contract(..))+import Morley.Util.CLI (mkCommandParser)  data ContractInfo =   forall cp st.

@@ -15,8 +15,8 @@ import Lorentz.Instr import Lorentz.Macro import Lorentz.Value-import Util.Named-import Util.TypeLits+import Morley.Util.Named+import Morley.Util.TypeLits  -- | Lorentz version of 'Default'. class LDefault a where@@ -41,8 +41,8 @@ -- We do not provide an instance for 'BigMap' since -- it cannot be checked on emptiness -instance (LDefault a, KnownSymbol n) => LDefault (n :! a) where-  ldef = P.fromLabel .! ldef+instance (LDefault a, KnownSymbol n) => LDefault (NamedF P.Identity a n) where+  ldef = P.fromLabel :! ldef   lIsDef = fromNamed P.fromLabel # lIsDef  instance (LDefault a, LDefault b) => LDefault (a, b) where

@@ -89,12 +89,12 @@ import Lorentz.Constraints import Lorentz.Value import Lorentz.Zip ()-import Michelson.Doc-import Michelson.Optimizer-import Michelson.Printer-import Michelson.Typed hiding (Contract)-import Util.Markdown-import Util.Type+import Morley.Michelson.Doc+import Morley.Michelson.Optimizer+import Morley.Michelson.Printer+import Morley.Michelson.Typed hiding (Contract)+import Morley.Util.Markdown+import Morley.Util.Type  -- | Put a document item. doc :: DocItem di => di -> s :-> s

@@ -22,7 +22,7 @@ import Lorentz.Doc import Lorentz.Errors import Lorentz.Value-import Michelson.Typed.Haskell.Doc+import Morley.Michelson.Typed.Haskell.Doc  -- | Replacement for uninhabited type. {-# DEPRECATED Empty "Use Never type instead" #-}

@@ -54,11 +54,11 @@ import qualified Fcf.Utils as Fcf import Fmt (pretty) -import Michelson.Typed-import qualified Michelson.Untyped as U-import Util.Label-import Util.Type-import Util.TypeLits+import Morley.Michelson.Typed+import qualified Morley.Michelson.Untyped as U+import Morley.Util.Label+import Morley.Util.Type+import Morley.Util.TypeLits  import Lorentz.Annotation (FollowEntrypointFlag(..), HasAnnotation, getAnnotation) import Lorentz.Constraints.Scopes

@@ -62,19 +62,19 @@ import Lorentz.Entrypoints.Core import Lorentz.Entrypoints.Helpers import Lorentz.Entrypoints.Impl-import Michelson.Printer (printTypedValue)-import Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)-import Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue, sing)-import qualified Michelson.Typed as T-import Michelson.Typed.Haskell.Doc-import Michelson.Typed.Haskell.Instr-import qualified Michelson.Untyped as Untyped-import Util.Label (Label)-import Util.Markdown-import Util.Type-import Util.TypeLits-import Util.TypeTuple-import Util.Typeable+import Morley.Michelson.Printer (printTypedValue)+import Morley.Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)+import Morley.Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue, sing)+import qualified Morley.Michelson.Typed as T+import Morley.Michelson.Typed.Haskell.Doc+import Morley.Michelson.Typed.Haskell.Instr+import qualified Morley.Michelson.Untyped as Untyped+import Morley.Util.Label (Label)+import Morley.Util.Markdown+import Morley.Util.Type+import Morley.Util.TypeLits+import Morley.Util.TypeTuple+import Morley.Util.Typeable  -- | Gathers information about single entrypoint. --

@@ -10,12 +10,12 @@   , RequireSumType   ) where -import Michelson.Typed.Haskell-import Michelson.Typed.T-import Michelson.Untyped (EpName, FieldAnn, unsafeMkAnnotation, epNameFromParamAnn)-import Util.Text-import Util.Type-import Util.TypeLits+import Morley.Michelson.Typed.Haskell+import Morley.Michelson.Typed.T+import Morley.Michelson.Untyped (EpName, FieldAnn, epNameFromParamAnn, unsafeMkAnnotation)+import Morley.Util.Text+import Morley.Util.Type+import Morley.Util.TypeLits  ctorNameToAnn :: forall ctor. (KnownSymbol ctor, HasCallStack) => FieldAnn ctorNameToAnn = unsafeMkAnnotation . headToLower $ (symbolValT' @ctor)

@@ -24,14 +24,14 @@ import Fcf (Eval, Exp) import qualified Fcf import qualified GHC.Generics as G-import Util.TypeLits+import Morley.Util.TypeLits  import Lorentz.Value-import Michelson.Typed-import Michelson.Typed.Haskell.Value (GValueType)-import Michelson.Untyped (FieldAnn, unsafeMkAnnotation, noAnn)-import Util.Fcf (type (<|>), Over2, TyEqSing)-import Util.Type+import Morley.Michelson.Typed+import Morley.Michelson.Typed.Haskell.Value (GValueType)+import Morley.Michelson.Untyped (FieldAnn, noAnn, unsafeMkAnnotation)+import Morley.Util.Fcf (Over2, TyEqSing, type (<|>))+import Morley.Util.Type  import Lorentz.Annotation import Lorentz.Entrypoints.Core@@ -65,7 +65,7 @@ -- -- If some entrypoint arguments have custom 'IsoValue' instance, this -- derivation way will not work. As a workaround, you can wrap your--- argument into some primitive (e.g. ':!').+-- argument into some primitive (e.g. t'Lorentz.ADT.:!'). data EpdRecursive instance PlainEntrypointsC EpdRecursive cp => EntrypointsDerivation EpdRecursive cp where   type EpdAllEntrypoints EpdRecursive cp = PlainAllEntrypointsExt EpdRecursive cp

@@ -10,14 +10,14 @@  import Lorentz.Constraints import Lorentz.Entrypoints.Core-import Lorentz.Wrappable (Wrappable)-import Michelson.Typed+import Lorentz.Wrappable+import Morley.Michelson.Typed  -- | Wrap parameter into this to locally assign a way to derive entrypoints for -- it. newtype ParameterWrapper (deriv :: Type) cp = ParameterWrapper { unParameterWraper :: cp }   deriving stock Generic-  deriving anyclass (IsoValue, Wrappable)+  deriving anyclass (IsoValue, Unwrappable, Wrappable)  -- Helper for implementing @instance ParameterHasEntrypoints ParameterWrapper@. data PwDeriv deriv

@@ -15,15 +15,16 @@   , ConstantScope   , isoErrorToVal   , isoErrorFromVal+  , simpleFailUsing   , ErrorHasDoc (..)   , typeDocMdDescriptionReferToError   , isInternalErrorClass    , UnspecifiedError (..)+  , Impossible (..)   , SomeError (..)      -- * General instructions-  , failUsing   , failUnexpected      -- * Custom errors@@ -58,18 +59,19 @@  import Lorentz.Base import Lorentz.Doc+import Lorentz.Ext import Lorentz.Instr hiding (cast) import Lorentz.Value-import Michelson.Text-import Michelson.Typed.Convert (untypeValue)-import Michelson.Typed.Haskell-import Michelson.Typed.Instr-import Michelson.Typed.Scope-import Michelson.Typed.Sing (castM, castSingE)-import Util.Markdown-import Util.Type-import Util.TypeLits-import Util.Typeable+import Morley.Michelson.Text+import Morley.Michelson.Typed.Convert (untypeValue)+import Morley.Michelson.Typed.Haskell+import Morley.Michelson.Typed.Instr+import Morley.Michelson.Typed.Scope+import Morley.Michelson.Typed.Sing (castM, castSingE)+import Morley.Util.Markdown+import Morley.Util.Type+import Morley.Util.TypeLits+import Morley.Util.Typeable  ---------------------------------------------------------------------------- -- IsError@@ -91,6 +93,10 @@   -- | Converts a @Value@ into Haskell error.   errorFromVal :: (SingI t) => Value t -> Either Text e +  -- | Fail with the given Haskell value.+  failUsing :: (IsError e) => e -> s :-> t+  failUsing = simpleFailUsing+ -- | Implementation of 'errorToVal' via 'IsoValue'. isoErrorToVal   :: (KnownError e, IsoValue e)@@ -103,6 +109,16 @@   => Value t -> Either Text e isoErrorFromVal e = fromVal <$> castSingE e +-- | Basic implementation for 'failUsing'.+simpleFailUsing+  :: forall e s t.+     (IsError e)+  => e -> s :-> t+simpleFailUsing err =+  errorToVal err $ \eval ->+    doc (DThrows (Proxy @e)) #+    (FI $ PUSH eval `Seq` FAILWITH)+ class Typeable e => ErrorHasDoc (e :: Type) where   -- | Name of error as it appears in the corresponding section title.   errorDocName :: Text@@ -160,7 +176,7 @@  -- | Use this for internal errors only. ----- "Normal" error scenarios should use the mechanism of custom errors, see below.+-- \"Normal\" error scenarios should use the mechanism of custom errors, see below. instance IsError MText where   errorToVal = isoErrorToVal   errorFromVal = isoErrorFromVal@@ -201,6 +217,35 @@   errorDocHaskellRep = typeDocMdReference (Proxy @()) (WithinParens False) <> "."   errorDocDependencies = typeDocDependencies (Proxy @()) +-- | Use this error when sure that failing at the current position is possible+-- in no curcumstances (including invalid user input or misconfigured storage).+--+-- To use this as error, you have to briefly specify the reason why the error+-- scenario is impossible (experimental feature).+data Impossible (reason :: Symbol) = HasCallStack => Impossible++instance KnownSymbol reason => IsError (Impossible reason) where+  errorToVal Impossible = ($ toVal ())+  errorFromVal = error "Extracting impossible error"++  failUsing err@Impossible =+    justComment codeComment #+    testAssert testDescription "" (push False) #+    simpleFailUsing err+    where+      codeComment = fromString $ "Failure from " <> prettyCallStack callStack+      testDescription =+        "Impossible happened: unexpected " <> symbolValT' @reason <> "\n\+        \At: " <> fromString (prettyCallStack callStack)++instance KnownSymbol reason => ErrorHasDoc (Impossible reason) where+  errorDocName = "Impossible error"+  errorDocMdCause =+    "An impossible error happened.\n\n\+    \If this error occured, contact the contract authors."+  errorDocHaskellRep = typeDocMdReference (Proxy @()) (WithinParens False) <> "."+  errorDocDependencies = typeDocDependencies (Proxy @())+ -- | Type wrapper for an @IsError@. data SomeError = forall e. (IsError e, Eq e) => SomeError e @@ -217,16 +262,6 @@ -- General instructions ---------------------------------------------------------------------------- --- | Fail with the given Haskell value.-failUsing-  :: forall e s t.-     (IsError e)-  => e -> s :-> t-failUsing err =-  errorToVal err $ \eval ->-    doc (DThrows (Proxy @e)) #-    (FI $ PUSH eval `Seq` FAILWITH)- -- | Fail, providing a reference to the place in the code where -- this function is called. --@@ -553,7 +588,7 @@    -- | Clarification of error argument meaning.   ---  -- Provide when it's not obvious, e.g. argument is not named with ':!'.+  -- Provide when it's not obvious, e.g. argument is not named with t'Lorentz.ADT.:!'.   --   -- NOTE: This should /not/ be an entire sentence, rather just the semantic   -- backbone.@@ -657,7 +692,7 @@   See the list of errors below for details.    We distinquish several error classes:-  + #{mdBold $ build ErrClassActionException}: given action cannot be performed with+  + #{errClassActionException}: given action cannot be performed with     regard to the current contract state.      Examples: "insufficient balance", "wallet does not exist".@@ -665,7 +700,7 @@     If you are implementing a middleware, such errors should be propagated to     the client. -  + #{mdBold $ build ErrClassBadArgument}: invalid argument supplied to the entrypoint.+  + #{errClassBadArgument}: invalid argument supplied to the entrypoint.      Examples: entrypoint accepts a natural number from `0-3` range, and you     supply `5`.@@ -673,7 +708,7 @@     If you are implementing a middleware, you should care about not letting     such errors happen. -  + #{mdBold $ build ErrClassContractInternal}: contract-internal error.+  + #{errClassContractInternal}: contract-internal error.      In ideal case, such errors should not take place, but still, make sure     that you are ready to handle them. They can signal either invalid contract@@ -681,3 +716,7 @@      If an internal error is thrown, please report it to the author of this contract.   |]+  where+    errClassActionException  = mdBold $ build ErrClassActionException+    errClassBadArgument      = mdBold $ build ErrClassBadArgument+    errClassContractInternal = mdBold $ build ErrClassContractInternal

@@ -39,10 +39,10 @@  import Lorentz.Base import Lorentz.Errors-import Michelson.Analyzer-import Michelson.FailPattern-import Michelson.Text (MText)-import Michelson.Typed+import Morley.Michelson.Analyzer+import Morley.Michelson.FailPattern+import Morley.Michelson.Text (MText)+import Morley.Michelson.Typed  -- | This is a bidirectional map with correspondence between numeric -- and textual error tags.@@ -126,7 +126,7 @@   where     errorTagMap = buildErrorTagMap $ gatherErrorTags instr --- This function works with 'Michelson.Typed' representation, not with Lorentz.+-- This function works with 'Morley.Michelson.Typed' representation, not with Lorentz. applyErrorTagMapWithExcT ::      HasCallStack   => ErrorTagMap

@@ -28,10 +28,10 @@ import Lorentz.Errors import Lorentz.Errors.Numeric.Contract import Lorentz.Macro-import Michelson.Text (MText)-import Michelson.Typed-import Util.Markdown-import Util.Typeable+import Morley.Michelson.Text (MText)+import Morley.Michelson.Typed+import Morley.Util.Markdown+import Morley.Util.Typeable  -- | Adds a section which explains error tag mapping. data DDescribeErrorTagMap = DDescribeErrorTagMap

@@ -10,11 +10,11 @@ we just need binary instructions in infix notation, not in Polish postfix notation that 'add' and other primitives provide. Compare: ->>> push 1; push 2; push 3; push 4; mul; rsub; add+> push 1; push 2; push 3; push 4; mul; rsub; add  vs ->>> push 1 |+| push 2 |-| push 3 |*| push 4+> push 1 |+| push 2 |-| push 3 |*| push 4  In these expressions each atom is some instruction providing a single value on top of the stack, for example:@@ -87,11 +87,13 @@   , (|<<|)   , (|>>|)   , (|:|)+  , pairE   , (|@|)   , listE+  , transferTokensE   ) where -import Prelude (foldr)+import Prelude (foldr, uncurry)  import Lorentz.Arith import Lorentz.Base@@ -100,7 +102,8 @@ import Lorentz.Macro import Lorentz.Rebinded import Lorentz.Value-import Michelson.Typed.Arith+import Morley.Michelson.Typed.Arith+import Morley.Util.Named  -- | Expression is just an instruction accepting stack @inp@ and producing -- stack @out@ with evaluation result @res@ at the top.@@ -162,22 +165,22 @@ -- | Expressions addition. infixl 6 |+| (|+|)-  :: (ArithOpHs Add a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Add a b)+  :: (ArithOpHs Add a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|+|) = binaryExpr add  -- | Expressions subtraction. infixl 6 |-| (|-|)-  :: (ArithOpHs Sub a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Sub a b)+  :: (ArithOpHs Sub a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|-|) = binaryExpr sub  -- | Expressions multiplication. infixl 7 |*| (|*|)-  :: (ArithOpHs Mul a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Mul a b)+  :: (ArithOpHs Mul a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|*|) = binaryExpr mul  -- | Expressions comparison.@@ -200,8 +203,8 @@ -- | Bitwise/logical @AND@ on expressions. infixl 2 |&| (|&|)-  :: (ArithOpHs And a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs And a b)+  :: (ArithOpHs And a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|&|) = binaryExpr and  -- | Bitwise/logical @OR@ on expressions.@@ -209,36 +212,36 @@ -- In case you find this operator looking weird, see '|.|.|' infixl 1 ||| (|||)-  :: (ArithOpHs Or a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)+  :: (ArithOpHs Or a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|||) = binaryExpr or  -- | An alias for '|||'. infixl 1 |.|.| (|.|.|)-  :: (ArithOpHs Or a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Or a b)+  :: (ArithOpHs Or a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|.|.|) = binaryExpr or  -- | Bitwise/logical @XOR@ on expressions. infixl 3 |^| (|^|)-  :: (ArithOpHs Xor a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Xor a b)+  :: (ArithOpHs Xor a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|^|) = binaryExpr xor  -- | Left shift on expressions. infix 8 |<<| (|<<|)-  :: (ArithOpHs Lsl a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsl a b)+  :: (ArithOpHs Lsl a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|<<|) = binaryExpr lsl  -- | Right shift on expressions. infix 8 |>>| (|>>|)-  :: (ArithOpHs Lsr a b)-  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (ArithResHs Lsr a b)+  :: (ArithOpHs Lsr a b r)+  => Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 r (|>>|) = binaryExpr lsr  -- | 'cons' on expressions.@@ -264,6 +267,45 @@ (|@|) :: Expr s0 s1 a -> Expr s1 s2 b -> Expr s0 s2 (a, b) (|@|) = binaryExpr pair +-- | An alias for '|@|'.+--+-- @+-- trivialContract :: ((), storage) :-> ([Operation], Storage)+-- trivialContract =+--   pairE+--     ( nil+--     , cdr+--     )+-- @+pairE :: (Expr s0 s1 a, Expr s1 s2 b) -> Expr s0 s2 (a, b)+pairE = uncurry (|@|)+ -- | Construct a list given the constructor for each element. listE :: KnownValue a => [Expr s s a] -> Expr s s [a] listE = foldr (\pushElem pushRec -> pushElem # dip pushRec # cons) nil++-- | Version of 'transferTokens' instruction that accepts+-- all the arguments as expressions.+--+-- @+-- transferTokensE+--   ! #arg L.unit+--   ! #amount (push zeroMutez)+--   ! #contract take+--   |:| nil+-- @+--+-- You can provide arguments in arbitrary order, but direction of stack changes+-- flow is fixed: stack change in @arg@ expression affects stack available in+-- @amount@ expression, and stack changes in @amount@ expression affect+-- stack changes in @contract@ expression.+transferTokensE+  :: (NiceParameter p)+  => ("arg" :! Expr s0 s1 p)+  -> ("amount" :! Expr s1 s2 Mutez)+  -> ("contract" :! Expr s2 s3 (ContractRef p))+  -> Expr s0 s3 Operation+transferTokensE (N paramE)+                (N amountE)+                (N contractE) =+  paramE # dip (amountE # dip contractE) # transferTokens

@@ -8,6 +8,10 @@ module Lorentz.Ext   ( stackRef   , printComment+  , justComment+  , comment+  , commentAroundFun+  , commentAroundStmt   , testAssert   , stackType   ) where@@ -16,14 +20,14 @@ import GHC.TypeNats (Nat)  import Lorentz.Base-import Michelson.Typed.Haskell-import Michelson.Typed.Instr-import Util.Peano hiding (Nat)+import Morley.Michelson.Typed.Haskell+import Morley.Michelson.Typed.Instr+import Morley.Util.Peano hiding (Nat)  -- | Include a value at given position on stack into comment produced -- by 'printComment'. ----- >>> stackRef @0+-- > stackRef @0 -- <includes the top of the stack> stackRef   :: forall (gn :: Nat) st n.@@ -33,30 +37,48 @@  -- | Print a comment. It will be visible in tests. ----- >>> printComment "Hello world!"--- >>> printComment $ "On top of the stack I see " <> stackRef @0+-- > printComment "Hello world!"+-- > printComment $ "On top of the stack I see " <> stackRef @0 printComment :: PrintComment (ToTs s) -> s :-> s printComment = I . Ext . PRINT +justComment :: Text -> s :-> s+justComment = comment . JustComment++comment :: CommentType -> s :-> s+comment = I . Ext . COMMENT_ITEM++commentAroundFun :: Text -> (i :-> o) -> (i :-> o)+commentAroundFun funName funBody =+  comment (FunctionStarts funName) #+  funBody #+  comment (FunctionEnds funName)++commentAroundStmt :: Text -> (i :-> o) -> (i :-> o)+commentAroundStmt stmtName stmtBody =+  comment (StatementStarts stmtName) #+  stmtBody #+  comment (StatementEnds stmtName)+ -- | Test an invariant, fail if it does not hold. -- -- This won't be included into production contract and is executed only in tests. testAssert-  :: (SingI (ToTs out), HasCallStack)+  :: (HasCallStack)   => Text -> PrintComment (ToTs inp) -> inp :-> Bool : out -> inp :-> inp-testAssert msg comment = \case-  I instr -> I . Ext . TEST_ASSERT $ TestAssert msg comment instr+testAssert msg comment' = \case+  I instr -> I . Ext . TEST_ASSERT $ TestAssert msg comment' instr   FI _ -> error "test assert branch always fails"  -- | Fix the current type of the stack to be given one. ----- >>> stackType @'[Natural]--- >>> stackType @(Integer : Natural : s)--- >>> stackType @'["balance" :! Integer, "toSpend" :! Integer, BigMap Address Integer]+-- > stackType @'[Natural]+-- > stackType @(Integer : Natural : s)+-- > stackType @'["balance" :! Integer, "toSpend" :! Integer, BigMap Address Integer] -- -- Note that you can omit arbitrary parts of the type. ----- >>> stackType @'["balance" :! Integer, "toSpend" :! _, BigMap _ _]+-- > stackType @'["balance" :! Integer, "toSpend" :! _, BigMap _ _] stackType :: forall s. s :-> s stackType = I Nop 

@@ -70,15 +70,15 @@ import Lorentz.Doc import Lorentz.Instr import Lorentz.Pack-import Michelson.Typed-import Util.Label (Label)-import Util.Markdown-import Util.Type-import Util.TypeLits+import Morley.Michelson.Typed+import Morley.Util.Label (Label)+import Morley.Util.Markdown+import Morley.Util.Type+import Morley.Util.TypeLits  newtype Extensible x = Extensible (Natural, ByteString)   deriving stock (Generic, Eq, Show)-  deriving anyclass (IsoValue, HasAnnotation, Wrappable)+  deriving anyclass (IsoValue, HasAnnotation, Unwrappable)  type ExtVal x = (Generic x, GExtVal x (G.Rep x)) type GetCtors x = GGetCtors (G.Rep x)@@ -113,7 +113,7 @@   :: forall t (n :: Nat) name field s.      (WrapExtC t n name field s)   => Label ("c" `AppendSymbol` name) -> AppendCtorField field s :-> Extensible t ': s-wrapExt _ = packForWrap @field # push (natVal (Proxy @n)) # pair # coerceWrap+wrapExt _ = packForWrap @field # push (natVal (Proxy @n)) # pair # unsafeCoerceWrap  type WrapExtC t n name field s =   ( 'Ctor n name field ~ LookupCtor name (EnumerateCtors (GetCtors t))

@@ -0,0 +1,264 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# LANGUAGE InstanceSigs #-}+-- This option was enabled, because of+{-# OPTIONS_GHC -Wno-orphans #-}++module Lorentz.FixedArith+  ( -- * Lorentz instructions+    Lorentz.FixedArith.div+  , castNFixedToFixed+  , castFixedToNFixed++    -- * Lorentz casts+  , LorentzRounding (..)+  , LorentzFixedCast (..)++  ) where++import Data.Fixed+import qualified GHC.TypeLits as Lit+import Prelude hiding (and, compare, drop, natVal, some, swap)+import qualified Prelude as P++import Lorentz.Arith+import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints.Scopes+import Lorentz.Errors+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Value+import Morley.Michelson.Typed.Arith+import Morley.Michelson.Typed.Scope+++-- | Class that enables support of rounding operations for Lorentz non-integer values+-- Note: Round is implemented using "banker's rounding" strategy, rounding half-way values+-- towards nearest even value+class LorentzRounding a b where+  round_ :: a : s :-> b : s+  ceil_ :: a : s :-> b : s+  floor_ :: a : s :-> b : s++instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where+  round_ = roundingHelper @a @b Round 10+  ceil_ = roundingHelper @a @b Ceil 10+  floor_ = roundingHelper @a @b Floor 10++instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where+  round_ = roundingHelper @a @b Round 2+  ceil_ = roundingHelper @a @b Ceil 2+  floor_ = roundingHelper @a @b Floor 2++instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))+  => LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where+  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed+  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed+  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed++instance (KnownNat a, KnownNat b)+  => LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where+  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed+  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed+  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed++-- | Class that allows casting @Fixed@ values to Integer in vice versa+class LorentzFixedCast a where+  fromFixed :: a : s :-> Integer : s+  toFixed :: Integer : s :-> a : s++instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where+  fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s+  fromFixed = (round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) # forcedCoerce_+  toFixed = let pow :: Integer = 10 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (DecBase a))++instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where+  fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s+  fromFixed = (round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) # forcedCoerce_+  toFixed = let pow :: Integer = 2 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (BinBase a))++instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where+  fromFixed = castNFixedToFixed # fromFixed+  toFixed = toFixed # castFixedToNFixed # assertSome [mt|casting negative value to NFixed|]++-- | Since Michelson doesn't support divide operation, we will use our own to represent+-- divison of Fixed and Rational values+data Div++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 10++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 2++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 10++instance ( KnownNat a+         , KnownNat b+         , KnownNat r+         ) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where+  evalArithOpHs = fixedDivHelper @a @b @r 2+++-- | Operation that represents division of two values with a given result+div+  :: forall r n m s. ArithOpHs Div n m r+  => n : m : s :-> r : s+div = evalArithOpHs @Div+++castNFixedToFixed :: NFixed p : s :-> Fixed p : s+castNFixedToFixed = int # forcedCoerce_++castFixedToNFixed :: Fixed p : s :-> Maybe (NFixed p) : s+castFixedToNFixed = coerceUnwrap # isNat # forcedCoerce_++unsafeCastFixedToNFixed ::  Fixed p : s :-> NFixed p : s+unsafeCastFixedToNFixed = coerceUnwrap # Lorentz.Instr.abs # forcedCoerce_++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Integer 10++instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 10++instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where+  evalArithOpHs = edivHelper @a @Natural 2++instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where+  evalArithOpHs = edivHelper @a @Natural 2++----------------------------------------------------------------------------+-- Helpers+----------------------------------------------------------------------------++data RoundingPattern = Round | Ceil | Floor++roundingHelper+  :: forall a b r1 r2 s.+    ( KnownNat a, KnownNat b+    , FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1)))+    , MichelsonCoercible r1 r2+    , Typeable (Unwrappabled r2)+    , IsoValue (Unwrappabled r2)+    , SingI (ToT (Unwrappabled r1))+    , Unwrappable r2+    , Unwrappable r1+    , ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)+    , ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)+    , ArithOpHs And (Unwrappabled r2) Natural Natural+    , ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))+    , ArithOpHs Mul Integer r1 r1+    )+  => RoundingPattern -> Natural -> (r1 : s :-> r2 : s)+roundingHelper rp base =+  let halfBase :: Natural = base `P.div` 2+      powDifference :: Integer = (Lit.natVal (Proxy @b)) - (Lit.natVal (Proxy @a))+      newPow :: Integer = fromIntegral $ 2 * halfNewPow+      halfNewPow :: Natural = halfBase * (base ^ (Prelude.abs powDifference - 1))+   in case () of+        _ | powDifference == 0 -> (forcedCoerce_ :: (r1 : s :-> r2 : s))+          | powDifference > 0 ->+              push newPow # mul # (forcedCoerce_ :: (r1 : s :-> r2 : s))+          | otherwise ->+              push newPow #+              swap #+              coerceUnwrap # ediv #+              assertSome (Impossible @"Division by zero impossible here") #+              case rp of+                Round ->+                  unpair #+                  swap #+                  push halfNewPow #+                  compare #+                  dup #+                  ifGe0 drop (+                    -- rem >= halfNewPow+                    dip (push (1 :: Natural)) #+                    -- if rem == halfNewPow, check if quot is odd+                    ifEq0 (dupN @2 # and) nop #+                    -- if quot is odd or rem > halfNewPow, add 1 to quot.+                    add+                   )+                Ceil ->+                  unpair #+                  swap #+                  ifNeq0 (push (1 :: Integer) # add) nop+                Floor -> car+              # unsafeCoerceWrap++fixedDivHelper+  :: forall t1 t2 t3 base b1 b2 a r s.+     ( KnownNat t1, KnownNat t2, KnownNat t3+     , Num base, NiceConstant base+     , Unwrappable r, Unwrappable b1, Unwrappable a+     , Unwrappabled a ~ base+     , ArithOpHs Mul base r r+     , ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))+     , IsoValue a, Typeable a+     )+  => base -> (r : b1 : s) :-> (Maybe a : s)+fixedDivHelper base =+  let powA = Lit.natVal (Proxy @t1)+      powB = Lit.natVal (Proxy @t2)+      powR = base ^ (Lit.natVal (Proxy @t3) - 1)+   in+     push powB #+     push powA #+     ifGt (push powR # mul) nop #+     dip coerceUnwrap #+     coerceUnwrap #+     ediv @_ @_ @(Maybe (base, b2)) #+     ifNone (none) (car # unsafeCoerceWrap # some)++edivHelper+  :: forall a base x y r1 r2 m s.+     ( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m+     , UnaryArithOpHs Eq' m, ArithOpHs Mul base y m+     , ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))+     , Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool+     )+  => base -> (x : y : s) :-> (Maybe (r1, r2) : s)+edivHelper base =+  let powA = base ^ (Lit.natVal (Proxy @a))+   in+     swap  #+     push powA #+     mul #+     dup #+     ifEq0 @m (dropN @2 # none)+     (+       swap #+       coerceUnwrap #+       ediv #+       assertSome (Impossible @"Division by zero impossible here") #+       unpair #+       dip unsafeCoerceWrap #+       pair #+       some+     )

@@ -6,10 +6,6 @@  module Lorentz.Instr   ( nop-  , justComment-  , comment-  , commentAroundFun-  , commentAroundStmt   , drop   , dropN   , ConstraintDUPNLorentz@@ -125,13 +121,13 @@   , ReadTicket   , readTicket   , splitTicket+  , splitTicketNamed   , joinTickets   , chainId   , level   , never   , framed   , LorentzFunctor (..)-  , NonZero (..)   ) where  import Prelude hiding@@ -149,40 +145,21 @@ import Lorentz.Polymorphic import Lorentz.Value import Lorentz.Zip-import Michelson.Typed-  (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,-  ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,-  EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), SingI, RemFail(..), SomeEntrypointCallT(..), UpdateN,-  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR,-  sepcName, starNotes)-import Michelson.Typed.Arith-import Michelson.Typed.Haskell.Value-import Util.Peano-import Util.PeanoNatural-import Util.Type+import Morley.Michelson.Typed+  (ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG, ConstraintDUG',+  ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN, EntrypointCallT(..), GetN,+  Instr(..), RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, Value'(..), pattern CAR,+  pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)+import Morley.Michelson.Typed.Arith+import Morley.Michelson.Typed.Haskell.Value+import Morley.Util.Named+import Morley.Util.Peano+import Morley.Util.PeanoNatural+import Morley.Util.Type  nop :: s :-> s nop = I Nop -justComment :: Text -> s :-> s-justComment = comment . JustComment--comment :: CommentType -> s :-> s-comment = I . Ext . COMMENT_ITEM--commentAroundFun :: Text -> (i :-> o) -> (i :-> o)-commentAroundFun funName funBody =-  comment (FunctionStarts funName) #-  funBody #-  comment (FunctionEnds funName)--commentAroundStmt :: Text -> (i :-> o) -> (i :-> o)-commentAroundStmt stmtName stmtBody =-  comment (StatementStarts stmtName) #-  stmtBody #-  comment (StatementEnds stmtName)-- drop :: a : s :-> s drop = I DROP @@ -555,88 +532,87 @@ isNat = I ISNAT  add-  :: ArithOpHs Add n m-  => n : m : s :-> ArithResHs Add n m : s-add = I ADD+  :: ArithOpHs Add n m r+  => n : m : s :-> r : s+add = evalArithOpHs @Add  sub-  :: ArithOpHs Sub n m-  => n : m : s :-> ArithResHs Sub n m : s-sub = I SUB+  :: ArithOpHs Sub n m r+  => n : m : s :-> r : s+sub = evalArithOpHs @Sub  rsub-  :: ArithOpHs Sub n m-  => m : n : s :-> ArithResHs Sub n m : s+  :: ArithOpHs Sub n m r+  => m : n : s :-> r : s rsub = swap # sub  mul-  :: ArithOpHs Mul n m-  => n : m : s :-> ArithResHs Mul n m : s-mul = I MUL+  :: ArithOpHs Mul n m r+  => n : m : s :-> r : s+mul = evalArithOpHs @Mul -ediv :: EDivOpHs n m+ediv :: ArithOpHs EDiv n m r      => n : m : s-     :-> Maybe ((EDivOpResHs n m, EModOpResHs n m)) : s-ediv = I EDIV+     :-> r : s+ediv = evalArithOpHs @EDiv  abs :: UnaryArithOpHs Abs n => n : s :-> UnaryArithResHs Abs n : s-abs = I ABS+abs = evalUnaryArithOpHs @Abs  neg :: UnaryArithOpHs Neg n => n : s :-> UnaryArithResHs Neg n : s-neg = I NEG-+neg = evalUnaryArithOpHs @Neg  lsl-  :: ArithOpHs Lsl n m-  => n : m : s :-> ArithResHs Lsl n m : s-lsl = I LSL+  :: ArithOpHs Lsl n m r+  => n : m : s :-> r : s+lsl = evalArithOpHs @Lsl  lsr-  :: ArithOpHs Lsr n m-  => n : m : s :-> ArithResHs Lsr n m : s-lsr = I LSR+  :: ArithOpHs Lsr n m r+  => n : m : s :-> r : s+lsr = evalArithOpHs @Lsr  or-  :: ArithOpHs Or n m-  => n : m : s :-> ArithResHs Or n m : s-or = I OR+  :: ArithOpHs Or n m r+  => n : m : s :-> r : s+or = evalArithOpHs @Or  and-  :: ArithOpHs And n m-  => n : m : s :-> ArithResHs And n m : s-and = I AND+  :: ArithOpHs And n m r+  => n : m : s :-> r : s+and = evalArithOpHs @And  xor-  :: (ArithOpHs Xor n m)-  => n : m : s :-> ArithResHs Xor n m : s-xor = I XOR+  :: (ArithOpHs Xor n m r)+  => n : m : s :-> r : s+xor = evalArithOpHs @Xor  not :: UnaryArithOpHs Not n => n : s :-> UnaryArithResHs Not n : s-not = I NOT+not = evalUnaryArithOpHs @Not  compare :: NiceComparable n => n : n : s :-> Integer : s compare = I COMPARE  eq0 :: UnaryArithOpHs Eq' n => n : s :-> UnaryArithResHs Eq' n : s-eq0 = I EQ+eq0 = evalUnaryArithOpHs @Eq'  neq0 :: UnaryArithOpHs Neq n => n : s :-> UnaryArithResHs Neq n : s-neq0 = I NEQ+neq0 = evalUnaryArithOpHs @Neq  lt0 :: UnaryArithOpHs Lt n => n : s :-> UnaryArithResHs Lt n : s-lt0 = I LT+lt0 = evalUnaryArithOpHs @Lt  gt0 :: UnaryArithOpHs Gt n => n : s :-> UnaryArithResHs Gt n : s-gt0 = I GT+gt0 = evalUnaryArithOpHs @Gt  le0 :: UnaryArithOpHs Le n => n : s :-> UnaryArithResHs Le n : s-le0 = I LE+le0 = evalUnaryArithOpHs @Le  ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s-ge0 = I GE+ge0 = evalUnaryArithOpHs @Ge  int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s-int = I INT+int = evalToIntOpHs  -- | Get a reference to the current contract. --@@ -820,12 +796,22 @@ ticket :: (NiceComparable a) => a : Natural : s :-> Ticket a : s ticket = I TICKET +-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module. readTicket :: Ticket a : s :-> ReadTicket a : Ticket a : s readTicket = I READ_TICKET +-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module. splitTicket :: Ticket a : (Natural, Natural) : s :-> Maybe (Ticket a, Ticket a) : s splitTicket = I SPLIT_TICKET +-- | Version of 'splitTicket' with entries named.+splitTicketNamed+  :: forall n1 n2 a s.+     Ticket a : (n1 :! Natural, n2 :! Natural) : s+  :-> Maybe (n1 :! Ticket a, n2 :! Ticket a) : s+splitTicketNamed = I SPLIT_TICKET++-- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module. joinTickets :: (Ticket a, Ticket a) : s :-> Maybe (Ticket a) : s joinTickets = I JOIN_TICKETS @@ -881,13 +867,3 @@  instance LorentzFunctor Maybe where   lmap f = ifNone none (f # some)--class NonZero t where-  -- | Retain the value only if it is not zero.-  nonZero :: t : s :-> Maybe t : s--instance NonZero Integer where-  nonZero = dup # eq0 # if_ (drop # none) some--instance NonZero Natural where-  nonZero = dup # int # eq0 # if_ (drop # none) some

@@ -20,10 +20,10 @@ import Lorentz.Default import Lorentz.Instr import Lorentz.Macro-import Util.Label-import Util.Named+import Morley.Util.Label+import Morley.Util.Named --- | Lorentz version of 'Control.Lens.Iso'.+-- | Lorentz version of "Control.Lens.Iso". data LIso a b = LIso   { liTo :: forall s. a : s :-> b : s   , liFrom :: forall s. b : s :-> a : s

@@ -60,6 +60,7 @@   , assertUsing    -- * Syntactic Conveniences+  , ErrInstr   , ConstraintReplaceNLorentz   , ConstraintUpdateNLorentz   , ReplaceN (..)@@ -115,6 +116,7 @@   , non   , non'   , isEmpty+  , NonZero (..)    -- * Buildable utils for additional Morley macros   , buildView@@ -131,9 +133,10 @@ import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+)) import Fmt.Internal.Tuple (TupleF) import qualified GHC.TypeLits as Lit-import GHC.TypeNats (type (-), type (+), type (*))+import GHC.TypeNats (type (*), type (+), type (-)) import qualified GHC.TypeNats as GHC (Nat) +import Lorentz.ADT import Lorentz.Annotation import Lorentz.Arith import Lorentz.Base@@ -145,14 +148,17 @@ import Lorentz.Instr import Lorentz.Polymorphic import Lorentz.Value-import Michelson.Typed (ConstraintDIPN', ConstraintDUG', T)-import Michelson.Typed.Arith-import Michelson.Typed.Haskell.Value-import Michelson.Typed.Scope-import Util.Markdown-import Util.Peano-import Util.Type+import Morley.Michelson.Typed (ConstraintDIPN', ConstraintDUG', T)+import Morley.Michelson.Typed.Arith+import Morley.Michelson.Typed.Haskell.Value+import Morley.Michelson.Typed.Scope+import Morley.Util.Markdown+import Morley.Util.Peano+import Morley.Util.Type +-- $setup+-- >>> :m +Lorentz.Run.Simple Lorentz.Instr+ ---------------------------------------------------------------------------- -- Compare ----------------------------------------------------------------------------@@ -318,6 +324,9 @@ -- Syntactic Conveniences ---------------------------------------------------------------------------- +-- | An instruction that always fails.+type ErrInstr s = forall serr. s :-> serr+ -- | Custom Lorentz macro that drops element with given index -- (starting from 0) from the stack. dropX@@ -331,23 +340,25 @@  class CloneX (n :: Peano) a s where   type CloneXT n a s :: [Type]-  cloneXImpl :: a : s :-> CloneXT n a s+  cloneXImpl :: a : s :-> a : CloneXT n a s+ instance CloneX 'Z a s where-  type CloneXT 'Z a s = a : s+  type CloneXT 'Z a s = s   cloneXImpl = nop+ instance (CloneX n a s, Dupable a) => CloneX ('S n) a s where-  type CloneXT ('S n) a s = a ': CloneXT n a s-  cloneXImpl = dup # dip (cloneXImpl @n)+  type CloneXT ('S n) a s = a : CloneXT n a s+  cloneXImpl = cloneXImpl @n # dup  -- | Duplicate the top of the stack @n@ times. -- -- For example, `cloneX @3` has type `a : s :-> a : a : a : a : s`. cloneX   :: forall (n :: GHC.Nat) a s. CloneX (ToPeano n) a s-  => a : s :-> CloneXT (ToPeano n) a s+  => a : s :-> a : CloneXT (ToPeano n) a s cloneX = cloneXImpl @(ToPeano n) --- | @DUU+P@ macro. For example, `duupX @3` is `DUUUP`, it puts+-- | @DUU+P@ macro. For example, @duupX @3@ is @DUUUP@, it puts -- the 3-rd (starting from 1) element to the top of the stack. -- -- Note that @DUU+P@ has since been added as the @DUP n@ instruction and so this@@ -495,7 +506,7 @@  -- | Insert given element into set. ----- This is a separate function from 'updateMap' because stacks they operate with+-- This is a separate function from 'mapUpdate' because stacks they operate with -- differ in length. setInsert :: NiceComparable e => e : Set e : s :-> Set e : s setInsert = dip (push True) # update@@ -601,14 +612,14 @@ -- | Replaces the nth element (0-indexed) with the result of the given "updating" -- instruction (binary with the return type equal to the second argument) applied -- to the 0th element and the nth element itself.--- For example, `updateN @3 cons` replaces the 3rd element with the result of--- `cons` applied to the topmost element and the 3rd one.--- `updateN @0 instr` is not a valid operation (and it is not implemented).--- `updateN @1 instr` is equivalent to `instr` (and so is implemented).--- `updateN @2 instr` is equivalent to `swap # dip instr` (and so is implemented).--- In all other cases `updateN @n instr` will put the topmost element right above--- the nth one (`dug @(n-1)`) and then apply the function to them in place--- (`dipN @(n-1) instr`).+-- For example, @updateN \@3 cons@ replaces the 3rd element with the result of+-- @cons@ applied to the topmost element and the 3rd one.+-- @updateN \@0 instr@ is not a valid operation (and it is not implemented).+-- @updateN \@1 instr@ is equivalent to @instr@ (and so is implemented).+-- @updateN \@2 instr@ is equivalent to @swap # dip instr@ (and so is implemented).+-- In all other cases @updateN \@n instr@ will put the topmost element right above+-- the nth one (@dug \@(n-1)@) and then apply the function to them in place+-- (@dipN \@(n-1) instr@). updateN :: forall (n :: GHC.Nat) a b (s :: [Type]) (mid :: [Type]) (tail :: [Type]).   ( ConstraintUpdateNLorentz (ToPeano (n - 1)) s a b mid tail   , UpdateN (ToPeano n) s a b mid tail@@ -875,3 +886,17 @@ -- | Check whether container is empty. isEmpty :: SizeOpHs c => c : s :-> Bool : s isEmpty = size # int # eq0++class NonZero t where+  -- | Retain the value only if it is not zero.+  nonZero :: t : s :-> Maybe t : s++instance NonZero Integer where+  nonZero = dup # eq0 # if_ (drop # none) some++instance NonZero Natural where+  nonZero = dup # int # eq0 # if_ (drop # none) some++instance (NiceComparable d) => NonZero (Ticket d) where+  nonZero =+    readTicket # toField #rtAmount # int # eq0 # if_ (drop # none) some

@@ -17,8 +17,8 @@ import Lorentz.Constraints import Lorentz.Run import Lorentz.Value-import Michelson.Typed (OpSize)-import qualified Michelson.Typed as T+import Morley.Michelson.Typed (OpSize)+import qualified Morley.Michelson.Typed as T  -- | Estimate code operation size. contractOpSize :: Contract cp st -> OpSize@@ -30,7 +30,7 @@ -}  -- | Estimate value operation size.-valueOpSize :: forall a. (NicePrintedValue a) => a -> OpSize+valueOpSize :: forall a. (NiceUntypedValue a) => a -> OpSize valueOpSize =   T.valueOpSize . toVal-  \\ nicePrintedValueEvi @a+  \\ niceUntypedValueEvi @a

@@ -18,11 +18,11 @@  import Lorentz.Bytes import Lorentz.Constraints-import Michelson.Interpret.Pack-import Michelson.Interpret.Unpack-import Michelson.Typed import Morley.Micheline (Expression, encodeExpression')-import Tezos.Crypto (blake2b)+import Morley.Michelson.Interpret.Pack+import Morley.Michelson.Interpret.Unpack+import Morley.Michelson.Typed+import Morley.Tezos.Crypto (blake2b)  lPackValueRaw   :: forall a.@@ -53,9 +53,9 @@   lUnpackValueRaw . unPacked  lEncodeValue-  :: forall a. (NicePrintedValue a)+  :: forall a. (NiceUntypedValue a)   => a -> ByteString-lEncodeValue = toBinary' . toVal \\ nicePrintedValueEvi @a+lEncodeValue = toBinary' . toVal \\ niceUntypedValueEvi @a  -- | This function transforms Lorentz values into @script_expr@. --

@@ -4,7 +4,7 @@  {-# LANGUAGE QuantifiedConstraints #-} --- | Type families from 'Michelson.Typed.Polymorphic' lifted to Haskell types.+-- | Type families from "Morley.Michelson.Typed.Polymorphic" lifted to Haskell types. module Lorentz.Polymorphic   ( MemOpHs (..)   , MapOpHs (..)@@ -19,10 +19,11 @@   , IsoMapOpRes   ) where +import Data.Fixed+ import Lorentz.Constraints.Scopes (NiceComparable)-import Michelson.Text-import Michelson.Typed-import Tezos.Core (Mutez)+import Lorentz.Value+import Morley.Michelson.Typed  ---------------------------------------------------------------------------- -- Mirrored from Michelson@@ -172,3 +173,35 @@ instance EDivOpHs Mutez Natural where   type EDivOpResHs Mutez Natural = Mutez   type EModOpResHs Mutez Natural = Mutez++instance (KnownNat a) => EDivOpHs (Fixed (DecBase a)) Integer where+  type EDivOpResHs (Fixed (DecBase a)) Integer = Integer+  type EModOpResHs (Fixed (DecBase a)) Integer = (NFixed (DecBase a))++instance (KnownNat a) => EDivOpHs (Fixed (BinBase a)) Integer where+  type EDivOpResHs (Fixed (BinBase a)) Integer = Integer+  type EModOpResHs (Fixed (BinBase a)) Integer = (NFixed (BinBase a))++instance (KnownNat a) => EDivOpHs (Fixed (DecBase a)) Natural where+  type EDivOpResHs (Fixed (DecBase a)) Natural = Integer+  type EModOpResHs (Fixed (DecBase a)) Natural = (NFixed (DecBase a))++instance (KnownNat a) => EDivOpHs (Fixed (BinBase a)) Natural where+  type EDivOpResHs (Fixed (BinBase a)) Natural = Integer+  type EModOpResHs (Fixed (BinBase a)) Natural = (NFixed (BinBase a))++instance (KnownNat a) => EDivOpHs (NFixed (DecBase a)) Integer where+  type EDivOpResHs (NFixed (DecBase a)) Integer = Integer+  type EModOpResHs (NFixed (DecBase a)) Integer = (NFixed (DecBase a))++instance (KnownNat a) => EDivOpHs (NFixed (BinBase a)) Integer where+  type EDivOpResHs (NFixed (BinBase a)) Integer = Integer+  type EModOpResHs (NFixed (BinBase a)) Integer = (NFixed (BinBase a))++instance (KnownNat a) => EDivOpHs (NFixed (DecBase a)) Natural where+  type EDivOpResHs (NFixed (DecBase a)) Natural = Natural+  type EModOpResHs (NFixed (DecBase a)) Natural = (NFixed (DecBase a))++instance (KnownNat a) => EDivOpHs (NFixed (BinBase a)) Natural where+  type EDivOpResHs (NFixed (BinBase a)) Natural = Natural+  type EModOpResHs (NFixed (BinBase a)) Natural = (NFixed (BinBase a))

@@ -12,16 +12,16 @@  import Lorentz.Constraints import Lorentz.Run-import Michelson.Printer (printTypedContract, printTypedValue)-import Michelson.Typed (toVal)+import Morley.Michelson.Printer (printTypedContract, printTypedValue)+import Morley.Michelson.Typed (toVal)  -- | Pretty-print a Haskell value as Michelson one. printLorentzValue   :: forall v.-    (NicePrintedValue v)+    (NiceUntypedValue v)   => Bool -> v -> LText printLorentzValue forceSingleLine =-  withDict (nicePrintedValueEvi @v) $+  withDict (niceUntypedValueEvi @v) $     printTypedValue forceSingleLine . toVal  -- | Pretty-print a Lorentz contract into Michelson code.

@@ -34,16 +34,15 @@  import Prelude hiding (drop, not, swap, (>>), (>>=)) -import Named ((:!))- import Lorentz.Arith import Lorentz.Base import Lorentz.Coercions import Lorentz.Constraints.Scopes import Lorentz.Instr import Lorentz.Macro-import Michelson.Typed.Arith-import Util.Label (Label)+import Morley.Michelson.Typed.Arith+import Morley.Util.Label (Label)+import Morley.Util.Named  -- | Aliases for '(#)' used by do-blocks. (>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)

@@ -11,7 +11,7 @@ -- one element of each type of stack, and in cases when this does not hold -- (e.g. entrypoint with multiple parameters of the same type), it might be -- a good idea to wrap those types into a newtype or to use primitives from--- 'named' package.+-- @named@ package. -- -- This module is experimental, i.e. everything here should work but may be -- removed in favor of better development practices.@@ -31,7 +31,7 @@ import Lorentz.Constraints import Lorentz.Instr import Lorentz.Value-import Util.Type+import Morley.Util.Type  -- Errors ----------------------------------------------------------------------------

@@ -24,19 +24,19 @@  import Data.Constraint ((\\)) import Data.Singletons (Sing)-import Named (NamedF(..))  import Lorentz.ADT import Lorentz.Base import Lorentz.Coercions import Lorentz.Constraints import Lorentz.Instr-import Michelson.Text-import Michelson.Typed-import Util.Label-import Util.Peano-import Util.Type-import Util.TypeLits+import Morley.Michelson.Text+import Morley.Michelson.Typed+import Morley.Util.Label+import Morley.Util.Named+import Morley.Util.Peano+import Morley.Util.Type+import Morley.Util.TypeLits  -- Errors ----------------------------------------------------------------------------@@ -150,7 +150,7 @@  -- | Version of 'HasNamedVar' for multiple variables. ----- >>> type HasContext = HasNamedVars s ["x" := Integer, "f" := Lambda MText MText]+-- > type HasContext = HasNamedVars s ["x" := Integer, "f" := Lambda MText MText] type family HasNamedVars (s :: [Type]) (vs :: [NamedField]) :: Constraint where   HasNamedVars _ '[] = ()   HasNamedVars s ((n := ty) ': vs) = (HasNamedVar s n ty, HasNamedVars s vs)

@@ -62,14 +62,14 @@ import Lorentz.Doc import Lorentz.Entrypoints import Lorentz.Entrypoints.Doc-import Michelson.Analyzer (AnalyzerRes, analyze)-import Michelson.Interpret-import Michelson.Optimizer (OptimizerConf, optimizeWithConf)-import Michelson.Text (MText)-import Michelson.Typed (Instr(..), IsoValue, IsoValuesStack(..), ToTs, starParamNotes)-import qualified Michelson.Typed as M (Contract(..))-import qualified Michelson.Untyped as U (canonicalEntriesOrder)-import Util.Lens+import Morley.Michelson.Analyzer (AnalyzerRes, analyze)+import Morley.Michelson.Interpret+import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf)+import Morley.Michelson.Text (MText)+import Morley.Michelson.Typed (Instr(..), IsoValue, IsoValuesStack(..), ToTs, starParamNotes)+import qualified Morley.Michelson.Typed as M (Contract(..))+import qualified Morley.Michelson.Untyped as U (canonicalEntriesOrder)+import Morley.Util.Lens  -- | Options to control Lorentz to Michelson compilation. data CompilationOptions = CompilationOptions@@ -170,9 +170,9 @@ -- | Compile a whole contract to Michelson. -- -- Note that compiled contract can be ill-typed in terms of Michelson code--- when some of the compilation options are used (e.g. when 'ccoDisableInitialCast'+-- when some of the compilation options are used (e.g. when 'coDisableInitialCast' -- is @True@, resulted contract can be ill-typed).--- However, compilation with 'defaultContractCompilationOptions' should be valid.+-- However, compilation with 'defaultCompilationOptions' should be valid. compileLorentzContract   :: forall cp st. ContractData cp st -> Contract cp st compileLorentzContract ContractData{..} = Contract{..}@@ -200,7 +200,7 @@   => ContractEnv   -> inp :-> out   -> Rec Identity inp-  -> Either MichelsonFailed (Rec Identity out)+  -> Either MichelsonFailureWithStack (Rec Identity out) interpretLorentzInstr env (compileLorentz -> instr) inp =   fromValStack <$> interpretInstr env instr (toValStack inp) @@ -211,7 +211,7 @@   => ContractEnv   -> Lambda inp out   -> inp-  -> Either MichelsonFailed out+  -> Either MichelsonFailureWithStack out interpretLorentzLambda env instr inp = do   res <- interpretLorentzInstr env instr (Identity inp :& RNil)   let Identity out :& RNil = res

@@ -19,8 +19,8 @@ import Lorentz.Run import Lorentz.Value import Lorentz.Zip-import Michelson.Interpret-import Michelson.Runtime.Dummy (dummyContractEnv)+import Morley.Michelson.Interpret+import Morley.Michelson.Runtime.Dummy (dummyContractEnv)  {- Note about priority: @@ -28,6 +28,9 @@ (which is 1), but less than priority of the most our other operators like '#'. -} +-- $setup+-- >>> :m +Lorentz.Base Lorentz.Instr+ ---------------------------------------------------------------------------- -- Common case ----------------------------------------------------------------------------@@ -40,22 +43,21 @@ -- For testing and demonstration purposes. infixr 2 -$? (-$?) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)-      => (inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailed out+      => (inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailureWithStack out code -$? inp = interpretLorentzLambda dummyContractEnv (unzipInstr # code) inp  -- | Like @'-$?'@, assumes that no failure is possible. ----- For testing and demonstration purposes.------ >>> import Lorentz.Instr+-- For testing and demonstration purposes. Note, that here types of variables are specified, because+-- the result type of arithmetic operations depends on them. -- -- >>> nop -$ 5 -- 5--- >>> sub -$ (3, 2)+-- >>> sub -$ ((3 :: Integer), (2 :: Integer)) -- 1 -- >>> push 9 -$ () -- 9--- >>> add # add -$ ((1, 2), 3)+-- >>> add # add -$ ((1 :: Integer), ((2 :: Integer), (3 :: Integer))) -- 6 infixr 2 -$ (-$) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out, HasCallStack)@@ -69,7 +71,7 @@ -- | Version of (-$?) with arguments flipped. infixl 2 &?- (&?-) :: (ZipInstr inps, IsoValue (ZippedStack inps), IsoValue out)-      => ZippedStack inps -> (inps :-> '[out]) -> Either MichelsonFailed out+      => ZippedStack inps -> (inps :-> '[out]) -> Either MichelsonFailureWithStack out (&?-) = flip (-$?)  -- | Version of (-$) with arguments flipped.

@@ -120,15 +120,10 @@ import Lorentz.Iso import qualified Lorentz.Macro as L import Lorentz.Value-import Michelson.Text (labelToMText)--{- $doctest-setup-->>> import Lorentz.Instr->>> import Lorentz.Value->>> import Lorentz.Run.Simple+import Morley.Michelson.Text (labelToMText) --}+-- $setup+-- >>> :m +Lorentz.Base Lorentz.Instr Lorentz.Run.Simple Morley.Michelson.Text  -- | Open kind for various field references. --@@ -140,7 +135,7 @@  -- | For a type-level field reference - an associated term-level representation. ----- This is similar to 'Sing' + 'SingI' pair but has small differences:+-- This is similar to @singletons@ @Sing@ + @SingI@ pair but has small differences: -- -- * Dedicated to field references, thus term-level thing has 'FieldRefKind' kind. -- * The type of term-level value (@FieldRefObject ty@) determines the kind of@@ -925,7 +920,7 @@     useSubmapValue l2 =       getSubmapValue # L.dip (sopSetField ops2 l2) --- | Utility to 'push' the 'MText' name of and entrypoint from its 'Label'+-- | Utility to 'L.push' the 'MText' name of and entrypoint from its 'Label' pushStEp :: Label name -> s :-> MText : s pushStEp = L.push . labelToMText @@ -1015,14 +1010,10 @@ Examples:  >>> push 5 # stMem this -$ (mempty :: Map Integer MText)-...-... Nothing-...+False  >>> stGetField this # pair -$ (5 :: Integer)-...-... (5, 5)-...+(5,5)  -} this :: SelfRef p

@@ -4,7 +4,7 @@  -- | Some conveniences for "Lorentz.StoreClass" module. ----- This is not part of the umbrella 'Lorentz' module, you have to import+-- This is not part of the umbrella "Lorentz" module, you have to import -- this specially. module Lorentz.StoreClass.Extra   ( (.)

@@ -0,0 +1,411 @@+-- SPDX-FileCopyrightText: 2021 Tocqueville Group+--+-- SPDX-License-Identifier: LicenseRef-MIT-TQ++{-# OPTIONS_GHC -Wno-orphans #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE NoApplicativeDo #-}++{- | Extended support for the tickets feature.++This module has to be imported explicitly, it is not re-exported by "Lorentz".++The primary use case for tickets: authorization tokens for specific actions.+For instance, in @Pause@ entrypoint a contract may accept a ticket, checking+that it is emitted from the administrator address.+The mechanism of tickets is more flexible than 'sender' and 'source' instructions:++* a ticket can be carried through an arbitrary chain of intermediate agents;+* it can permit a limited number of certain actions;+* tickets may have a restricted set of authorized actions.++More details below.++The amount of tokens in a ticket may stand for a number of allowed actions+invocations, in this case accepted tickets are checked to contain just @1@ token.+This semantics makes sense, taking @SPLIT_TICKET@ and @JOIN_TICKETS@ instructions+into account, and also the fact that tickets are not dupable.++One important precaution to be kept in mind is that an emitted ticket must+permit exactly one kind of action in exactly one contract. This way the ticket+emitter can be sure that his ticket cannot be used in an unexpected way.+We see two main approaches to this:++* Make the data carried by the ticket identify the target contract and the+action that is being permitted. The contract has to verify the data in the+ticket.++* Make tickets carry as little data as possible, and instead let the main+authorized entity keep a single tickets emitting contract per target contract+per action (the latter is optional). This way, the burden of separating+tickets' area of applicability lies on that main authorized entity instead of+the target contract, but actions become cheaper.++Some examples of use cases:++* An administrator may emit a ticket that permits some delegate to pause the+  contract.+  In this case, the ticket should carry a description of the pausing+  capability (string or enum value) and permission's expiry time.++  It is also easy to share admin privileges among other participants by+  providing them with a ticket with a very large tokens amount.+  The target contract does not even need to know about many administrators+  being involved.++* A user may wish to delegate some actions to an intermediate service.+  In this case, tickets can serve as signatures made on behalf of the user's+  contract, with replay protection provided out-of-the-box.++  Note that at the moment of writing, implicit addresses cannot serve as ticket+  emitters.++* The allowances mechanism known by FA1.2/FA2 may be replaced with tickets.+  In this case, the tokens amount in a ticket will correspond to the amount of+  tokens that can be spent by an operator.++This module provides helpers to cover the mentioned cases.++-}+module Lorentz.Tickets+  ( -- * Actions authorization+    authorizeAction++    -- * Ticket data verification+  , verifyTargetContract+  , verifyTargetContractAnd++    -- * Tokens spending authorization+  , STicket (..)+  , toSTicket+  , coerceUnwrap++    -- ** Permitted tokens arithmetics+  , readSTicket+  , sTicketAmount+  , subtractSTicket+  , subtractSTicketPlain+  , addSTicket+  , addSTicketPlain++    -- * Generic tickets verification+  , verifyTicketGeneric+  , verifyTicketGeneric'+  , verifyTicketer+  ) where++import Prelude (Generic, Typeable, ($))+import qualified Prelude as P++import Lorentz.ADT+import Lorentz.Annotation+import Lorentz.Base+import Lorentz.Coercions+import Lorentz.Constraints+import Lorentz.Doc+import Lorentz.Errors+import Lorentz.Expr+import Lorentz.Instr+import Lorentz.Macro+import Lorentz.Rebinded+import Lorentz.Value+import Morley.Michelson.Typed.Haskell.Doc+import Morley.Util.Markdown++-- Common errors+----------------------------------------------------------------------------++type instance ErrorArg "wRONG_TICKETER" = NoErrorArg++instance CustomErrorHasDoc "wRONG_TICKETER" where+  customErrClass = ErrClassActionException+  customErrDocMdCause = "Ticket emitted by the wrong entity."++type instance ErrorArg "nOT_TICKET_TARGET" = NoErrorArg++instance CustomErrorHasDoc "nOT_TICKET_TARGET" where+  customErrClass = ErrClassBadArgument+  customErrDocMdCause =+    "Data in the ticket tells that it is intended for a different contract."++type instance ErrorArg "nOT_SINGLE_TICKET_TOKEN" = NoErrorArg++instance CustomErrorHasDoc "nOT_SINGLE_TICKET_TOKEN" where+  customErrClass = ErrClassBadArgument+  customErrDocMdCause =+    "This action expected a ticket with exactly one token."++----------------------------------------------------------------------------+-- Tickets verification+----------------------------------------------------------------------------++-- | Verifies a ticket.+--+-- This is an extremely generified 'verifyTicketGeneric', allows providing+-- verifiers for all the ticket's parts. Provided just in case.+verifyTicketGeneric'+  :: (IsoValue td)+  => (forall s0. Address : Address : s0 :-> s0)+      -- ^ Ticket emitter verifier+  -> (forall s0. Natural : s0 :-> s0)+      -- ^ Ticket tokens verifier+  -> td : s :-> s'+      -- ^ Ticket data verifier+  -> TAddress emitterParam : Ticket td : s :-> Ticket td : s'+verifyTicketGeneric' verifyTicketer' verifyTokens verifyData = do+  dip do+    readTicket; swap; dip deconstruct+  swap; dip @(Ticket _) $ do+    checkedCoerce_; verifyTicketer'+    swap+    verifyTokens+    verifyData++-- | Generic method for verifying tickets that authorize some action.+--+-- For concrete example of use see 'authorizeAction'.+verifyTicketGeneric+  :: (IsoValue td)+  => (forall s0. Natural : s0 :-> s0)  -- ^ Ticket tokens verifier+  -> td : s :-> s'                     -- ^ Ticket data verifier+  -> TAddress emitterParam : Ticket td : s :-> Ticket td : s'+verifyTicketGeneric = verifyTicketGeneric' verifyTicketer++-- | Generic method for verifying the ticketer.+verifyTicketer :: Address : Address : s :-> s+verifyTicketer = if IsEq then nop else failCustomNoArg #wRONG_TICKETER++-- Helpers for checking tickets that remember their target contract+----------------------------------------------------------------------------++-- | Check data in a ticket when it carries target contract address and some+-- other data that is to be verified with the given handler.+verifyTargetContractAnd+  :: (d : s :-> s')+  -> (TAddress selfParam, d) : s :-> s'+verifyTargetContractAnd verifyData = do+  unpair; verifyTargetContract; verifyData++-- | Check data in a ticket when it solely carries target contract address.+verifyTargetContract :: TAddress selfParam : s :-> s+verifyTargetContract =+  if checkedCoerce_ |==| selfAddress+  then nop+  else failCustomNoArg #nOT_TICKET_TARGET++-- Tickets for actions+----------------------------------------------------------------------------++-- | Verifies the given ticket value that permits running an action.+--+-- 1. Ticketer is checked to match the given address.+-- 2. Tokens amount in the ticket is checked to be equal to @1@.+-- 3. Ticket data is checked with the provided handler.+--    In case the data contains target contract, consider using+--    'verifyTargetContract' or 'verifyTargetContractAnd'.+authorizeAction+  :: (IsoValue td)+  => (td : s :-> s')+  -> TAddress emitterParam : Ticket td : s :-> s'+authorizeAction verifyTicketData = do+  verifyTicketGeneric+    verifySingleToken+    verifyTicketData+  drop+  where+    verifySingleToken :: Natural : s :-> s+    verifySingleToken =+      if take |==| push 1+      then nop+      else failCustomNoArg #nOT_SINGLE_TICKET_TOKEN++-- Tickets for tokens+----------------------------------------------------------------------------++-- | A ticket kept in storage.+--+-- The common pattern of use here is+-- 1. A ticket that permits spending few tokens comes in, it is partially+--    validated and this 'STicket' type is produced.+-- 2. This type can repeatedly be used to consume up to the amount of permitted+--    tokens.+--+-- So in order to count allowed tokens, in storage you usually put this type,+-- not bare 'Ticket'.+--+-- The @action@ type parameter serves to distinguish tickets for different+-- actions at type level and usually just matches the value in ticket data:+--+-- * If the data in ticket is validated to be @"pause"@, then the result of+--   validation can be @STicket "pause" ...@; This is the preferred+--   option.+-- * If the data in ticket has enum type, and the value is validated to be+--   some @PauseAction@, then validation can produce+--   @STicket PauseAction ...@.+--+-- CAUTION: when working with this type, you __must__ ensure that the+-- expected ticket emitter (the one you validate tickets against, e.g. admin+-- address) is __constant__ for the lifetime of the 'STicket' value.+-- Otherwise, tickets arithmetics (provided via methods below) won't work.+-- So do one of+--+-- * Either never change the expected ticket emitter;+-- * Or, when it is changed, wipe all the 'STicket' values validated+--   against the old ticketer from storage;+-- * Or keep ticket values in a map where key is the currently expected+--   ticket emitter.+--+-- Note some specificity of this type - its values mostly always appear+-- optionally, either in a map, or in 'Maybe' (this is clear from the+-- potential use cases).+newtype STicket (action :: k) td = STicket (Ticket td)+  deriving stock (Generic)+  deriving anyclass (Unwrappable)++deriving newtype instance+  NiceComparable td =>+  IsoValue (STicket action td)+deriving newtype instance+  (HasAnnotation td, NiceComparable td) =>+  HasAnnotation (STicket action td)++instance (a `CanCastTo` a2, td `CanCastTo` td2) =>+         STicket a td `CanCastTo` STicket a2 td2++instance (NiceComparable d, Typeable k, Typeable action) =>+          NonZero (STicket (action :: k) d) where+  nonZero = do coerceUnwrap; nonZero; lmap unsafeCoerceWrap++instance (Typeable k, Typeable action, TypeHasDoc td) =>+         TypeHasDoc (STicket (action :: k) td) where+  typeDocMdDescription = [md|+    Ticket kept in storage that remembers permissions to spend something.++    The first type argument describes the kind of action or currency that is+    being permitted to perform/spend.+    |]+  typeDocMdReference p =+    customTypeDocMdReference' ("STicket", DType p)+      [ \wp -> mdTicked $ buildTypeWithinParens @action wp+      , typeDocMdReference (P.Proxy @td)+      ]+  typeDocDependencies _ = [dTypeDep @(Ticket Natural)]+  typeDocHaskellRep =+    -- Have to use unsafe version since kinds of @action@ and @"myTokens"@+    -- are different+    unsafeConcreteTypeDocHaskellRep @(STicket "myTokens" Natural)+  typeDocMichelsonRep =+    unsafeConcreteTypeDocMichelsonRep @(STicket "myTokens" Natural)++-- | Constructs an 'STicket'.+--+-- This also emits the ticketer address and ticket data for further use.+-- You are oblidged to do something with both of them:+--+-- * Either validate against the expected value, you can use 'verifyTicketer',+--   'verifyTargetContract' and 'verifyTargetContractAnd' helpers here.+-- * Or use as key in a map where 'STicket' should be put to as a value.+--+-- This way you can be sure that arithmetics on @STickets@ works smoothly+-- and there are no, for instance, attempts to join two tickets from different+-- emitters.+toSTicket+  :: (IsoValue td)+  => Ticket td : s+  :-> Address : td : STicket action td : s+toSTicket = do+  readTicket+  dip unsafeCoerceWrap+  deconstruct+  dipN @2 drop++-- | Read contents of 'STicket'.+readSTicket+  :: STicket action td : s+  :-> ReadTicket td : STicket action td : s+readSTicket = do+  coerceUnwrap; readTicket; dip unsafeCoerceWrap++-- | Read tokens amount in 'STicket'.+sTicketAmount+  :: (IsoValue td)+  => Maybe (STicket action td) : s+  :-> Natural : s+sTicketAmount =+  if IsSome then sTicketAmountPlain else push 0++-- | Version of 'sTicketAmount' that works without @Maybe@.+sTicketAmountPlain+  :: (IsoValue td)+  => STicket action td : s+  :-> Natural : s+sTicketAmountPlain = do+  readSTicket; toField #rtAmount; dip drop++-- | Consume given amount of tokens from the ticket, failing with given handler+-- if amount of tokens in the ticket is insufficient.+--+-- We do not provide a ready error for this case since it will probably depend+-- on particular tokens that the given @STicket@ serves to permit.+--+-- Note that you may want to run @isSome nonZero none@ on the result to save+-- storage space.+subtractSTicket+  :: (IsoValue d, KnownValue (STicket action d))+  => (forall s0. ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))+  -> Natural : Maybe (STicket action d) : s+  :-> Maybe (STicket action d) : s+subtractSTicket onInsufficientTokens = do+  swap+  if IsNone+  then do drop @Natural; none+  else do swap; subtractSTicketPlain onInsufficientTokens; some++-- | Similar to 'subtractSTicket', but without @Maybe@.+--+-- You may want to run 'nonZero' after this function call to save+-- storage space.+subtractSTicketPlain+  :: (IsoValue d)+  => (forall s0. ErrInstr (("permitted" :! Natural, "spent" :! Natural) : s0))+  -> Natural : STicket action d : s+  :-> STicket action d : s+subtractSTicketPlain onInsufficientTokens = do+  toNamed #spent+  dip do+    coerceUnwrap;+    readTicket; toField #rtAmount; toNamed #permitted+  swap; dupTop2+  isNat $: (fromNamed #permitted |-| fromNamed #spent)+  if IsSome+    then do toNamed #remainder; dip $ drop @("permitted" :! _)+    else do pair; onInsufficientTokens+  pair; swap; splitTicketNamed+  assertSome (Impossible @"by construction of token parts")+  car; fromNamed #remainder+  unsafeCoerceWrap++-- | Adds tokens permitted by an incoming ticket.+--+-- Useful when someone permits you to spend even more tokens than you already+-- have been allowed to spend.+--+-- This assumes that the ticket being added has already been verified.+-- The passed tickets must be verified against the same ticket data and ticket+-- emitter.+addSTicket+  :: STicket action d : Maybe (STicket action d) : s+  :-> Maybe (STicket action d) : s+addSTicket = do+  swap; ifSome addSTicketPlain nop; some++-- | Similar to 'addSTicket', but without @Maybe@.+addSTicketPlain+  :: STicket action d : STicket action d : s+  :-> STicket action d : s+addSTicketPlain = do+  coerceUnwrap; dip coerceUnwrap+  pair; joinTickets+  assertSome [mt|badtjoin|]+  unsafeCoerceWrap

@@ -64,13 +64,13 @@ import Lorentz.Instr as L import Lorentz.Macro import Lorentz.Pack-import Michelson.Text-import Michelson.Typed-import Util.Label (Label)-import Util.Markdown-import Util.Type-import Util.TypeLits-import Util.TypeTuple+import Morley.Michelson.Text+import Morley.Michelson.Typed+import Morley.Util.Label (Label)+import Morley.Util.Markdown+import Morley.Util.Type+import Morley.Util.TypeLits+import Morley.Util.TypeTuple  -- | An entrypoint is described by two types: its name and type of argument. type EntrypointKind = (Symbol, Type)@@ -85,7 +85,7 @@ -- to one of entry points from @entries@ list. newtype UParam (entries :: [EntrypointKind]) = UnsafeUParam (MText, ByteString)   deriving stock (Generic, Eq, Show)-  deriving anyclass (IsoValue, HasAnnotation, Wrappable)+  deriving anyclass (IsoValue, HasAnnotation, Unwrappable)  -- Casting to homomorphic value ----------------------------------------------------------------------------

@@ -9,11 +9,11 @@   , typeDoc   ) where -import Prelude hiding (lift) import Data.Text (stripPrefix, stripSuffix) import Language.Haskell.TH-import Language.Haskell.TH.Syntax import Language.Haskell.TH.Quote+import Language.Haskell.TH.Syntax+import Prelude hiding (lift)  import Lorentz.Doc import Lorentz.Entrypoints

@@ -8,9 +8,9 @@ -- defines aliases for constructors of typed values. -- module Lorentz.Value-  ( Value-  , IsoValue (..)-  , WellTypedIsoValue+  ( M.Value+  , M.IsoValue (..)+  , M.WellTypedIsoValue      -- * Primitive types   , Integer@@ -33,7 +33,7 @@   , Set   , Map   , M.BigMapId (..)-  , M.BigMap (..)+  , M.BigMap   , M.mkBigMap   , M.Operation   , Maybe (..)@@ -46,9 +46,15 @@    , M.EpName   , pattern M.DefEpName-  , EntrypointCall-  , SomeEntrypointCall+  , M.EntrypointCall+  , M.SomeEntrypointCall +    -- * Custom datatypes+  , Fixed (..)+  , NFixed (..)+  , DecBase (..)+  , BinBase (..)+     -- * Constructors   , toMutez   , zeroMutez@@ -60,6 +66,8 @@      -- * Conversions   , M.coerceContractRef+  , callingAddress+  , callingDefAddress   , callingTAddress   , callingDefTAddress   , ToAddress (..)@@ -80,20 +88,25 @@  import Data.Constraint ((\\)) import Data.Default (Default(..))+import Data.Fixed (Fixed(..), HasResolution(..))+import GHC.Num+import Prelude hiding (fromInteger)+import qualified Text.Show  import Fmt (Buildable(..))+ import Lorentz.Address import Lorentz.Constraints.Scopes-import Michelson.Text-import Michelson.Typed (EntrypointCall, IsoValue(..), SomeEntrypointCall, Value, WellTypedIsoValue)-import qualified Michelson.Typed as M-import Michelson.Typed.Haskell.Compatibility as ReExports-import Tezos.Core+import Lorentz.Wrappable+import Morley.Michelson.Text+import qualified Morley.Michelson.Typed as M+import Morley.Michelson.Typed.Haskell.Compatibility as ReExports+import Morley.Tezos.Core   (ChainId, Mutez, Timestamp, oneMutez, timestampFromSeconds, timestampFromUTCTime, timestampQuote,   toMutez, zeroMutez)-import Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)-import Util.CustomGeneric as ReExports-import Util.Label (Label(..))+import Morley.Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)+import Morley.Util.CustomGeneric as ReExports+import Morley.Util.Label (Label(..))  import Lorentz.Annotation @@ -101,7 +114,7 @@  data Never   deriving stock (Generic, Show, Eq, Ord)-  deriving anyclass (IsoValue, NFData)+  deriving anyclass (M.IsoValue, NFData)  instance Buildable Never where   build = \case@@ -121,14 +134,63 @@  customGeneric "ReadTicket" rightComb -deriving anyclass instance IsoValue a => IsoValue (ReadTicket a)+deriving anyclass instance M.IsoValue a => M.IsoValue (ReadTicket a)  -- | Provides 'Buildable' instance that prints Lorentz value via Michelson's--- 'Value'.+-- 'M.Value'. -- -- Result won't be very pretty, but this avoids requiring 'Show' or -- 'Buildable' instances. newtype PrintAsValue a = PrintAsValue a -instance NicePrintedValue a => Buildable (PrintAsValue a) where-  build (PrintAsValue a) = build (toVal a) \\ nicePrintedValueEvi @a+instance NiceUntypedValue a => Buildable (PrintAsValue a) where+  build (PrintAsValue a) = build (M.toVal a) \\ niceUntypedValueEvi @a++-- | Datatypes, representing base of the fixed-point values+data DecBase p where+  DecBase :: KnownNat p => DecBase p+data BinBase p where+  BinBase :: KnownNat p => BinBase p++instance KnownNat p => HasResolution (DecBase p) where+  resolution _ = 10 ^ (natVal (Proxy @p))++instance KnownNat p => HasResolution (BinBase p) where+  resolution _ = 2 ^ (natVal (Proxy @p))++-- | Like @Fixed@ but with a @Natural@ value inside constructor+newtype NFixed p = MkNFixed Natural deriving stock (Eq, Ord)++convertNFixedToFixed :: NFixed a -> Fixed a+convertNFixedToFixed (MkNFixed a) = MkFixed (fromIntegral a)++instance (HasResolution a) => Show (NFixed a) where+  show = show . convertNFixedToFixed++-- Note: This instances are copies of those in Data.Fixed for Fixed datatype+instance (HasResolution a) => Num (NFixed a) where+  (MkNFixed a) + (MkNFixed b) = MkNFixed (a + b)+  (MkNFixed a) - (MkNFixed b) = MkNFixed (a - b)+  fa@(MkNFixed a) * (MkNFixed b) = MkNFixed (div (a * b) (fromInteger (resolution fa)))+  negate (MkNFixed a) = MkNFixed (negate a)+  abs = id+  signum (MkNFixed a) = MkNFixed (signum a)+  fromInteger i = withResolution (\res -> MkNFixed ((fromInteger i) * res))++instance (HasResolution a) => Fractional (NFixed a) where+  fa@(MkNFixed a) / (MkNFixed b) = MkNFixed (div (a * (fromInteger (resolution fa))) b)+  recip fa@(MkNFixed a) = MkNFixed (div (res * res) a) where+      res = fromInteger $ resolution fa+  fromRational r = withResolution (\res -> MkNFixed (floor (r * (toRational res))))++instance M.IsoValue (NFixed p) where+  type ToT (NFixed p) = 'M.TNat+  toVal (MkNFixed x) = M.VNat x+  fromVal (M.VNat x) = MkNFixed x++instance Unwrappable (NFixed a) where+  type Unwrappabled (NFixed a) = Natural++-- Helpers copied from Data.Fixed, because they are not exported from there+withResolution :: forall a f. (HasResolution a) => (Natural -> f a) -> f a+withResolution foo = foo . fromInteger . resolution $ Proxy @a

@@ -2,30 +2,58 @@ -- -- SPDX-License-Identifier: LicenseRef-MIT-TQ +-- | Permissions for casts between wrappers and their inner types. module Lorentz.Wrappable-  ( Wrappable-  , Unwrappable+  ( Unwrappable (..)+  , Wrappable   ) where +import Data.Fixed (Fixed(..)) import GHC.Generics import GHC.TypeLits-import Named (NamedF(..)) -import Michelson.Typed (ToT)+import Morley.Michelson.Typed (ToT)+import Morley.Util.Named --- | 'Wrappable' is similar to lens 'Wrapped' class without the method.--- It provides type family that is mainly used as constraint when--- unwrapping Lorentz instruction into a Haskell newtype and vice versa.-class ToT s ~ ToT (Unwrappable s) => Wrappable (s :: Type) where-  type Unwrappable s :: Type-  type Unwrappable s = GUnwrappable (Rep s)+-- | Declares that this type is just a wrapper over some other type+-- and it can be safely unwrapped to that inner type.+--+-- Inspired by lens @Wrapped@.+class ToT s ~ ToT (Unwrappabled s) => Unwrappable (s :: Type) where+  -- | The type we unwrap to (inner type of the newtype).+  --+  -- Used in constraint for Lorentz instruction wrapping into a Haskell newtype+  -- and vice versa.+  type Unwrappabled s :: Type+  type Unwrappabled s = GUnwrappabled s (Rep s) -type family GUnwrappable (rep :: Type -> Type) :: Type where-  GUnwrappable (D1 ('MetaData _ _ _ 'True) (C1 _ (S1 _ (Rec0 a)))) = a-  GUnwrappable _ = TypeError ('Text "Type is not a newtype")+-- | Declares that it is safe to wrap an inner type to the given+-- wrapper type. Can be provided in addition to 'Unwrappable'.+--+-- You can declare this instance when your wrapper exists just to+-- make type system differentiate the two types. Example:+-- @newtype TokenId = TokenId Natural@.+--+-- Do /not/ define this instance for wrappers that provide some invariants.+-- Example: @UStore@ type from @morley-upgradeable@.+--+-- 'Wrappable' is similar to lens @Wrapped@ class without the method.+class Unwrappable s => Wrappable (s :: Type) -instance Wrappable (NamedF Identity a name) where-  type Unwrappable (NamedF Identity a name) = a+type family GUnwrappabled (orig :: Type) (rep :: Type -> Type) :: Type where+  GUnwrappabled _ (D1 ('MetaData _ _ _ 'True) (C1 _ (S1 _ (Rec0 a)))) = a+  GUnwrappabled orig _ =+    TypeError ('Text "Type " ':<>: 'ShowType orig ':<>: 'Text " is not a newtype") -instance Wrappable (NamedF Maybe a name) where-  type Unwrappable (NamedF Maybe a name) = Maybe a+instance Unwrappable (NamedF Identity a name) where+  type Unwrappabled (NamedF Identity a name) = a++instance Wrappable (NamedF Identity a name)++instance Unwrappable (NamedF Maybe a name) where+  type Unwrappabled (NamedF Maybe a name) = Maybe a++instance Wrappable (NamedF Maybe a name)++instance Unwrappable (Fixed a) where+  type Unwrappabled (Fixed a) = Integer

@@ -23,8 +23,8 @@  import Lorentz.Annotation import Lorentz.Base-import Michelson.Typed-import Michelson.Untyped (noAnn)+import Morley.Michelson.Typed+import Morley.Michelson.Untyped (noAnn)  -- | Version of '#' which performs some optimizations immediately. --