diff --git a/clientlib/storage_modeling/README.md b/clientlib/storage_modeling/README.md
new file mode 100644
index 00000000..85efbe1a
--- /dev/null
+++ b/clientlib/storage_modeling/README.md
@@ -0,0 +1,115 @@
+# Storage Modeling
+Recovers the contract's storage layout and information about statements that deal with storage.
+This documentation currently covers the core parts of the storage modeling functionality.
+See the [API](storage_modeling_api.dl) and [clienthelpers](clienthelpers.dl) for additional functionality.
+
+## Type Declarations
+## `StorageConstruct`
+`StorageConstruct` is the main type that defines arbitrarily nested data structures using a nested ADT type.
+
+### Definition
+```solidity
+.type StorageConstruct = Constant {value: Value}
+                        | StaticArray {parConstruct: StorageConstruct, arraySize: number}
+                        | Array {parConstruct: StorageConstruct}
+                        | Mapping {parConstruct: StorageConstruct}
+                        | Offset {parConstruct: StorageConstruct, offset: number}
+                        | Variable {construct: StorageConstruct}
+                        | TightlyPackedVariable {construct: StorageConstruct, byteLow: number, byteHigh: number}
+```
+
+#### Example
+The following example can be used to intuitively understand how nested structures are modeled.
+Smart contract declarations:
+```solidity
+contract StorageExample {
+  uint256 public supply;  // slot 0x0
+  address public owner;   // slot 0x1
+  bool public isPaused;   // slot 0x1
+  uint256[] public supplies; // slot 0x2
+  mapping (address => bool) public admins; // slot 0x3
+  struct vals {uint256 field0; uint256 field1;}
+  mapping (address => mapping(uint256 => vals)) public complex; // slot 0x4
+}
+```
+
+Construct inferences:
+```solidity
+Variable(Constant(0x0)) // uint256 supply
+Variable(Constant(0x1)) // address owner , bool isPaused
+Variable(Array(Constant(0x2))) // uint256 [] supplies
+Variable(Mapping(Constant(0x3))) // mapping admins
+// the 2 fields of struct value of nested mapping complex :
+Variable(Mapping(Mapping(Constant(0x4))))
+Variable(Offset(Mapping(Mapping(Constant(0x4))), 1))
+```
+
+## `StorageStmtKind`
+The `StorageStmtKind` type is used to describe the kind of load or write a storage statement performs.
+
+### Definition
+```solidity
+.type StorageStmtKind = VariableAccess {}
+                      | ArrayDataStart {}
+                      | ArrayLength {}
+```
+
+Storage statement kind can be:
+* `VariableAccess` which can be used to read or write either:
+  * A top-level variable
+  * A struct field
+  * An array or mapping element
+* `ArrayDataStart` which loads or writes to the start location of an array
+* `ArrayLength` which is used to load or write the length of an array
+
+## `VarOrConstWrite`
+The `VarOrConstWrite` type is introduced to unify writes of variables and constants.
+
+### Definition
+```solidity
+.type VarOrConstWrite = VariableWrite {var: Variable}
+                      | ConstantWrite {const: Value}
+```
+
+## Main relations
+
+---
+`.decl StorageStmtKindAndConstruct(stmt: Statement, kind: StorageStmtKind, construct: StorageConstruct)`
+Maps Storage Stmts to their corresponding construct and their `StorageStmtKind`
+__Note__: Storage stmts do not have to be `SSTORE` and `SLOAD` statements, see `StorageLoad` for more info
+
+---
+`.decl StorageStmt_HighLevelUses(stmt: Statement, accessVar: Variable, offset: number, i: number, nestedness: number)`
+Information about storage stmts on potentially nested data structures.
+Can be used to get all information on index variables and field offsets at every step.
+
+---
+`.decl StorageLoad(load: Statement, cons: StorageConstruct, loadedVar: Variable)`
+Storage load information.
+In cases of packed variables a single `SLOAD` can load multiple high-level variables.
+In these cases we consider the `load` to not be the `SLOAD` but rather the statement that ends up
+extracting the bytes that define the packed variable (cast, etc).
+
+---
+`.decl StorageStore(store: Statement, cons: StorageConstruct, write: VarOrConstWrite)`
+`SSTORE` statement write information.
+A write can be either a Variable or a Constant in cases where the actual written constant doesn't have a corresponding `Variable_Value` fact.  
+__Note__: Due to optimized packed variable write patterns, one `SSTORE` can write multiple different constructs
+
+---
+`.decl ArrayDeleteOp(sstore: Statement, loop: Block, array: StorageConstruct)`
+An `array` is deleted by setting its length to zero in `sstore` and then erasing all its contents in a following `loop`.
+
+---
+`.decl DataStructureValueIsStruct(cons: StorageConstruct, structID: symbol, elemNum: number)`
+Data structure construct has a value (Mappings) or element (Arrays) that is a struct identified by its `structID`
+
+---
+`.decl StructToString(structID: symbol, stringStruct: symbol)`
+Map struct identified by `structID` to solidity-like struct definition `stringStruct`.
+
+---
+
+
+
+---
\ No newline at end of file
diff --git a/clientlib/storage_modeling/clienthelpers.dl b/clientlib/storage_modeling/clienthelpers.dl
new file mode 100644
index 00000000..ed2a505f
--- /dev/null
+++ b/clientlib/storage_modeling/clienthelpers.dl
@@ -0,0 +1,18 @@
+
+/**
+  Storage modeling client helpers
+  Relations that can be computed using relations in the API but are useful standalone
+*/
+
+// Doesn't contain TightlyPackedVariable, maybe revisit
+.decl StorageConstruct_ParentAndOffset(cons: StorageConstruct, parentCons: StorageConstruct, offset: number)
+
+
+.decl StorageConstructPredecesor(cons: StorageConstruct, predCons: StorageConstruct)
+
+StorageConstructPredecesor(cons, parentCons):-
+  StorageConstruct_ParentAndOffset(cons, parentCons, _).
+
+StorageConstructPredecesor(cons, predParentCons):-
+  StorageConstructPredecesor(cons, predCons),
+  StorageConstruct_ParentAndOffset(predCons, predParentCons, _).
\ No newline at end of file
diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 9d02c4b2..1f4f418d 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -1,8 +1,4 @@
 
-/***
- New Storage Model
- Aims to support arbituary nested data structures
-***/
 
 /**
   `StorageIndex` contains information on the data structure used as well as the variables
@@ -15,16 +11,6 @@
                     | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
                     | OffsetIndex {parIndex: StorageIndex, offset: number}
 
-/**
-  `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
-*/
-.type StorageConstruct = Constant {value: Value}
-                        | StaticArray {parConstruct: StorageConstruct, arraySize: number}
-                        | Array {parConstruct: StorageConstruct}
-                        | Mapping {parConstruct: StorageConstruct}
-                        | Offset {parConstruct: StorageConstruct, offset: number}
-                        | Variable {construct: StorageConstruct}
-                        | TightlyPackedVariable {construct: StorageConstruct, byteLow: number, byteHigh: number}
 
 /**
   Syntactic translation of `StorageIndex` to `StorageConstruct`
@@ -51,12 +37,20 @@
 // Indexes in this relation can only be used directly to construct offset indexes
 .decl LikelyVariableLoadingStorageIndex(index: StorageIndex)
 
+/**
+  Maps `SSTORE`, `SLOAD` (and more, for packed vars) statements to the high-level information:
+  - `kind` can be "ACCESS", "LENGTH", "GETDATASTART"
+  - `index` can be used to get the high-level uses of the composite storage data structure accesses and writes
+  - `construct` is the data structure that is being accessed/written to
+*/
+.decl StorageStmtToIndexAndConstruct(stmt: Statement, kind: symbol, index: StorageIndex, construct: StorageConstruct)
+
+.decl StorageIndex_HighLevelUses(index: StorageIndex, accessVar: Variable, offset: number, i: number, nestedness: number)
+
 // Construct is not used as a variable (i.e. is used as an array or mapping)
 // Used to find the ones that are end-level variables
 .decl NonVariableConstruct(cons: StorageConstruct)
 
-.decl StorageIndex_HighLevelUses(index: StorageIndex, accessVar: Variable, offset: number, i: number, nestedness: number)
-
 .decl IsStorageConstruct(cons: StorageConstruct)
 
 // StorageConstruct is array or mapping
@@ -65,37 +59,13 @@
 // Number of elements the value of a data structure construct (Array or Mapping) has
 .decl DataStructure_ElemNum(cons: StorageConstruct, elemNum: number)
 
-// Data structure construct has a value (Mappings) or element (Arrays) that is a struct
-.decl DataStructureValueIsStruct(cons: StorageConstruct, structID: symbol, elemNum: number)
-
-// value type for mapping or element type for arrays
-.decl DataStructure_ValueOrElementType(cons: StorageConstruct, type: symbol)
-
-// key type for mapping
-.decl Mapping_KeyType(cons: StorageConstruct, type: symbol)
-
-// Map `structID` to solidity-like struct definition `stringStruct`
-.decl StructToString(structID: symbol, stringStruct: symbol)
+// Internal predicate, used to compute `StructToString`
 .decl StructToStringUpTo(structID: symbol, stringStruct: symbol, upTo: number)
 
 // Map tightly packed field in storage struct to solidity-like def used by `StructToString`
 .decl PackedStructWordToString(structID: symbol, offset: number, stringRep: symbol)
 .decl PackedStructWordToStringUpTo(structID: symbol, offset: number, stringRep: symbol, upToByte: number, upToIndex: number)
 
-// Note: Can probably be unified with `StorageVariable_Type`
-.decl DataStructure_Type(cons: StorageConstruct, type: symbol)
-
-// Doesn't contain TightlyPackedVariable, maybe revisit
-.decl StorageConstruct_ParentAndOffset(cons: StorageConstruct, parentCons: StorageConstruct, offset: number)
-
-/**
-  Maps `SSTORE` and `SLOAD` statements to the high-level information:
-  - `kind` can be "ACCESS", "LENGTH", "GETDATASTART"
-  - `index` can be used to get the high-level uses of the composite storage data structure accesses and writes
-  - `construct` is the data structure that is being accessed/written to
-*/
-.decl StorageStmtToIndexAndConstruct(stmt: Statement, kind: symbol, index: StorageIndex, construct: StorageConstruct)
-
 // Same as `StorageStmtToIndexAndConstruct`, populated before the tight packing component
 .decl InitialStorageStmtToIndexAndConstruct(stmt: Statement, kind: symbol, index: StorageIndex, construct: StorageConstruct)
 
@@ -496,6 +466,7 @@ StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $Variable(cons)):-
   StorageAccessOp(stmt, var),
   ProcessedStorageVariable($Variable(cons), $Variable(cons)).
 
+StorageLoad(stmt, $TightlyPackedVariable(cons, actualLow, actualHigh), var),
 StorageStmtToIndexAndConstruct(stmt, "ACCESS", index, $TightlyPackedVariable(cons, actualLow, actualHigh)):-
   LikelyVariableLoadingStorageIndex(index),
   StorageIndex_StorageConstruct(index, cons),
@@ -516,6 +487,68 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
   NormalizeStorageVarByteLimits($Variable(cons), low, high, actualLow, actualHigh),
   ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)).
 
+// New API relation computation
+DEBUG_OUTPUT(StorageLoad)
+DEBUG_OUTPUT(StorageStore)
+
+StorageLoad(stmt, $Variable(cons), loadedVar):-
+  LikelyVariableLoadingStorageIndex(index),
+  StorageIndex_StorageConstruct(index, cons),
+  Variable_StorageIndex(var, index),
+  SLOAD(stmt, var, loadedVar),
+  ProcessedStorageVariable($Variable(cons), $Variable(cons)).
+
+StorageStore(store, $Variable(cons), $VariableWrite(storedVar)):-
+  LikelyVariableLoadingStorageIndex(index),
+  StorageIndex_StorageConstruct(index, cons),
+  Variable_StorageIndex(var, index),
+  SSTORE(store, var, storedVar),
+  ProcessedStorageVariable($Variable(cons), $Variable(cons)).
+
+StorageStore(store, $TightlyPackedVariable(cons, actualLow, actualHigh), $VariableWrite(storedVar)):-
+  LikelyVariableLoadingStorageIndex(index),
+  StorageIndex_StorageConstruct(index, cons),
+  Variable_StorageIndex(indexVar, index),
+  StorageAccessOp(store, indexVar),
+  VarWrittenToBytesOfStorVarFinal(storedVar, store, $Variable(cons), low, high),
+  NormalizeStorageVarByteLimits($Variable(cons), low, high, actualLow, actualHigh),
+  ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)).
+
+StorageStore(store, $TightlyPackedVariable(cons, actualLow, actualHigh), $ConstantWrite(const)):-
+  LikelyVariableLoadingStorageIndex(index),
+  StorageIndex_StorageConstruct(index, cons),
+  Variable_StorageIndex(indexVar, index),
+  StorageAccessOp(store, indexVar),
+  ConstWrittenToBytesOfStorVarProcessed(_, const, store, _, $Variable(cons), low, high),
+  NormalizeStorageVarByteLimits($Variable(cons), low, high, actualLow, actualHigh),
+  ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)),
+  !VarWrittenToBytesOfStorVarFinal(_, store, $Variable(cons), low, high).
+
+// Not sure if this is needed
+// StorageStore(store, $Variable(cons), $ConstantWrite("0x0")):-
+//   LikelyVariableLoadingStorageIndex(index),
+//   StorageIndex_StorageConstruct(index, cons),
+//   Variable_StorageIndex(indexVar, index),
+//   StorageAccessOp(store, indexVar),
+//   DeleteOfStructSlot(store, $Variable(cons)),
+//   NormalizeStorageVarByteLimits($Variable(cons), _, _, actualLow, actualHigh),
+//   ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)).
+
+
+
+StorageStmtKindAndConstruct(stmt, $VariableAccess(), construct):-
+  StorageStmtToIndexAndConstruct(stmt, "ACCESS", _, construct).
+
+StorageStmtKindAndConstruct(stmt, $ArrayLength(), construct):-
+  StorageStmtToIndexAndConstruct(stmt, "LENGTH", _, construct).
+
+StorageStmtKindAndConstruct(stmt, $ArrayDataStart(), construct):-
+  StorageStmtToIndexAndConstruct(stmt, "GETDATASTART", _, construct).
+
+StorageStmt_HighLevelUses(stmt, accessVar, offset, i, nestedness):-
+  StorageStmtToIndexAndConstruct(stmt, _, index, _),
+  StorageIndex_HighLevelUses(index, accessVar, offset, i, nestedness).
+
 .decl StorageOffset_Type(offset: Value, type: symbol)
 
 StorageOffset_Type(offset, type):-
@@ -631,12 +664,8 @@ StorageConstantToHash(const, zeroPaded, as(@hex_keccak_256(zeroPaded), Value)):-
   Helper_Zeros(zeros, 64 - strlen(cut)),
   zeroPaded = cat("0x", cat(zeros, cut)).
 
-/**
-  An `array` is deleted by setting its length to zero in `sstore` and then erasing all its contents in a following `loop`. 
-*/
-.decl ArrayDeleteOp(sstore: Statement, loop: Block, array: StorageConstruct)
-DEBUG_OUTPUT(ArrayDeleteOp)
 
+DEBUG_OUTPUT(ArrayDeleteOp)
 ArrayDeleteOp(sstore, loop, array):-
   SSTORE(sstore, _, zeroVar),
   Variable_Value(zeroVar, "0x0"),
diff --git a/clientlib/storage_modeling/storage_modeling.dl b/clientlib/storage_modeling/storage_modeling.dl
index 1f461795..f9e384ac 100644
--- a/clientlib/storage_modeling/storage_modeling.dl
+++ b/clientlib/storage_modeling/storage_modeling.dl
@@ -7,12 +7,16 @@
 
 #define PACKED_FIELD(fieldNum,byteLow,byteHigh) MERGED_STORAGE_VAR(cat("field", to_string(fieldNum)),byteLow,byteHigh)
 
+#define MISSING_VAR_PLACEHOLDER "0xNoVar"
+
 #include "../dominators.dl"
 #include "../flows.dl"
 #include "../casts_shifts.dl"
 
+#include "storage_modeling_api.dl"
 #include "data_structures.dl"
 #include "tight_packing.dl"
 #include "type_inference.dl"
+#include "clienthelpers.dl"
 #include "legacy_data_structures.dl"
 #include "metrics.dl"
\ No newline at end of file
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
new file mode 100644
index 00000000..7fedfad2
--- /dev/null
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -0,0 +1,107 @@
+
+/***
+ New Storage Model
+ Aims to support arbituary nested data structures
+***/
+
+/**
+  `StorageConstruct` contains the information that can be used to describe arbitrarily nested data structures.
+  Each construct will start from a `Constant` offset that represent its allocated offset.
+  End-level (non intermediate) constucts end with `Variable` or `TightlyPackedVariable` facts.
+*/
+.type StorageConstruct = Constant {value: Value}
+                        | StaticArray {parConstruct: StorageConstruct, arraySize: number}
+                        | Array {parConstruct: StorageConstruct}
+                        | Mapping {parConstruct: StorageConstruct}
+                        | Offset {parConstruct: StorageConstruct, offset: number}
+                        | Variable {construct: StorageConstruct}
+                        | TightlyPackedVariable {construct: StorageConstruct, byteLow: number, byteHigh: number}
+
+/**
+  Storage Statement Kind:
+    * VariableAccess which can be used to read or write either:
+      * A top-level variable
+      * A struct field
+      * An array or mapping element
+    * ArrayDataStart which loads or writes to the start location of an array
+    * ArrayLength which is used to load or write the length of an array
+
+*/
+.type StorageStmtKind = VariableAccess {}
+                      | ArrayDataStart {}
+                      | ArrayLength {}
+
+.type VarOrConstWrite = VariableWrite {var: Variable}
+                      | ConstantWrite {const: Value}
+
+
+/**
+  Maps Storage Stmts to their corresponding construct and their `StorageStmtKind`
+  __Note__: Storage stmts do not have to be `SSTORE` and `SLOAD` statements, see `StorageLoad` for more info
+*/
+.decl StorageStmtKindAndConstruct(stmt: Statement, kind: StorageStmtKind, construct: StorageConstruct)
+
+/**
+  Information about storage stmts on potentially nested data structures.
+  Can be used to get all information on index variables and field offsets at every step.
+*/
+.decl StorageStmt_HighLevelUses(stmt: Statement, accessVar: Variable, offset: number, i: number, nestedness: number)
+
+/**
+  Storage load information.
+  In cases of packed variables a single `SLOAD` can load multiple high-level variables.
+  In these cases we consider the `load` to not be the `SLOAD` but rather the statement that ends up
+  extracting the bytes that define the packed variable (cast, etc)
+*/
+.decl StorageLoad(load: Statement, cons: StorageConstruct, loadedVar: Variable)
+
+/**
+  `SSTORE` statement write information.
+  A write can be either a Variable or a Constant in cases where the actual written constant doesn't have a corresponding
+  `Variable_Value` fact.  
+  __Note__: Due to optimized packed variable write patterns, one `SSTORE` can write multiple different constructs
+*/
+.decl StorageStore(store: Statement, cons: StorageConstruct, write: VarOrConstWrite)
+
+/**
+  Top-Level Global Variables
+  There is some overlap with the other, more general definitions
+  but I've also kept these separate relations for backwards compatibility
+ */
+
+.decl GlobalVariable(v: Value)
+
+.decl LoadGlobalVariable(stmt: Statement, val: Value, var: Variable)
+
+.decl StoreGlobalVariable(stmt: Statement, val: Value, var: Variable)
+
+// Info for top-level global variables
+.decl StorageVariableInfo(storageVariable: symbol, storageSlot: symbol, byteLow: number, byteHigh: number)
+
+
+/**
+  An `array` is deleted by setting its length to zero in `sstore` and then erasing all its contents in a following `loop`. 
+*/
+.decl ArrayDeleteOp(sstore: Statement, loop: Block, array: StorageConstruct)
+
+// Data structure construct has a value (Mappings) or element (Arrays) that is a struct
+.decl DataStructureValueIsStruct(cons: StorageConstruct, structID: symbol, elemNum: number)
+
+// Map `structID` to solidity-like struct definition `stringStruct`
+.decl StructToString(structID: symbol, stringStruct: symbol)
+
+/**
+  Type related outputs
+*/
+
+// value type for mapping or element type for arrays
+.decl DataStructure_ValueOrElementType(cons: StorageConstruct, type: symbol)
+
+// key type for mapping
+.decl Mapping_KeyType(cons: StorageConstruct, type: symbol)
+
+// Note: Can probably be unified with `DataStructure_Type`
+.decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
+
+// Note: Can probably be unified with `StorageVariable_Type`
+.decl DataStructure_Type(cons: StorageConstruct, type: symbol)
\ No newline at end of file
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 29eefed7..560dad22 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -499,7 +499,7 @@ SSTOREZeroRange(store, construct, byteLow, byteHigh):-
   byteLow <= byteHigh,
   1 + byteHigh - byteLow = count : {SSTOREZeroByte(store, construct, k), byteLow <= k, k <= byteHigh}.
 
-ConstWrittenToBytesOfStorVar("0xNoVar", "0x0", store, "lolo", construct, byteLow, byteHigh):-
+ConstWrittenToBytesOfStorVar(MISSING_VAR_PLACEHOLDER, "0x0", store, "lolo", construct, byteLow, byteHigh):-
   SSTOREZeroRange(store, construct, byteLow, byteHigh).
 
 
@@ -520,7 +520,7 @@ VarWrittenToBytesOfStorVarFinal(writtenVar, store, construct, byteLow, byteHigh)
 
 
 BytesOfStorVarKept(store, load, construct, keepByteLow, keepByteHigh),
-ConstWrittenToBytesOfStorVar("0xNoVar", "0x0", store, load, construct, maskByteLow, maskByteHigh):-
+ConstWrittenToBytesOfStorVar(MISSING_VAR_PLACEHOLDER, "0x0", store, load, construct, maskByteLow, maskByteHigh):-
   VarHoldsBytesOfStorVar(originVar, load, construct, 0, 31),
   ByteMaskOpKeepRange(originVar, storedVar, [keepByteLow, keepByteHigh]),
   ByteMaskOpMaskRange(originVar, storedVar, [maskByteLow, maskByteHigh]),
@@ -601,18 +601,6 @@ NormalizeStorageVarByteLimits(storVar, low, high, low, actualHigh):-
   actualHigh = max otherHigh :AnyLoadStoreStorVarBytes(_, storVar, low, otherHigh).
 
 
-/**
-  Top-Level Global Variables
- */
-
-.decl GlobalVariable(v: Value)
-
-.decl LoadGlobalVariable(stmt: Statement, val: Value, var: Variable)
-
-.decl StoreGlobalVariable(stmt: Statement, val: Value, var: Variable)
-
-// Info for top-level global variables
-.decl StorageVariableInfo(storageVariable: symbol, storageSlot: symbol, byteLow: number, byteHigh: number)
 
 // Processing of storage variables, accounting for tightly packed words
 .decl ProcessedStorageVariable(storageVar: StorageConstruct, storageVarProcessed: StorageConstruct)
@@ -624,69 +612,32 @@ DEBUG_OUTPUT(ProcessedStorageVariable)
 .decl StorageVariablePacksNVars(storageVar: StorageConstruct, numberOfVars: number)
 DEBUG_OUTPUT(StorageVariablePacksNVars)
 
-/* Old logic
-GlobalVariable(v) :-
-  SLOAD(_, index, _),
-  Variable_Value(index, v).
-*/
 
 GlobalVariable(v):-
   LoadGlobalVariable(_, v, _) ;
   StoreGlobalVariable(_, v, _).
 
+LoadGlobalVariable(load, storVar, loadedVar):-
+  StorageLoad(load, $Variable($Constant(storVar)), loadedVar).
 
-LoadGlobalVariable(stmt, storVar, var):-
-  SLOADOfConst(stmt, storVar, var),
-  FailedMergedStorageModeling($Variable($Constant(storVar))).
+LoadGlobalVariable(load, MERGED_STORAGE_VAR(storVar, low, high), loadedVar):-
+  StorageLoad(load, $TightlyPackedVariable($Constant(storVar), low, high), loadedVar).
 
-LoadGlobalVariable(stmt, as(storVar, Value), var):-
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  (SLOADOfConst(_, storVar, _); SSTOREToConst(_, storVar, _)), // ensure it's a global variable
-  VarHoldsBytesOfStorVarFinal(var, _, $Variable($Constant(storVar)), 0, 31),
-  Statement_Defines(stmt, var, 0).
+StoreGlobalVariable(store, storVar, writtenVar):-
+  StorageStore(store, $Variable($Constant(storVar)), $VariableWrite(writtenVar)).
 
-LoadGlobalVariable(stmt, v, var):-
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  (SLOADOfConst(_, storVar, _); SSTOREToConst(_, storVar, _)), // ensure it's a global variable
-  VarHoldsBytesOfStorVarFinal(_, _, $Variable($Constant(storVar)), low, high),
-  // perhaps we need to add new instruction here
-  NormalizeStorageVarByteLimits($Variable($Constant(storVar)), low, high, actualLow, actualHigh),
-  VarHoldsBytesOfStorVar(var, _, $Variable($Constant(storVar)), actualLow, actualHigh),
-  Statement_Defines(stmt, var, 0),
-  (low != 0 ; high != 31),
-  v = MERGED_STORAGE_VAR(storVar, low, high).
-
-StoreGlobalVariable(stmt, storVar, var):-
-  SSTOREToConst(stmt, storVar, var),
-  FailedMergedStorageModeling($Variable($Constant(storVar))).
-
-StoreGlobalVariable(stmt, storVar, var):-
-  SSTOREToConst(stmt, storVar, var),
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  (VarHoldsBytesOfStorVarFinal(_, _, $Variable($Constant(storVar)), 0, 31); !SLOADOfConstruct(_, $Variable($Constant(storVar)), _)).
-
-StoreGlobalVariable(store, v, writtenVar):-
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  SSTOREToConst(_, storVar, _), // ensure it's a global variable
-  VarWrittenToBytesOfStorVarFinal(writtenVar, store, $Variable($Constant(storVar)), byteLow, byteHigh),
-  NormalizeStorageVarByteLimits($Variable($Constant(storVar)), byteLow, byteHigh, actualLow, actualHigh),
-  ProcessedStorageVariable($Variable($Constant(storVar)), $TightlyPackedVariable($Constant(storVar), actualLow, actualHigh)),
-  v = MERGED_STORAGE_VAR(storVar, actualLow, actualHigh).
+StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), writtenVar):-
+  StorageStore(store, $TightlyPackedVariable($Constant(storVar), low, high), $VariableWrite(writtenVar)).
 
-StoreGlobalVariable(store, storVar, writtenVar):-
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  SSTOREToConst(_, storVar, _), // ensure it's a global variable
-  VarWrittenToBytesOfStorVarFinal(writtenVar, store, $Variable($Constant(storVar)), byteLow, byteHigh),
-  NormalizeStorageVarByteLimits($Variable($Constant(storVar)), byteLow, byteHigh, 0, 31),
-  ProcessedStorageVariable($Variable($Constant(storVar)), $Variable($Constant(storVar))).
+// MissingVar because we only infer a ConstantWrite when we cannot infer a variable write
+StoreGlobalVariable(store, storVar, MISSING_VAR_PLACEHOLDER):-
+  StorageStore(store, $Variable($Constant(storVar)), $ConstantWrite(const)),
+  const = const.
 
-StoreGlobalVariable(store, v, constVar):-
-  SuccessfulMergedStorageModeling($Variable($Constant(storVar))),
-  SSTOREToConst(_, storVar, _), // ensure it's a global variable
-  ConstWrittenToBytesOfStorVarProcessed(constVar, _, store, _, $Variable($Constant(storVar)), byteLow, byteHigh),
-  NormalizeStorageVarByteLimits($Variable($Constant(storVar)), byteLow, byteHigh, actualLow, actualHigh),
-  ProcessedStorageVariable($Variable($Constant(storVar)), $TightlyPackedVariable($Constant(storVar), actualLow, actualHigh)),
-  v = MERGED_STORAGE_VAR(storVar, actualLow, actualHigh).
+// MissingVar because we only infer a ConstantWrite when we cannot infer a variable write
+StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), MISSING_VAR_PLACEHOLDER):-
+  StorageStore(store, $TightlyPackedVariable($Constant(storVar), low, high), $ConstantWrite(const)),
+  const = const.
 
 
 StorageVariableInfo(storVar, storVar, 0, 31):-
@@ -707,6 +658,14 @@ ProcessedStorageVariable(construct, construct):-
     VarHoldsBytesOfStorVarFinal(_, _, construct, 0, 31)
   ).
 
+// Edge case
+// REVIEW: See if we can handle it using the above rule
+ProcessedStorageVariable(construct, construct):-
+  SuccessfulMergedStorageModeling(construct),
+  ConstWrittenToBytesOfStorVar(_, _, _, _, construct, 0, 31),
+  !VarWrittenToBytesOfStorVarFinal(_, _, construct, _, _),
+  !VarHoldsBytesOfStorVarFinal(_, _, construct, _, _).
+
 ProcessedStorageVariable(storageVar, $TightlyPackedVariable(parentCons, actualLow, actualHigh)):-
   SuccessfulMergedStorageModeling(storageVar),
   storageVar = $Variable(parentCons),
@@ -740,14 +699,14 @@ ConstWrittenToBytesOfStorVarProcessed(constVar, const, store, load, $Variable(pa
   ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, byteLow, actualByteHigh)),
   actualByteHigh > byteHigh.
 
-ConstWrittenToBytesOfStorVarProcessed("0xNoVar", as(@and_256(const, mask), Value), store, load, $Variable(parentCons), byteLow, actualByteHigh):-
+ConstWrittenToBytesOfStorVarProcessed(MISSING_VAR_PLACEHOLDER, as(@and_256(const, mask), Value), store, load, $Variable(parentCons), byteLow, actualByteHigh):-
   ConstWrittenToBytesOfStorVar(_, const, store, load, $Variable(parentCons), byteLow, byteHigh),
   ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, byteLow, actualByteHigh)),
   actualByteHigh < byteHigh,
   Mask_Length(mask, byteHigh - actualByteHigh),
   ValueIsByteMask(mask).
 
-ConstWrittenToBytesOfStorVarProcessed("0xNoVar", newVal, store, load, $Variable(parentCons), actualByteLow, actualByteHigh):-
+ConstWrittenToBytesOfStorVarProcessed(MISSING_VAR_PLACEHOLDER, newVal, store, load, $Variable(parentCons), actualByteLow, actualByteHigh):-
   ConstWrittenToBytesOfStorVar(_, const, store, load, $Variable(parentCons), writeByteLow, writeByteHigh),
   ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, actualByteLow, actualByteHigh)),
   writeByteLow <= actualByteLow,
@@ -757,7 +716,7 @@ ConstWrittenToBytesOfStorVarProcessed("0xNoVar", newVal, store, load, $Variable(
   ValueIsByteMask(mask),
   newVal = as(@and_256(@shr_256(@number_to_hex(excessRightBytes*8), const), mask), Value).
 
-ConstWrittenToBytesOfStorVarProcessed("0xNoVar", "0x0", store, store, $Variable(parentCons), actualByteLow, actualByteHigh):-
+ConstWrittenToBytesOfStorVarProcessed(MISSING_VAR_PLACEHOLDER, "0x0", store, store, $Variable(parentCons), actualByteLow, actualByteHigh):-
   DeleteOfStructSlot(store, $Variable(parentCons)),
   ProcessedStorageVariable($Variable(parentCons), $TightlyPackedVariable(parentCons, actualByteLow, actualByteHigh)).
 
@@ -794,4 +753,6 @@ DataStructuresTempStmt(load):-
   SuccessfulMergedStorageModeling(storVar),
   VarHoldsBytesOfStorVarFinal(var, load, storVar, _, _),
   Statement_Defines(stmt, var, 0),
+  // Ensure it's an SLOAD, it can be an SSTORE in some rare cases
+  Statement_Opcode(load, "SLOAD"),
   stmt != load.
diff --git a/clientlib/storage_modeling/type_inference.dl b/clientlib/storage_modeling/type_inference.dl
index d97c79b5..08ce8137 100644
--- a/clientlib/storage_modeling/type_inference.dl
+++ b/clientlib/storage_modeling/type_inference.dl
@@ -31,9 +31,6 @@ Type_Width(type, byteWidth):-
   type = cat("bytes", to_string(byteWidth)).
 
 
-// Note: Can probably be unified with `DataStructure_Type`
-.decl StorageVariable_Type(cons: StorageConstruct, type: symbol)
-
 // Added interm relation that can results removed via subsumption
 .decl StorageVariable_IntermType(cons: StorageConstruct, type: symbol) btree_delete