wip

src/Juvix/Compiler/Concrete/Data/Builtins.hs

@@ -280,6 +280,8 @@ data BuiltinAxiom
   | BuiltinAnomaRandomSplit
   | BuiltinAnomaIsCommitment
   | BuiltinAnomaIsNullifier
+  | BuiltinAnomaActionCreate
+  | BuiltinAnomaTransactionCompose
   | BuiltinAnomaSet
   | BuiltinAnomaSetToList
   | BuiltinAnomaSetFromList
@@ -350,6 +352,8 @@ instance HasNameKind BuiltinAxiom where
     BuiltinAnomaRandomSplit -> KNameFunction
     BuiltinAnomaIsCommitment -> KNameFunction
     BuiltinAnomaIsNullifier -> KNameFunction
+    BuiltinAnomaActionCreate -> KNameFunction
+    BuiltinAnomaTransactionCompose -> KNameFunction
     BuiltinPoseidon -> KNameFunction
     BuiltinEcOp -> KNameFunction
     BuiltinRandomEcPoint -> KNameFunction
@@ -427,6 +431,8 @@ instance Pretty BuiltinAxiom where
     BuiltinAnomaRandomSplit -> Str.anomaRandomSplit
     BuiltinAnomaIsCommitment -> Str.anomaIsCommitment
     BuiltinAnomaIsNullifier -> Str.anomaIsNullifier
+    BuiltinAnomaTransactionCompose -> Str.anomaTransactionCompose
+    BuiltinAnomaActionCreate -> Str.anomaActionCreate
     BuiltinAnomaSet -> Str.anomaSet
     BuiltinAnomaSetToList -> Str.anomaSetToList
     BuiltinAnomaSetFromList -> Str.anomaSetFromList

src/Juvix/Compiler/Core/Translation/FromInternal.hs

@@ -703,6 +703,8 @@ builtinInductive a =
         Internal.BuiltinAnomaRandomSplit -> Nothing
         Internal.BuiltinAnomaIsCommitment -> Nothing
         Internal.BuiltinAnomaIsNullifier -> Nothing
+        Internal.BuiltinAnomaActionCreate -> Nothing
+        Internal.BuiltinAnomaTransactionCompose -> Nothing
         Internal.BuiltinAnomaSet -> Just (registerInductiveAxiom (Just BuiltinAnomaSet) [])
         Internal.BuiltinAnomaSetToList -> Nothing
         Internal.BuiltinAnomaSetFromList -> Nothing
@@ -1039,6 +1041,22 @@ goAxiomDef a = maybe goAxiomNotBuiltin builtinBody (a ^. Internal.axiomBuiltin)
               natType
               (mkBuiltinApp' OpAnomaIsCommitment [mkVar' 0])
           )
+      Internal.BuiltinAnomaActionCreate -> do
+        registerAxiomDef
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          $ mkBuiltinApp' OpAnomaActionCreate [mkVar' 2, mkVar' 1, mkVar' 0]
+      Internal.BuiltinAnomaTransactionCompose -> do
+        registerAxiomDef
+          . mkLambda'
+            mkDynamic'
+          . mkLambda'
+            mkDynamic'
+          $ mkBuiltinApp' OpAnomaTransactionCompose [mkVar' 1, mkVar' 0]
       Internal.BuiltinAnomaIsNullifier -> do
         natType <- getNatType
         registerAxiomDef
@@ -1518,6 +1536,8 @@ goApplication a = do
         Just Internal.BuiltinAnomaRandomSplit -> app
         Just Internal.BuiltinAnomaIsCommitment -> app
         Just Internal.BuiltinAnomaIsNullifier -> app
+        Just Internal.BuiltinAnomaTransactionCompose -> app
+        Just Internal.BuiltinAnomaActionCreate -> app
         Just Internal.BuiltinAnomaSet -> app
         Just Internal.BuiltinAnomaSetToList -> app
         Just Internal.BuiltinAnomaSetFromList -> app

src/Juvix/Compiler/Core/Translation/Stripped/FromCore.hs

@@ -147,6 +147,8 @@ fromCore' tab =
         BuiltinAnomaRandomSplit -> False
         BuiltinAnomaIsCommitment -> False
         BuiltinAnomaIsNullifier -> False
+        BuiltinAnomaTransactionCompose -> False
+        BuiltinAnomaActionCreate -> False
         BuiltinAnomaSet -> False
         BuiltinAnomaSetToList -> False
         BuiltinAnomaSetFromList -> False

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -1081,6 +1081,8 @@ checkBuiltinAxiom d b = localBuiltins $ case b of
   BuiltinAnomaRandomSplit -> checkAnomaRandomSplit d
   BuiltinAnomaIsCommitment -> checkAnomaIsCommitment d
   BuiltinAnomaIsNullifier -> checkAnomaIsNullifier d
+  BuiltinAnomaActionCreate -> return ()
+  BuiltinAnomaTransactionCompose -> return ()
   BuiltinAnomaSet -> checkAnomaSet d
   BuiltinAnomaSetToList -> checkAnomaSetToList d
   BuiltinAnomaSetFromList -> checkAnomaSetFromList d

test/Anoma.hs

@@ -8,6 +8,6 @@ allTests :: TestTree
 allTests =
   testGroup
     "Anoma tests"
-    [ Compilation.allTests,
-      Client.allTests
+    [ Compilation.allTests
+    -- Client.allTests
     ]

test/Main.hs

@@ -32,37 +32,39 @@ slowTests =
     "Juvix slow tests"
     AllFinish
     <$> sequence
-      [ return Runtime.allTests,
-        return Reg.allTests,
-        return Asm.allTests,
-        return Tree.allTests,
-        return Core.allTests,
-        return Internal.allTests,
-        return Compilation.allTests,
-        return Examples.allTests,
-        Casm.allTests,
-        return Anoma.allTests,
-        return Repl.allTests
+      [ -- return Runtime.allTests,
+        -- return Reg.allTests,
+        -- return Asm.allTests,
+        -- return Tree.allTests,
+        -- return Core.allTests,
+        -- return Internal.allTests,
+        -- return Compilation.allTests,
+        -- return Examples.allTests,
+        -- Casm.allTests,
+        return Anoma.allTests
+        -- return Repl.allTests
       ]
-      <> sequence (if Config.config ^. Config.configRust then [Rust.allTests] else [])
+
+-- <> sequence (if Config.config ^. Config.configRust then [Rust.allTests] else [])
 
 fastTests :: IO TestTree
 fastTests =
   return $
     testGroup
       "Juvix fast tests"
-      [ Parsing.allTests,
-        Resolver.allTests,
-        Scope.allTests,
-        Termination.allTests,
-        Typecheck.allTests,
-        Format.allTests,
-        Formatter.allTests,
-        Package.allTests,
-        BackendMarkdown.allTests,
-        Isabelle.allTests,
-        Nockma.allTests
-      ]
+      []
+
+-- Parsing.allTests,
+-- Resolver.allTests,
+-- Scope.allTests,
+-- Termination.allTests,
+-- Typecheck.allTests,
+-- Format.allTests,
+-- Formatter.allTests,
+-- Package.allTests,
+-- BackendMarkdown.allTests,
+-- Isabelle.allTests,
+-- Nockma.allTests
 
 main :: IO ()
 main = do

tests/Anoma/Compilation/positive/test085/client/ByteArray.juvix

@@ -0,0 +1,38 @@
+module ByteArray;
+
+import Stdlib.Prelude open;
+import Stdlib.Trait.Ord.Eq open using {fromOrdToEq};
+
+module ByteArray;
+  builtin bytearray
+  axiom ByteArray : Type;
+
+  builtin bytearray-from-list-byte
+  axiom mk : List Byte -> ByteArray;
+
+  zero (length : Nat) : ByteArray := mk (replicate length 0x0);
+
+  --- The number of bytes in the ;ByteArray;
+  builtin bytearray-length
+  axiom size : ByteArray -> Nat;
+
+  builtin anoma-bytearray-to-anoma-contents
+  axiom toAnomaContents : ByteArray -> Nat;
+
+  builtin anoma-bytearray-from-anoma-contents
+  axiom fromAnomaContents : Nat -> Nat -> ByteArray;
+end;
+
+open ByteArray using {ByteArray; fromAnomaContents; toAnomaContents} public;
+
+instance
+ByteArray-Ord : Ord ByteArray :=
+  let
+    prod (b : ByteArray) : _ := ByteArray.size b, toAnomaContents b;
+  in Ord.mk@{
+       compare (lhs rhs : ByteArray) : Ordering :=
+         Ord.compare (prod lhs) (prod rhs);
+     };
+
+instance
+ByteArray-Eq : Eq ByteArray := fromOrdToEq;

tests/Anoma/Compilation/positive/test085/client/Encode.juvix

@@ -0,0 +1,39 @@
+module Encode;
+
+import Stdlib.Prelude open;
+
+--- Encodes a value into a natural number.
+builtin anoma-encode
+axiom builtinAnomaEncode
+  : {Value : Type}
+    -- | The value to encode.
+    -> Value
+    -- | The encoded natural number.
+    -> Nat;
+
+--- Decodes a value from a natural number.
+builtin anoma-decode
+axiom builtinAnomaDecode
+  : {Value : Type}
+    -- | The natural number to decode.
+    -> Nat
+    -- | The decoded value.
+    -> Value;
+
+type Encoded A := internalMk Nat
+with
+  coerceFromNat {A} : Nat -> Encoded A := internalMk;
+
+  decode {A} : (encoded : Encoded A) -> A
+    | (internalMk n) := builtinAnomaDecode n;
+
+  encode {A} (obj : A) : Encoded A := internalMk (builtinAnomaEncode obj);
+
+  deriving instance
+  Encoded-Ord {A} : Ord (Encoded A);
+
+  deriving instance
+  Encoded-Eq {A} : Eq (Encoded A);
+end;
+
+open Encoded using {decode; encode} public;

tests/Anoma/Compilation/positive/test085/delta.juvix

@@ -3,42 +3,36 @@ module delta;
 import Stdlib.Prelude open;
 import Stdlib.Debug.Trace open;
 import ResourceMachine open;
+import Encode open;
+import ByteArray open;
 
 main : Delta :=
   let
     resource : Resource :=
-      mkResource@{
-        label := 11;
-        logic := \{_ _ := true};
+      Resource.mk@{
+        label := Label.mk 11;
+        logic := Encoded.encode (Logic.mk \{_ := true});
+        value := AnomaAtom.fromNat 0;
+        nullifierKeyCommitment := NullifierKeyCommitment.zero;
         ephemeral := true;
         quantity := 55;
-        data := 0;
-        nullifier-key := 0;
-        nonce := 0;
-        rseed := 0;
+        nonce := Nonce.fromNat 0;
+        unusedRandSeed := 0;
       };
     action : Action :=
-      mkAction@{
-        commitments := [];
-        nullifiers := [];
-        proofs := [];
-        app-data := 1;
+      Action.create@{
+        consumed := [];
+        created := [];
+        appData := AppData.empty;
       };
-    resCommitment : Nat := commitment resource;
-    resNullifier : Nat := nullifier resource;
+    resCommitment : Commitment := commitment resource;
+    resNullifier : Nullifier := Resource.Transparent.nullifier resource;
   in -- Most of these call return large nouns that are not appropritate for testing.
       -- This test checks that these functions do not crash.
       kind
       resource
-    >-> addDelta (resource-delta resource) (resource-delta resource)
-    >-> addDelta (resource-delta resource) (resource-delta resource)
-    >-> proveDelta zeroDelta
+    >-> addDelta (Action.delta action) (Action.delta action)
     >-> trace (subDelta zeroDelta zeroDelta)
     >-> trace (addDelta zeroDelta zeroDelta)
-    >-> proveAction action
-    >-> trace (actionDelta action)
-    >-> trace (isCommitment resCommitment)
-    >-> trace (isNullifier resNullifier)
-    >-> trace (isCommitment resNullifier)
-    >-> trace (isNullifier resCommitment)
-    >-> actionsDelta [action];
+    >-> trace (Action.delta action)
+    >-> Action.listDelta [action];