From 5b5acfdbeb632ce9eea220b7defcab81ee2709c5 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 28 Nov 2024 17:42:48 +0200
Subject: [PATCH 01/15] Separate storage modeling API. Initial commit. WIP.

---
 clientlib/storage_modeling/data_structures.dl | 58 +------------
 .../storage_modeling/storage_modeling.dl      |  1 +
 .../storage_modeling/storage_modeling_api.dl  | 82 +++++++++++++++++++
 clientlib/storage_modeling/tight_packing.dl   | 12 ---
 clientlib/storage_modeling/type_inference.dl  |  3 -
 5 files changed, 85 insertions(+), 71 deletions(-)
 create mode 100644 clientlib/storage_modeling/storage_modeling_api.dl

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 9d02c4b2..26488806 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -1,31 +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
-  used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
-*/
-.type StorageIndex = ConstantIndex {value: Value}
-                    | StaticArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
-                    | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
-                    | ArrayDataStartIndex {parIndex: StorageIndex}
-                    | 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`
 */
@@ -55,8 +28,6 @@
 // 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 +36,16 @@
 // 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)
 
@@ -631,12 +581,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..063f9d3a 100644
--- a/clientlib/storage_modeling/storage_modeling.dl
+++ b/clientlib/storage_modeling/storage_modeling.dl
@@ -11,6 +11,7 @@
 #include "../flows.dl"
 #include "../casts_shifts.dl"
 
+#include "storage_modeling_api.dl"
 #include "data_structures.dl"
 #include "tight_packing.dl"
 #include "type_inference.dl"
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
new file mode 100644
index 00000000..f97b160d
--- /dev/null
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -0,0 +1,82 @@
+
+/***
+ New Storage Model
+ Aims to support arbituary nested data structures
+***/
+
+/**
+  `StorageIndex` contains information on the data structure used as well as the variables
+  used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
+*/
+.type StorageIndex = ConstantIndex {value: Value}
+                    | StaticArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
+                    | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
+                    | ArrayDataStartIndex {parIndex: StorageIndex}
+                    | 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}
+
+
+
+/**
+  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)
+
+.decl StorageIndex_HighLevelUses(index: StorageIndex, accessVar: Variable, offset: number, i: number, nestedness: number)
+
+/**
+  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..42327af9 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -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)
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
 

From cfbe12de85dea29274bbe31c40e9a5b5f2956102 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Tue, 4 Feb 2025 17:46:47 +0200
Subject: [PATCH 02/15] Add new relations to storage modeling API in order to
 remove anything that uses index.

---
 clientlib/storage_modeling/data_structures.dl      | 14 ++++++++++++++
 clientlib/storage_modeling/storage_modeling_api.dl |  8 ++++++++
 2 files changed, 22 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 26488806..76264f4c 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -466,6 +466,20 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
   NormalizeStorageVarByteLimits($Variable(cons), low, high, 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, $DataStart(), construct):-
+  StorageStmtToIndexAndConstruct(stmt, "GETDATASTART", _, construct).
+
+StorageStmt_HighLevelUses(stmt, accessVar, offset, i, nestedness):-
+  StorageAccessOp(stmt, indexVar),
+  Variable_StorageIndex(indexVar, index),
+  StorageIndex_HighLevelUses(index, accessVar, offset, i, nestedness).
+
 .decl StorageOffset_Type(offset: Value, type: symbol)
 
 StorageOffset_Type(offset, type):-
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
index f97b160d..3f047b4a 100644
--- a/clientlib/storage_modeling/storage_modeling_api.dl
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -15,6 +15,10 @@
                     | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
                     | OffsetIndex {parIndex: StorageIndex, offset: number}
 
+.type StorageStmtKind = VariableAccess {}
+                      | DataStart {}
+                      | ArrayLength {}
+
 /**
   `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
 */
@@ -38,6 +42,10 @@
 
 .decl StorageIndex_HighLevelUses(index: StorageIndex, accessVar: Variable, offset: number, i: number, nestedness: number)
 
+.decl StorageStmtKindAndConstruct(stmt: Statement, kind: StorageStmtKind, construct: StorageConstruct)
+
+.decl StorageStmt_HighLevelUses(stmt: Statement, accessVar: Variable, offset: number, i: number, nestedness: number)
+
 /**
   Top-Level Global Variables
   There is some overlap with the other, more general definitions

From a0a612a011b0a9a4f872395971745bae4013b100 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 5 Feb 2025 02:38:07 +0200
Subject: [PATCH 03/15] More work in storage modeling API, introduce
 clienthelpers.dl

---
 clientlib/storage_modeling/clienthelpers.dl    | 18 ++++++++++++++++++
 clientlib/storage_modeling/data_structures.dl  |  3 ---
 clientlib/storage_modeling/storage_modeling.dl |  1 +
 3 files changed, 19 insertions(+), 3 deletions(-)
 create mode 100644 clientlib/storage_modeling/clienthelpers.dl

diff --git a/clientlib/storage_modeling/clienthelpers.dl b/clientlib/storage_modeling/clienthelpers.dl
new file mode 100644
index 00000000..4d1ebaeb
--- /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 76264f4c..6c2872c8 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -43,9 +43,6 @@
 .decl PackedStructWordToString(structID: symbol, offset: number, stringRep: symbol)
 .decl PackedStructWordToStringUpTo(structID: symbol, offset: number, stringRep: symbol, upToByte: number, upToIndex: number)
 
-// Doesn't contain TightlyPackedVariable, maybe revisit
-.decl StorageConstruct_ParentAndOffset(cons: StorageConstruct, parentCons: StorageConstruct, offset: number)
-
 // Same as `StorageStmtToIndexAndConstruct`, populated before the tight packing component
 .decl InitialStorageStmtToIndexAndConstruct(stmt: Statement, kind: symbol, index: StorageIndex, construct: StorageConstruct)
 
diff --git a/clientlib/storage_modeling/storage_modeling.dl b/clientlib/storage_modeling/storage_modeling.dl
index 063f9d3a..5f343026 100644
--- a/clientlib/storage_modeling/storage_modeling.dl
+++ b/clientlib/storage_modeling/storage_modeling.dl
@@ -15,5 +15,6 @@
 #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

From 94d58f1982823dc0308881e0affd9c496f0ce6e3 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 5 Feb 2025 02:40:13 +0200
Subject: [PATCH 04/15] fix bug in new rel

---
 clientlib/storage_modeling/clienthelpers.dl | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/clienthelpers.dl b/clientlib/storage_modeling/clienthelpers.dl
index 4d1ebaeb..ed2a505f 100644
--- a/clientlib/storage_modeling/clienthelpers.dl
+++ b/clientlib/storage_modeling/clienthelpers.dl
@@ -11,8 +11,8 @@
 .decl StorageConstructPredecesor(cons: StorageConstruct, predCons: StorageConstruct)
 
 StorageConstructPredecesor(cons, parentCons):-
-  StorageConstruct_ParentAndOffset(cons, parentCons).
+  StorageConstruct_ParentAndOffset(cons, parentCons, _).
 
 StorageConstructPredecesor(cons, predParentCons):-
   StorageConstructPredecesor(cons, predCons),
-  StorageConstruct_ParentAndOffset(predCons, predParentCons).
\ No newline at end of file
+  StorageConstruct_ParentAndOffset(predCons, predParentCons, _).
\ No newline at end of file

From cefa471bcf55668e2d72fb551b0a81a8e8245e0d Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 5 Feb 2025 12:26:01 +0200
Subject: [PATCH 05/15] Fix incompleteness in definition of
 StorageStmt_HighLevelUses

---
 clientlib/storage_modeling/data_structures.dl | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 6c2872c8..2119d7a1 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -473,8 +473,7 @@ StorageStmtKindAndConstruct(stmt, $DataStart(), construct):-
   StorageStmtToIndexAndConstruct(stmt, "GETDATASTART", _, construct).
 
 StorageStmt_HighLevelUses(stmt, accessVar, offset, i, nestedness):-
-  StorageAccessOp(stmt, indexVar),
-  Variable_StorageIndex(indexVar, index),
+  StorageStmtToIndexAndConstruct(stmt, _, index, _),
   StorageIndex_HighLevelUses(index, accessVar, offset, i, nestedness).
 
 .decl StorageOffset_Type(offset: Value, type: symbol)

From d5b7753b1120775a1ebc2b32830efc229dbf16df Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 5 Feb 2025 15:46:44 +0200
Subject: [PATCH 06/15] Improve naming and documentation in StorageStmtKind.

---
 clientlib/storage_modeling/data_structures.dl  |  2 +-
 .../storage_modeling/storage_modeling_api.dl   | 18 ++++++++++++++----
 2 files changed, 15 insertions(+), 5 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 2119d7a1..c5f7b612 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -469,7 +469,7 @@ StorageStmtKindAndConstruct(stmt, $VariableAccess(), construct):-
 StorageStmtKindAndConstruct(stmt, $ArrayLength(), construct):-
   StorageStmtToIndexAndConstruct(stmt, "LENGTH", _, construct).
 
-StorageStmtKindAndConstruct(stmt, $DataStart(), construct):-
+StorageStmtKindAndConstruct(stmt, $ArrayDataStart(), construct):-
   StorageStmtToIndexAndConstruct(stmt, "GETDATASTART", _, construct).
 
 StorageStmt_HighLevelUses(stmt, accessVar, offset, i, nestedness):-
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
index 3f047b4a..3d7c9ea3 100644
--- a/clientlib/storage_modeling/storage_modeling_api.dl
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -15,10 +15,6 @@
                     | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
                     | OffsetIndex {parIndex: StorageIndex, offset: number}
 
-.type StorageStmtKind = VariableAccess {}
-                      | DataStart {}
-                      | ArrayLength {}
-
 /**
   `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
 */
@@ -30,6 +26,20 @@
                         | 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 {}
+
 
 
 /**

From 336845b30713a443cadb4282b1c47495f3f290f1 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Wed, 5 Feb 2025 19:06:11 +0200
Subject: [PATCH 07/15] Add new StorageLoad, StorageStore relations to the API.

---
 clientlib/storage_modeling/data_structures.dl | 47 +++++++++++++++++++
 .../storage_modeling/storage_modeling_api.dl  |  6 +++
 2 files changed, 53 insertions(+)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index c5f7b612..9fdab099 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -443,6 +443,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),
@@ -463,6 +464,52 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
   NormalizeStorageVarByteLimits($Variable(cons), low, high, actualLow, actualHigh),
   ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)).
 
+// New API relation computation
+
+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)).
+
+// 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).
 
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
index 3d7c9ea3..d43abcaa 100644
--- a/clientlib/storage_modeling/storage_modeling_api.dl
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -40,6 +40,8 @@
                       | ArrayDataStart {}
                       | ArrayLength {}
 
+.type VarOrConstWrite = VariableWrite {var: Variable}
+                      | ConstantWrite {const: Value}
 
 
 /**
@@ -56,6 +58,10 @@
 
 .decl StorageStmt_HighLevelUses(stmt: Statement, accessVar: Variable, offset: number, i: number, nestedness: number)
 
+.decl StorageLoad(load: Statement, cons: StorageConstruct, loadedVar: Variable)
+
+.decl StorageStore(store: Statement, cons: StorageConstruct, write: VarOrConstWrite)
+
 /**
   Top-Level Global Variables
   There is some overlap with the other, more general definitions

From 61e31afac6ef900f571faa66d2bbffb23b93321d Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Thu, 6 Feb 2025 14:42:01 +0200
Subject: [PATCH 08/15] only add ConstantWrite fact to StorageStore if no
 variable fact can exist

---
 clientlib/storage_modeling/data_structures.dl | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 9fdab099..6e238178 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -496,7 +496,8 @@ StorageStore(store, $TightlyPackedVariable(cons, actualLow, actualHigh), $Consta
   StorageAccessOp(store, indexVar),
   ConstWrittenToBytesOfStorVarProcessed(_, const, store, _, $Variable(cons), low, high),
   NormalizeStorageVarByteLimits($Variable(cons), low, high, actualLow, actualHigh),
-  ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, 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")):-

From 53ce067bc84417f0e9ac2f43c97310fdc30a015f Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 7 Feb 2025 13:31:21 +0200
Subject: [PATCH 09/15] Legay API relations for global variables now use new
 general API relations

---
 clientlib/storage_modeling/data_structures.dl |   2 +
 clientlib/storage_modeling/tight_packing.dl   | 123 +++++++++++-------
 2 files changed, 75 insertions(+), 50 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 6e238178..142a6faa 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -465,6 +465,8 @@ StorageStmtToIndexAndConstruct(store, "ACCESS", index, $TightlyPackedVariable(co
   ProcessedStorageVariable($Variable(cons), $TightlyPackedVariable(cons, actualLow, actualHigh)).
 
 // New API relation computation
+DEBUG_OUTPUT(StorageLoad)
+DEBUG_OUTPUT(StorageStore)
 
 StorageLoad(stmt, $Variable(cons), loadedVar):-
   LikelyVariableLoadingStorageIndex(index),
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 42327af9..2923596c 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -623,58 +623,81 @@ GlobalVariable(v):-
   StoreGlobalVariable(_, v, _).
 
 
-LoadGlobalVariable(stmt, storVar, var):-
-  SLOADOfConst(stmt, storVar, var),
-  FailedMergedStorageModeling($Variable($Constant(storVar))).
-
-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).
-
-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).
+// LoadGlobalVariable(stmt, storVar, var):-
+//   SLOADOfConst(stmt, storVar, var),
+//   FailedMergedStorageModeling($Variable($Constant(storVar))).
+
+// 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).
+
+// 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, 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))).
+
+// 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).
+
+LoadGlobalVariable(load, storVar, loadedVar):-
+  StorageLoad(load, $Variable($Constant(storVar)), loadedVar).
+
+LoadGlobalVariable(load, MERGED_STORAGE_VAR(storVar, low, high), loadedVar):-
+  StorageLoad(load, $TightlyPackedVariable($Constant(storVar), low, high), loadedVar).
 
 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))).
-
-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).
+  StorageStore(store, $Variable($Constant(storVar)), $VariableWrite(writtenVar)).
+
+StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), writtenVar):-
+  StorageStore(store, $TightlyPackedVariable($Constant(storVar), low, high), $VariableWrite(writtenVar)).
+
+// NoVar because we only infer a ConstantWrite when we cannot infer a variable write
+StoreGlobalVariable(store, storVar, "0xNoVar"):-
+  StorageStore(store, $Variable($Constant(storVar)), $ConstantWrite(const)),
+  const = const.
+  // ConstWrittenToBytesOfStorVarProcessed(constVar, const, store, _, $Variable($Constant(storVar)), _, _).
+
+// NoVar because we only infer a ConstantWrite when we cannot infer a variable write
+StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), "0xNoVar"):-
+  StorageStore(store, $TightlyPackedVariable($Constant(storVar), low, high), $ConstantWrite(const)),
+  const = const.
 
 
 StorageVariableInfo(storVar, storVar, 0, 31):-

From bf769ff485f0f711f99968fce9667bda5e23e4db Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 7 Feb 2025 15:30:48 +0200
Subject: [PATCH 10/15] Handle edge case for cases where things are storage
 vars are only stored (with const values)

---
 clientlib/storage_modeling/tight_packing.dl | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 2923596c..18162e7c 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -718,6 +718,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),

From 4bc0bd8c1534a0921d5beef04c7c3f27469e22b1 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 7 Feb 2025 16:50:59 +0200
Subject: [PATCH 11/15] Storage modeling: define common constant once

---
 clientlib/storage_modeling/storage_modeling.dl |  2 ++
 clientlib/storage_modeling/tight_packing.dl    | 18 +++++++++---------
 2 files changed, 11 insertions(+), 9 deletions(-)

diff --git a/clientlib/storage_modeling/storage_modeling.dl b/clientlib/storage_modeling/storage_modeling.dl
index 5f343026..f9e384ac 100644
--- a/clientlib/storage_modeling/storage_modeling.dl
+++ b/clientlib/storage_modeling/storage_modeling.dl
@@ -7,6 +7,8 @@
 
 #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"
diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 18162e7c..81685cf7 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]),
@@ -688,14 +688,14 @@ StoreGlobalVariable(store, storVar, writtenVar):-
 StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), writtenVar):-
   StorageStore(store, $TightlyPackedVariable($Constant(storVar), low, high), $VariableWrite(writtenVar)).
 
-// NoVar because we only infer a ConstantWrite when we cannot infer a variable write
-StoreGlobalVariable(store, storVar, "0xNoVar"):-
+// 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.
   // ConstWrittenToBytesOfStorVarProcessed(constVar, const, store, _, $Variable($Constant(storVar)), _, _).
 
-// NoVar because we only infer a ConstantWrite when we cannot infer a variable write
-StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), "0xNoVar"):-
+// 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.
 
@@ -759,14 +759,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,
@@ -776,7 +776,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)).
 

From a300e8d932666e3a099f0e76dc582c73b50d0147 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Fri, 7 Feb 2025 19:47:25 +0200
Subject: [PATCH 12/15] Fix case in DataStructuresTempStmt

---
 clientlib/storage_modeling/tight_packing.dl | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 81685cf7..3e68752a 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -813,4 +813,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.

From 5febdb381bd6425f7c002a3a3d730e73d248244c Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 10 Feb 2025 15:31:15 +0200
Subject: [PATCH 13/15] Move relations that deal with indexes out of the API.
 Add comments.

---
 clientlib/storage_modeling/data_structures.dl | 23 +++++++++++
 .../storage_modeling/storage_modeling_api.dl  | 41 ++++++++++---------
 2 files changed, 44 insertions(+), 20 deletions(-)

diff --git a/clientlib/storage_modeling/data_structures.dl b/clientlib/storage_modeling/data_structures.dl
index 142a6faa..1f4f418d 100644
--- a/clientlib/storage_modeling/data_structures.dl
+++ b/clientlib/storage_modeling/data_structures.dl
@@ -1,4 +1,17 @@
 
+
+/**
+  `StorageIndex` contains information on the data structure used as well as the variables
+  used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
+*/
+.type StorageIndex = ConstantIndex {value: Value}
+                    | StaticArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
+                    | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
+                    | ArrayDataStartIndex {parIndex: StorageIndex}
+                    | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
+                    | OffsetIndex {parIndex: StorageIndex, offset: number}
+
+
 /**
   Syntactic translation of `StorageIndex` to `StorageConstruct`
 */
@@ -24,6 +37,16 @@
 // 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)
diff --git a/clientlib/storage_modeling/storage_modeling_api.dl b/clientlib/storage_modeling/storage_modeling_api.dl
index d43abcaa..7fedfad2 100644
--- a/clientlib/storage_modeling/storage_modeling_api.dl
+++ b/clientlib/storage_modeling/storage_modeling_api.dl
@@ -5,18 +5,9 @@
 ***/
 
 /**
-  `StorageIndex` contains information on the data structure used as well as the variables
-  used to index/access it, representing the actual low-level index flowing to `SSTORE`/`SLOAD` stmts.
-*/
-.type StorageIndex = ConstantIndex {value: Value}
-                    | StaticArrayAccessIndex {parIndex: StorageIndex, arraySize: number, indexVar: Variable}
-                    | ArrayAccessIndex {parIndex: StorageIndex, indexVar: Variable}
-                    | ArrayDataStartIndex {parIndex: StorageIndex}
-                    | MappingAccessIndex {parIndex: StorageIndex, keyVar: Variable}
-                    | OffsetIndex {parIndex: StorageIndex, offset: number}
-
-/**
-  `StorageConstruct` contains the information of `StorageIndex`, stripped of indexing/access vars
+  `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}
@@ -45,21 +36,31 @@
 
 
 /**
-  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
+  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 StorageStmtToIndexAndConstruct(stmt: Statement, kind: symbol, index: StorageIndex, construct: StorageConstruct)
-
-.decl StorageIndex_HighLevelUses(index: StorageIndex, accessVar: Variable, offset: number, i: number, nestedness: number)
-
 .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)
 
 /**

From 04efd7f44650f8da81d28b62fcee78e2ebf0037c Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 10 Feb 2025 16:46:44 +0200
Subject: [PATCH 14/15] Add documentation

---
 clientlib/storage_modeling/README.md | 115 +++++++++++++++++++++++++++
 1 file changed, 115 insertions(+)
 create mode 100644 clientlib/storage_modeling/README.md

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

From 4efed9887c1ff540b74d11cd61d1b8450a8b8506 Mon Sep 17 00:00:00 2001
From: Sifis Lagouvardos <sifislag@gmail.com>
Date: Mon, 10 Feb 2025 18:26:26 +0200
Subject: [PATCH 15/15] cleanup old commented out logic.

---
 clientlib/storage_modeling/tight_packing.dl | 60 ---------------------
 1 file changed, 60 deletions(-)

diff --git a/clientlib/storage_modeling/tight_packing.dl b/clientlib/storage_modeling/tight_packing.dl
index 3e68752a..560dad22 100644
--- a/clientlib/storage_modeling/tight_packing.dl
+++ b/clientlib/storage_modeling/tight_packing.dl
@@ -612,70 +612,11 @@ 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(stmt, storVar, var):-
-//   SLOADOfConst(stmt, storVar, var),
-//   FailedMergedStorageModeling($Variable($Constant(storVar))).
-
-// 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).
-
-// 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, 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))).
-
-// 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).
-
 LoadGlobalVariable(load, storVar, loadedVar):-
   StorageLoad(load, $Variable($Constant(storVar)), loadedVar).
 
@@ -692,7 +633,6 @@ StoreGlobalVariable(store, MERGED_STORAGE_VAR(storVar, low, high), writtenVar):-
 StoreGlobalVariable(store, storVar, MISSING_VAR_PLACEHOLDER):-
   StorageStore(store, $Variable($Constant(storVar)), $ConstantWrite(const)),
   const = const.
-  // ConstWrittenToBytesOfStorVarProcessed(constVar, const, store, _, $Variable($Constant(storVar)), _, _).
 
 // 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):-