Rename Nockma stdlib to anomalib and add RM references

bench2/Benchmark/Nockma/Encoding.hs

@@ -1,20 +1,20 @@
 module Benchmark.Nockma.Encoding where
 
+import Juvix.Compiler.Nockma.AnomaLib (anomaLib)
 import Juvix.Compiler.Nockma.Encoding
 import Juvix.Compiler.Nockma.Language
-import Juvix.Compiler.Nockma.Stdlib (stdlib)
 import Juvix.Prelude.Base
 import Test.Tasty.Bench
 
 jamStdlib :: Natural
-jamStdlib = runJam stdlib
+jamStdlib = runJam anomaLib
 
 bm :: Benchmark
 bm =
   bgroup
     "Jam"
-    [ bench "jam stdlib" $ nf runJam stdlib,
-      bench "cue (jam stdlib)" $ nf runCue jamStdlib
+    [ bench "jam anomaLib" $ nf runJam anomaLib,
+      bench "cue (jam anomaLib)" $ nf runCue jamStdlib
     ]
 
 runJam :: Term Natural -> Natural

runtime/nockma/README.md

@@ -1,11 +1,11 @@
 ## Anoma Resource Machine Standard Library
 
-The file `stdlib.nockma` is obtained from the [Anoma Node repository](https://github.com/anoma/anoma).
+The file `anomalib.nockma` is obtained from the [Anoma Node repository](https://github.com/anoma/anoma).
 
 Follow the compilation instructions for Anoma and run the Elixir interactive
 shell in the root of the Anoma clone:
 
 ```sh
 iex -S mix
-iex(1)> File.write("./stdlib.nockma", Nock.rm_core |> Noun.Format.print)
+iex(1)> File.write("./anomalib.nockma", Nock.rm_core |> Noun.Format.print)
 ```

src/Juvix/Compiler/Nockma/AnomaLib.hs

@@ -0,0 +1,104 @@
+module Juvix.Compiler.Nockma.AnomaLib where
+
+import Data.FileEmbed qualified as FE
+import Juvix.Compiler.Nockma.Translation.FromSource
+import Juvix.Prelude.Base
+
+anomaLib :: Term Natural
+anomaLib =
+  fromRight impossible $
+    parseText $
+      decodeUtf8 $(FE.makeRelativeToProject "runtime/nockma/anomalib.nockma" >>= FE.embedFile)
+
+-- | The anoma lib paths are obtained from the Urbit dojo
+-- * Load the anoma lib file into the Urbit dojo
+-- * Run: `=>  anoma  !=(s)` where s is an anoma lib symbol
+-- eg:
+--      =>  anoma  !=(add)
+--      [9 20 0 15]
+anomaLibPath :: AnomaLib -> Term Natural
+anomaLibPath = \case
+  AnomaLibFunction (AnomaStdlibFunction f) -> case f of
+    StdlibDec -> [nock| [9 342 0 511] |]
+    StdlibAdd -> [nock| [9 20 0 511] |]
+    StdlibSub -> [nock| [9 47 0 511] |]
+    StdlibMul -> [nock| [9 4 0 511] |]
+    StdlibDiv -> [nock| [9 170 0 511] |]
+    StdlibMod -> [nock| [9 46 0 511] |]
+    StdlibLe -> [nock| [9 84 0 511] |]
+    StdlibLt -> [nock| [9 343 0 511] |]
+    -- pow2 is called bex in hoon
+    StdlibPow2 -> [nock| [9 4 0 63] |]
+    -- encode is called jam in hoon
+    StdlibEncode -> [nock| [9 22 0 31] |]
+    -- decode is called cue in hoon
+    StdlibDecode -> [nock| [9 94 0 31] |]
+    -- verifyDetached is called verify-detatched in hoon
+    StdlibVerifyDetached -> [nock| [9 22 0 15] |]
+    StdlibSign -> [nock| [9 10 0 15] |]
+    StdlibSignDetached -> [nock| [9 23 0 15] |]
+    StdlibVerify -> [nock| [9 4 0 15] |]
+    StdlibLengthList -> [nock| [9 1.406 0 255] |]
+    StdlibCurry -> [nock| [9 4 0 255] |]
+    -- sha256 is called shax in hoon
+    StdlibSha256 -> [nock| [9 22 0 7] |]
+    -- Obtained from the urbit dojo using:
+    --
+    -- =>  anoma  !=(~(met block 3))
+    --
+    -- The `3` here is because we want to treat each atom as sequences of 2^3
+    -- bits, i.e bytes.
+    StdlibLengthBytes -> [nock| [8 [9 10 0 63] 9 190 10 [6 7 [0 3] 1 3] 0 2] |]
+    -- Obtained from the urbit dojo using:
+    --
+    -- =>  anoma  !=(~(cat block 3))
+    --
+    -- The `3` here is because we want to treat each atom as sequences of 2^3
+    -- bits, i.e bytes.
+    StdlibCatBytes -> [nock| [8 [9 10 0 63] 9 4 10 [6 7 [0 3] 1 3] 0 2] |]
+    -- Obtained from the urbit dojo using:
+    --
+    -- =>(anoma !=(|=([l=(list @)] (foldr l |=([fst=@ snd=@] (add (~(lsh block 3) 1 snd) fst))))))
+    --
+    -- The `3` here is because we want to shift left in byte = 2^3 bit steps.
+    StdlibFoldBytes ->
+      [nock|
+              [ 8
+                [1 0]
+                [ 1
+                  8
+                  [9 46 0 1.023]
+                  9
+                  2
+                  10
+                  [ 6
+                    [0 14]
+                    7
+                    [0 3]
+                    8
+                    [1 0 0]
+                    [1 8 [9 20 0 8.191] 9 2 10 [6 [7 [0 3] 8 [8 [9 10 0 1.023] 9 90 10 [6 7 [0 3] 1 3] 0 2] 9 2 10 [6 [7 [0 3] 1 1] 0 29] 0 2] 0 28] 0 2]
+                    0
+                    1
+                  ]
+                  0
+                  2
+                ]
+                0
+                1
+              ]
+      |]
+  AnomaLibFunction (AnomaRmFunction f) -> case f of
+    RmCommit -> [nock| [9 94 0 1] |]
+    RmNullify -> [nock| [9 350 0 1] |]
+    RmKind -> [nock| [9 1.492 0 1] |]
+    RmProveLogic -> [nock| [9 342 0 1] |]
+    RmProveAction -> [nock| [9 22 0 1] |]
+    RmDeltaAdd -> [nock| [9 92 0 1] |]
+    RmDeltaSub -> [nock| [9 763 0 1] |]
+    RmResourceDelta -> [nock| [9 343 0 1] |]
+    RmActionDelta -> [nock| [9 4 0 1] |]
+    RmMakeDelta -> [nock| [9 372 0 1] |]
+    RmProveDelta -> [nock| [9 1.535 0 1] |]
+  AnomaLibValue (AnomaRmValue v) -> case v of
+    RmZeroDelta -> [nock| [9 20 0 1] |]

src/Juvix/Compiler/Nockma/AnomaLib/Base.hs

@@ -0,0 +1,128 @@
+module Juvix.Compiler.Nockma.AnomaLib.Base where
+
+import Juvix.Prelude hiding (Atom, Path)
+import Juvix.Prelude.Pretty
+
+data AnomaFunction
+  = AnomaStdlibFunction StdlibFunction
+  | AnomaRmFunction RmFunction
+  deriving stock (Show, Lift, Eq, Generic)
+
+instance Hashable AnomaFunction
+
+instance NFData AnomaFunction
+
+data StdlibFunction
+  = StdlibDec
+  | StdlibAdd
+  | StdlibSub
+  | StdlibMul
+  | StdlibDiv
+  | StdlibMod
+  | StdlibLt
+  | StdlibLe
+  | StdlibPow2
+  | StdlibEncode
+  | StdlibDecode
+  | StdlibVerifyDetached
+  | StdlibSign
+  | StdlibSignDetached
+  | StdlibVerify
+  | StdlibCatBytes
+  | StdlibFoldBytes
+  | StdlibLengthList
+  | StdlibLengthBytes
+  | StdlibCurry
+  | StdlibSha256
+  deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
+
+instance Hashable StdlibFunction
+
+instance NFData StdlibFunction
+
+-- | Anoma Resource Machine client library functions
+data RmFunction
+  = RmCommit
+  | RmNullify
+  | RmKind
+  | RmProveLogic
+  | RmProveAction
+  | RmDeltaAdd
+  | RmDeltaSub
+  | RmResourceDelta
+  | RmActionDelta
+  | RmMakeDelta
+  | RmProveDelta
+  deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
+
+instance Hashable RmFunction
+
+instance NFData RmFunction
+
+newtype AnomaValue
+  = AnomaRmValue RmValue
+  deriving stock (Show, Lift, Eq, Generic)
+
+instance Hashable AnomaValue
+
+instance NFData AnomaValue
+
+-- | Anoma Resource Machine client library values
+data RmValue
+  = RmZeroDelta
+  deriving stock (Show, Lift, Eq, Bounded, Enum, Generic)
+
+instance Hashable RmValue
+
+instance NFData RmValue
+
+data AnomaLib
+  = AnomaLibFunction AnomaFunction
+  | AnomaLibValue AnomaValue
+  deriving stock (Show, Lift, Eq, Generic)
+
+instance Hashable AnomaLib
+
+instance NFData AnomaLib
+
+instance Pretty StdlibFunction where
+  pretty = \case
+    StdlibDec -> "dec"
+    StdlibAdd -> "add"
+    StdlibSub -> "sub"
+    StdlibMul -> "mul"
+    StdlibDiv -> "div"
+    StdlibMod -> "mod"
+    StdlibLt -> "<"
+    StdlibLe -> "<="
+    StdlibPow2 -> "pow2"
+    StdlibEncode -> "encode"
+    StdlibDecode -> "decode"
+    StdlibVerifyDetached -> "verify-detached"
+    StdlibSign -> "sign"
+    StdlibSignDetached -> "sign-detached"
+    StdlibVerify -> "verify"
+    StdlibCatBytes -> "cat"
+    StdlibFoldBytes -> "fold-bytes"
+    StdlibLengthList -> "length-list"
+    StdlibLengthBytes -> "length-bytes"
+    StdlibCurry -> "curry"
+    StdlibSha256 -> "sha256"
+
+instance Pretty RmFunction where
+  pretty = \case
+    RmCommit -> "commit"
+    RmNullify -> "nullify"
+    RmKind -> "kind"
+    RmProveLogic -> "prove-logic"
+    RmProveAction -> "prove-action"
+    RmDeltaAdd -> "delta-add"
+    RmDeltaSub -> "delta-sub"
+    RmResourceDelta -> "resource-delta"
+    RmActionDelta -> "action-delta"
+    RmMakeDelta -> "make-delta"
+    RmProveDelta -> "prove-delta"
+
+instance Pretty RmValue where
+  pretty = \case
+    RmZeroDelta -> "zero-delta"