diff --git a/Anoma.juvix b/Anoma.juvix
index 7e203c1..19bd487 100644
--- a/Anoma.juvix
+++ b/Anoma.juvix
@@ -2,17 +2,13 @@ module Anoma;
 
 -- import Anoma.Random open public;
 -- import Anoma.Primitives open public;
+import Anoma.Transaction.CustomInputs open public;
 import Anoma.Resource open public;
-import Anoma.Transaction open public;
 import Anoma.Identity open public;
 import Anoma.Builtin.ByteArray open public;
-import Anoma.Generic.ProofRecord open public;
 -- import Anoma.Compliance as Compliance public;
-import Anoma.Logic as Logic public;
 import Anoma.Delta as Delta public;
-import Anoma.Logic open using {Logic} public;
 import Anoma.Delta open using {Delta} public;
--- import Anoma.Logic open using {Logic} public;
 -- import Anoma.Delta open using {Delta} public;
 -- import Anoma.State open public;
 import Anoma.Random open public;
diff --git a/Anoma/Generic/ProofRecord.juvix b/Anoma/Generic/ProofRecord.juvix
deleted file mode 100644
index 02e9523..0000000
--- a/Anoma/Generic/ProofRecord.juvix
+++ /dev/null
@@ -1,13 +0,0 @@
-module Anoma.Generic.ProofRecord;
-
-import Stdlib.Prelude open;
-
-import Anoma.Logic.Types as Logic;
-import Anoma.Delta.Types as Delta;
-import Anoma.Utils open;
-
---- A wrapper type for all of the supported proof record types.
-type ProofRecord :=
-  | ComplianceProofRecord
-  | LogicProofRecord Logic.ProofRecord
-  | DeltaProofRecord;
diff --git a/Anoma/Logic.juvix b/Anoma/Logic.juvix
deleted file mode 100644
index 1d5cf3b..0000000
--- a/Anoma/Logic.juvix
+++ /dev/null
@@ -1,4 +0,0 @@
-module Anoma.Logic;
-
-import Anoma.Logic.Types open public;
-import Anoma.Logic.ProvingSystem open public;
diff --git a/Anoma/Logic/ProvingSystem.juvix b/Anoma/Logic/ProvingSystem.juvix
deleted file mode 100644
index 4f058ae..0000000
--- a/Anoma/Logic/ProvingSystem.juvix
+++ /dev/null
@@ -1,13 +0,0 @@
-module Anoma.Logic.ProvingSystem;
-
-import Anoma.Logic.Types open;
-import BaseLayer.ResourceMachine as B;
-import Anoma.Resource.Object open;
-import Stdlib.Prelude open;
-
-prove
-  (provingKey : ProvingKey)
-  (publicInputs : Instance)
-  (privateInputs : Witness)
-  : Proof :=
-  proofLogic (ProvingKey.unProvingKey provingKey) (publicInputs, privateInputs);
diff --git a/Anoma/Logic/Types.juvix b/Anoma/Logic/Types.juvix
deleted file mode 100644
index d38e996..0000000
--- a/Anoma/Logic/Types.juvix
+++ /dev/null
@@ -1,78 +0,0 @@
-module Anoma.Logic.Types;
-
-import Anoma.Resource.Object open using {Resource};
-import Anoma.Resource.Tag open;
-import Anoma.Resource.Computable open;
-import Stdlib.Prelude open;
-import Stdlib.Debug open;
-
-import BaseLayer.ResourceMachine as B;
-
-open B using {
-  Proof;
-  LogicProof;
-  ComplianceProof;
-  mkProofCompliance;
-  proofLogic;
-  proofCompliance;
-} public;
-
-open B using {
-  Instance;
-  mkInstance;
-  module Instance;
-  Witness;
-  mkWitness;
-  module Witness;
-} public;
-
-syntax alias BaseLayerInstance := B.Instance;
-
-module Proper;
-  type Instance :=
-    mkInstance@{
-      commitments : List Nat;
-      nullifiers : List Nat;
-      tag : Tag;
-      appData : Nat;
-    };
-
-  fromBaseLayerInstance (b : B.Instance) (w : Witness) : Instance :=
-    let
-      btag := B.Instance.tag b;
-      isCommit (r : Resource) : Bool := base-commitment r == btag;
-      isNullifier (r : Resource) : Bool := base-nullifier r == btag;
-      findCommit : Maybe Resource := find isCommit (Witness.created w);
-      tag :=
-        case findCommit of
-          | just createdResource := Created (commitment createdResource)
-          | nothing :=
-            let
-              findNullifier : Maybe Resource :=
-                find isNullifier (Witness.consumed w);
-            in case findNullifier of
-                 | nothing :=
-                   failwith
-                     "impossible: tag didn't match any nullifier or commitment"
-                 | just consumedRes := Consumed (nullifier consumedRes);
-    in mkInstance@{
-         commitments := B.Instance.commitments b;
-         nullifiers := B.Instance.nullifiers b;
-         appData := B.Instance.appData b;
-         tag;
-       };
-end;
-
-syntax alias Logic := B.Logic;
-
-type ProvingKey :=
-  mkProvingKey@{
-    unProvingKey : Resource;
-  };
-
-type ProofRecord :=
-  mkProofRecord@{
-    proof : Proof;
-    verifyingKeyUNUSED : Unit;
-    instance : Instance;
-  };
diff --git a/Anoma/Transaction.juvix b/Anoma/Transaction.juvix
deleted file mode 100644
index 6cfd0f9..0000000
--- a/Anoma/Transaction.juvix
+++ /dev/null
@@ -1,6 +0,0 @@
-module Anoma.Transaction;
-
-import Anoma.Transaction.Action open public;
-import Anoma.Transaction.AppData open public;
-import Anoma.Transaction.CustomInputs open public;
-import Anoma.Transaction.Object open public;
diff --git a/Anoma/Transaction/Action.juvix b/Anoma/Transaction/Action.juvix
deleted file mode 100644
index 6ff0a20..0000000
--- a/Anoma/Transaction/Action.juvix
+++ /dev/null
@@ -1,6 +0,0 @@
-module Anoma.Transaction.Action;
-
-import BaseLayer.ResourceMachine as B;
-
-open B using {Action; mkAction; module Action} public;
-open B using {actionDelta; actionsDelta} public;
diff --git a/Anoma/Transaction/AppData.juvix b/Anoma/Transaction/AppData.juvix
deleted file mode 100644
index bd3f950..0000000
--- a/Anoma/Transaction/AppData.juvix
+++ /dev/null
@@ -1,63 +0,0 @@
-module Anoma.Transaction.AppData;
-
-import Stdlib.Prelude open;
-import Stdlib.Data.Map as Map open using {Map};
-import Anoma.Builtin.ByteArray open using {ByteArray};
-import Anoma.Builtin.System open using {anomaEncode; anomaDecode};
-import Anoma.Utils open;
-
---- A data type encoding the deletion criterion.
--- TODO Add enumeration from the specs.
-type DeletionCriterion :=
-  | AfterBlock STILL_MISSING_DEFINITION
-  | AfterTimestamp STILL_MISSING_DEFINITION
-  | AfterSignatureOverData STILL_MISSING_DEFINITION
-  | AfterPredicates STILL_MISSING_DEFINITION
-  | StoreForever;
-
---- A data type encoding the lookup key of application.
---- TODO Add an equivalent to `anomaEncode` and `anomaDecode` to be able to change this to ;ByteArray;.
-type AppDataKey :=
-  mkAppDataKey@{
-    unAppDataKey : Nat;
-  };
-
---- A data type encoding the lookup value of application data.
---- TODO Add an equivalent to `anomaEncode` and `anomaDecode` to be able to change this to ;ByteArray;.
-type AppDataValue :=
-  mkAppDataValue@{
-    data : Nat;
-    deletionCriterion : DeletionCriterion;
-  };
-
--- A type describing an app data map.
--- AppData : Type := Nat;
-
-deriving instance
-DeletionCriterion-Ord : Ord DeletionCriterion;
-
-deriving instance
-DeletionCriterion-Eq : Eq DeletionCriterion;
-
-deriving instance
-AppDataKey-Ord : Ord AppDataKey;
-
-deriving instance
-AppDataKey-Eq : Eq AppDataKey;
-
-deriving instance
-AppDataValue-Ord : Ord AppDataValue;
-
-deriving instance
-AppDataValue-Eq : Eq AppDataValue;
-
--- lookupAppData
---   {Key Value : Type} (key : Key) (appData : AppData) : Maybe Value :=
---   case
---     Map.lookup@{
---       key := anomaEncode key |> mkAppDataKey;
---       map := appData;
---     }
---   of
---     | nothing := nothing
---     | just value := just (value |> AppDataValue.data |> anomaDecode);
diff --git a/Anoma/Transaction/Object.juvix b/Anoma/Transaction/Object.juvix
deleted file mode 100644
index 70f0739..0000000
--- a/Anoma/Transaction/Object.juvix
+++ /dev/null
@@ -1,5 +0,0 @@
-module Anoma.Transaction.Object;
-
-import BaseLayer.ResourceMachine as B;
-
-open B using {Transaction; mkTransaction; module Transaction} public;
diff --git a/Applib/Authorization.juvix b/Applib/Authorization.juvix
index c791d2b..1e19454 100644
--- a/Applib/Authorization.juvix
+++ b/Applib/Authorization.juvix
@@ -2,4 +2,3 @@ module Applib.Authorization;
 
 -- import Applib.Authorization.Check as Check open public;
 import Applib.Identities as Identities open public;
-import Applib.Authorization.Message as Message open public;
diff --git a/Applib/Authorization/Message.juvix b/Applib/Authorization/Message.juvix
deleted file mode 100644
index 086fcf3..0000000
--- a/Applib/Authorization/Message.juvix
+++ /dev/null
@@ -1,142 +0,0 @@
-module Applib.Authorization.Message;
-
-import Stdlib.Prelude open;
-import Stdlib.Data.Set as Set open using {Set};
-import Stdlib.Data.Map as Map;
-import Anoma open;
-import Anoma.Builtin.System open;
-
-import Applib.Helpers open;
-import Applib.Identities open;
-
---- A message format specifiying resources that must be created and consumed within an ;Action;.
---- @param origin The reference to the resource performing the check.
---- @param mustBeConsumed The resources that must be consumed.
---- @param mustBeCreated The resources that must be created.
-type ResourceRelationship :=
-  mkResourceRelationship@{
-    origin : Tag;
-    mustBeConsumed : Set Nullifier;
-    mustBeCreated : Set Commitment;
-  };
-
---- Checks that a ;ResourceRelationship; message has the expected values.
---- @param message The resource relationship message to check.
---- @param origin The expected origin.
---- @param nullifiers The nullifier set that must contain the `mustBeConsumed` nullifiers as a subset.
---- @param commitments The commitment set that must contain the `mustBeCreated` commitments as a subset.
---- @return The check result.
-checkResourceRelationship
-  (message : ResourceRelationship)
-  (origin : Tag)
-  (nullifiers : Set Nullifier)
-  (commitments : Set Commitment)
-  : Bool :=
-  ResourceRelationship.origin message == origin
-    && Set.isSubset (ResourceRelationship.mustBeConsumed message) nullifiers
-    && Set.isSubset (ResourceRelationship.mustBeCreated message) commitments;
-
--- --- Creates an ;AppData; entry consisting of a ;ResourceRelationship; message and corresponding ;Signature; as the ;AppDataValue; and the resource ;Tag; value as the ;AppDataKey;.
---- @param identity The identity to derive the nullifier key from.
---- @param origin The resource performing the check.
---- @param mustBeConsumed The resources that must be consumed.
---- @param mustBeCreated The resources that must be created.
---- @return The app data entry.
-mkResourceRelationshipAppDataEntry
-  (signer : InternalIdentity)
-  (origin : Tag)
-  (mustBeConsumed : Set Nullifier)
-  (mustBeCreated : Set Commitment)
-  : Pair AppDataKey AppDataValue :=
-  let
-    message : ResourceRelationship :=
-      mkResourceRelationship@{
-        origin;
-        mustBeConsumed;
-        mustBeCreated;
-      };
-    signature : Signature :=
-      sign@{
-        message;
-        signer;
-      };
-  in case origin of
-       | Created commitment :=
-         toAppDataEntry@{
-           key := commitment;
-           data := message, signature;
-         }
-       | Consumed nullifier :=
-         toAppDataEntry@{
-           key := nullifier;
-           data := message, signature;
-         };
-
--- module ActionFromConvertable;
---   import Applib.Resource.Traits.Convertable open;
---   import Applib.Transaction.Traits open;
-
--- --- Instantiates the ;ActionConvertable; trait with a parametrized function accepting `ConsumedTypedResource` and `CreatedTypedResource` being required to implement the ;Ord; and ;Convertable; traits.
--- --- The underlying inmplementation converts the typed resources to standard ;Resource;s and creates an ;Action; with
--- --- - authorization ;AppData; containing an ;AppData; entry for every consumed ;Resource;.
--- --- - custom inputs (;CustomInputs;) containing entries mapping nullifiers to consumed resources and commitments to created resources.
--- actionWithAuthorizationAppData
---   {ConsumedTypedResource CreatedTypedResource}
---   {{Ord ConsumedTypedResource}}
---   {{Ord CreatedTypedResource}}
---   {{Convertable ConsumedTypedResource}}
---   {{Convertable CreatedTypedResource}}
---   : ActionConvertable ConsumedTypedResource CreatedTypedResource :=
---   mkActionConvertable@{
---     toAction
---       (standardInputs : StandardInputs)
---       (consumedResources : Set ConsumedTypedResource)
---       (createdResources : Set CreatedTypedResource)
---       : Action :=
---       let
---         -- Convert typed resources to resources.
---         consumed :=
---           Set.map (r in consumedResources) {
---             Convertable.toResource r
---           };
---         created :=
---           Set.map (r in createdResources) {
---             Convertable.toResource r
---           };
-
---         -- Put maps into the custom inputs that map:
---         -- - nullifiers to consumed resources
---         -- - commitments to created resources
---         tagsAndCustomInputs :=
---           computeTagsAndCustomInputs@{
---             consumed;
---             created;
---           };
---         tags := TagsAndCustomInputs.tags tagsAndCustomInputs;
---         pair := tagsToPair tags;
---         nullifiers := fst pair;
---         commitments := snd pair;
-
---         -- Put signed messages and signatures by the owner in the app data.
---         -- The signed messages link back to the original consumed resources, where the signature verification is part of the resource logic requiring the commitments of created resources to be part of the action.
---         appData :=
---           Set.map (nullifier in nullifiers) {
---               mkResourceRelationshipAppDataEntry@{
---                 signer :=
---                   Identity.internal (StandardInputs.caller standardInputs);
---                 origin := Consumed nullifier;
---                 mustBeConsumed := Set.empty;
---                 mustBeCreated := commitments;
---               }
---             }
---             |> Map.fromSet;
---       in mkActionHelper@{
---            consumed;
---            created;
---            appData;
---            customInputs :=
---              TagsAndCustomInputs.customInputs tagsAndCustomInputs;
---            tags;
---          };
---   };
--- end;
diff --git a/Applib/Helpers.juvix b/Applib/Helpers.juvix
index 70dd9c8..330c5bf 100644
--- a/Applib/Helpers.juvix
+++ b/Applib/Helpers.juvix
@@ -14,24 +14,20 @@ import BaseLayer.ResourceMachine as BaseLayer;
 
 import Applib.Resource.Traits.Convertable open;
 
-fromJust {A} : Maybe A -> A
-  | nothing := failwith "fromJust"
-  | (just x) := x;
-
 findResourceByNullifier
-  (nf : Nat) (privateInputs : Logic.Witness) : Maybe Resource :=
+  (nf : Nat) (privateInputs : BaseLayer.Witness) : Maybe Resource :=
   let
-    hasNullifier (nf : Nat) (r : Resource) : Bool := base-nullifier r == nf;
+    hasNullifier (nf : Nat) (r : Resource) : Bool := BaseLayer.nullifier r == nf;
     getConsumed (nf : Nat) : Maybe Resource :=
-      find (hasNullifier nf) (Logic.Witness.consumed privateInputs);
+      find (hasNullifier nf) (BaseLayer.Witness.consumed privateInputs);
   in getConsumed nf;
 
 findResourceByCommitment
-  (cm : Nat) (privateInputs : Logic.Witness) : Maybe Resource :=
+  (cm : Nat) (privateInputs : BaseLayer.Witness) : Maybe Resource :=
   let
-    hasCommitment (cm : Nat) (r : Resource) : Bool := base-commitment r == cm;
+    hasCommitment (cm : Nat) (r : Resource) : Bool := BaseLayer.commitment r == cm;
     getCreated (cm : Nat) : Maybe Resource :=
-      find (hasCommitment cm) (Logic.Witness.created privateInputs);
+      find (hasCommitment cm) (BaseLayer.Witness.created privateInputs);
   in getCreated cm;
 
 type ResourceStatus :=
@@ -39,13 +35,7 @@ type ResourceStatus :=
   | CreatedRes Resource
   | ConsumedRes Resource;
 
-fromStatus (status : ResourceStatus) : Resource :=
-  case status of
-    | CreatedRes r := r
-    | ConsumedRes r := r
-    | NonExisting := failwith "resource does not exist";
-
-findResource (tag : Nat) (privateInputs : Logic.Witness) : ResourceStatus :=
+findResource (tag : Nat) (privateInputs : BaseLayer.Witness) : ResourceStatus :=
   case findResourceByNullifier tag privateInputs of
     | just consumed := ConsumedRes consumed
     | nothing :=
@@ -63,21 +53,6 @@ lookupResource {A} (key : A) (customInputs : CustomInputs) : Maybe Resource :=
     customInputs;
   };
 
-toAppDataEntry
-  {Key Data : Type}
-  (key : Key)
-  (data : Data)
-  {deletionCriterion : DeletionCriterion := StoreForever}
-  : Pair AppDataKey AppDataValue :=
-
-  mkAppDataKey@{
-    unAppDataKey := anomaEncode key;
-  }
-    , mkAppDataValue@{
-        data := anomaEncode data;
-        deletionCriterion;
-      };
-
 toCustomInputsEntry
   {Key Value : Type}
   (key : Key)
@@ -105,147 +80,52 @@ type TagsAndCustomInputs :=
     customInputs : CustomInputs;
   };
 
-tagsToPair (tags : List Tag) : Pair (List Nullifier) (List Commitment) :=
-  for (nfs, cms := [], []) (tag in tags) {
-    case tag of
-      | Consumed nf := nfs ++ [nf], cms
-      | Created cm := nfs, cms ++ [cm]
-  };
-
-pairtoTags
-  (nullifiers : Set Nullifier) (commitments : Set Commitment) : Set Tag :=
-  Set.union
-    Set.map (nullifier in nullifiers) {
-      Consumed nullifier
-    }
-    Set.map (commitment in commitments) {
-      Created commitment
-    };
-
-computeTags (consumed created : List Resource) : List Tag :=
-  let
-    nullifierTags :=
-      map (r in consumed) {
-        Consumed (nullifier r)
-      };
-    commitmentTags :=
-      map (r in created) {
-        Created (commitment r)
-      };
-  in nullifierTags ++ commitmentTags;
-
-computeTagsAndCustomInputs
-  (consumed created : List Resource) : TagsAndCustomInputs :=
+mkActionHelper
+  (consumed created : List Resource) {app-data : Nat := 0} : BaseLayer.Action :=
   let
-    consumed' : List Resource := consumed;
-    created' : List Resource := created;
-
-    nullifiers' : List Nullifier := map nullifier consumed';
-    commitments' : List Commitment := map commitment created';
-
-    tags' : List Tag := map Consumed nullifiers' ++ map Created commitments';
-  in mkTagsAndCustomInputs@{
-       tags := tags';
-       customInputs :=
-         Map.fromList
-           (zipWith toCustomInputsEntry tags' (consumed' ++ created'));
-     };
-
-module ProvingHelpers;
-  createLogicProofRecord
-    (tag : Tag)
-    (publicInputs : Logic.Instance)
-    (privateInputs : Logic.Witness)
-    : ProofRecord :=
-    let
-      proof : Logic.Proof :=
-        Logic.prove@{
-          provingKey :=
-            Logic.mkProvingKey
-              (fromStatus (findResource (tagToNat tag) privateInputs));
-          publicInputs;
-          privateInputs;
+    nullifiers := map BaseLayer.nullifier consumed;
+    commitments := map BaseLayer.commitment created;
+    all-resources := zip consumed nullifiers ++ zip created commitments;
+
+    public-inputs : Nat -> BaseLayer.Instance
+      | tag :=
+        BaseLayer.mkInstance@{
+          commitments;
+          nullifiers;
+          tag;
+          app-data;
         };
-      verifyingKey := unit;
-      proofRecord := Logic.mkProofRecord proof verifyingKey publicInputs;
-    in LogicProofRecord proofRecord;
-end;
-
-open ProvingHelpers;
 
--- Helps with the creation of an action ;Action;.
--- @param identity The identity to derive the nullifier key from.
--- @param consumed The resources being consumed in this action.
--- @param created The resources being created in this action.
--- @param appData The app data of the action.
--- @param customInputs The custom inputs of the action.
--- @param maybeNullifiers Optional nullifiers to avoid recomputation.
--- @param maybeCommitments Optional commitments to avoid recomputation.
--- @return The action object.
-mkActionHelper
-  (consumed created : List Resource)
-  {appData : Nat := 0}
-  {custom : CustomInputs := Map.empty}
-  : Action :=
-  let
-    tags :=
-      computeTags@{
-        consumed;
+    private :=
+      BaseLayer.mkWitness@{
         created;
+        consumed;
+        customInputs := 0;
       };
-    (nullifiers', commitments') := tagsToPair tags;
-    nullifiers := map Nullifier.unNullifier nullifiers';
-    commitments := map Commitment.unCommitment commitments';
-
     -- Compute proofs
-    logicProofs : List ProofRecord :=
-      map (tag in tags) {
-        createLogicProofRecord@{
-          tag;
-          publicInputs :=
-            Logic.mkInstance@{
-              tag := tagToNat tag;
-              commitments;
-              nullifiers;
-              appData;
-            };
-          privateInputs :=
-            Logic.mkWitness@{
-              created;
-              consumed;
-              customInputs := anomaEncode custom;
-            };
-        }
+    logicProofs : List BaseLayer.Proof :=
+      map (resource, tag in all-resources) {
+        BaseLayer.proofLogic resource (public-inputs tag, private)
       };
-
-    complianceProofs : List ProofRecord := [];
-  in mkAction@{
+  in BaseLayer.mkAction@{
        commitments;
        nullifiers;
-       proofs := map proofRecordToProof (logicProofs ++ complianceProofs);
-       appData := appData;
+       proofs := logicProofs;
+       app-data;
      };
 
-logicProofRecordToProof (p : Logic.ProofRecord) : Logic.Proof :=
-  Logic.ProofRecord.proof p;
-
-proofRecordToProof : ProofRecord -> Logic.Proof
-  | (LogicProofRecord logProof) := logicProofRecordToProof logProof
-  | ComplianceProofRecord := failwith "proofRecordToProof"
-  | DeltaProofRecord := failwith "proofRecordToProof";
-
 mkTransactionHelper
   {roots : List CommitmentTree.Root := []}
-  (actions : List Action)
-  : Transaction :=
-  mkTransaction@{
+  (actions : List BaseLayer.Action)
+  : BaseLayer.Transaction :=
+  BaseLayer.mkTransaction@{
     roots := map CommitmentTree.unRoot roots;
     actions;
     delta := BaseLayer.zeroDelta;
     deltaProof := 0;
   };
 
-emptyTx : Transaction :=
+emptyTx : BaseLayer.Transaction :=
   mkTransactionHelper@{
     roots := [];
     actions := [];
@@ -260,31 +140,14 @@ emptyTx : Transaction :=
 prepareStandardTransaction
   (standardInputs : StandardInputs)
   (consumed created : List Resource)
-  {appData : Nat := 0}
-  : Transaction :=
-  let
-    -- Put maps into the custom inputs that map:
-    -- - nullifiers to consumed resources
-    -- - commitments to created resources
-    tagsAndCustomInputs :=
-      computeTagsAndCustomInputs@{
-        consumed;
-        created;
-      };
-  in mkTransactionHelper@{
-       roots := [StandardInputs.currentRoot standardInputs];
-       actions :=
-         [
-           mkActionHelper@{
-             consumed;
-             created;
-             appData;
-             custom := TagsAndCustomInputs.customInputs tagsAndCustomInputs;
-           };
-         ];
-     };
+  {app-data : Nat := 0}
+  : BaseLayer.Transaction :=
+  mkTransactionHelper@{
+    roots := [StandardInputs.currentRoot standardInputs];
+    actions := [mkActionHelper consumed created {app-data}];
+  };
 
-composeAll (txs : Set Transaction) : Transaction :=
+composeAll (txs : Set BaseLayer.Transaction) : BaseLayer.Transaction :=
   for (acc := emptyTx) (tx in txs) {
     BaseLayer.compose acc tx
   };
diff --git a/Applib/Resource/Traits/Logic.juvix b/Applib/Resource/Traits/Logic.juvix
deleted file mode 100644
index 82afc3c..0000000
--- a/Applib/Resource/Traits/Logic.juvix
+++ /dev/null
@@ -1,20 +0,0 @@
-module Applib.Resource.Traits.Logic;
-
-import Stdlib.Prelude open;
-import Anoma open;
-
-trait
-type HasLogic ResourceT :=
-  mkHasLogic@{
-    get : ResourceT -> Logic;
-    set : Logic -> ResourceT -> ResourceT;
-  };
-
-instance
-Resource-HasLogic : HasLogic Resource :=
-  mkHasLogic@{
-    get (resource : Resource) : Logic := resource |> Resource.logic;
-
-    set (logic : Logic) (resource : Resource) : Resource :=
-      resource@Resource{logic};
-  };
diff --git a/BaseLayer/ResourceMachine.juvix b/BaseLayer/ResourceMachine.juvix
index 12f7824..2960f8a 100644
--- a/BaseLayer/ResourceMachine.juvix
+++ b/BaseLayer/ResourceMachine.juvix
@@ -25,7 +25,7 @@ type Instance :=
     commitments : List Nat;
     nullifiers : List Nat;
     tag : Nat;
-    appData : Nat;
+    app-data : Nat;
   };
 
 positive
@@ -86,7 +86,7 @@ type Action :=
     commitments : List Nat;
     nullifiers : List Nat;
     proofs : List Proof;
-    appData : Nat;
+    app-data : Nat;
   };
 
 builtin anoma-action-delta