Readable storage hooks

Pi-Squared-Inc · Nov 25, 2024 · 6cc98d8 · 6cc98d8
1 parent 0ea0abd
commit 6cc98d8
Show file tree

Hide file tree

Showing 12 changed files with 142 additions and 12 deletions.
diff --git a/compilation/prepare-rust-bundle.sh b/compilation/prepare-rust-bundle.sh
@@ -25,9 +25,9 @@ cat $ULM_CONTRACTS_TESTING_INPUT_DIR/bytes_hooks.rs >> $output_file
 echo ">)>" >> $output_file
 
 echo "<(<" >> $output_file
-echo "::test_helpers" >> $output_file
+echo "::debug" >> $output_file
 echo "<|>" >> $output_file
-cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file
+cat $ULM_CONTRACTS_TESTING_INPUT_DIR/debug.rs >> $output_file
 echo ">)>" >> $output_file
 
 echo "<(<" >> $output_file
@@ -48,6 +48,12 @@ echo "<|>" >> $output_file
 cat $ULM_CONTRACTS_TESTING_INPUT_DIR/single_value_mapper.rs >> $output_file
 echo ">)>" >> $output_file
 
+echo "<(<" >> $output_file
+echo "::test_helpers" >> $output_file
+echo "<|>" >> $output_file
+cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file
+echo ">)>" >> $output_file
+
 echo "<(<" >> $output_file
 echo "::ulm" >> $output_file
 echo "<|>" >> $output_file

diff --git a/tests/ulm-contracts/debug.rs b/tests/ulm-contracts/debug.rs
@@ -0,0 +1,12 @@
+extern "C" {
+  fn debug_u256(value: u256);
+  fn debug_u160(value: u160);
+  fn debug_u128(value: u128);
+  fn debug_u64(value: u64);
+  fn debug_u32(value: u32);
+  fn debug_u16(value: u16);
+  fn debug_u8(value: u8);
+  fn debug_bool(value: bool);
+  fn debug_str(value: &str);
+  fn debug_unit(value: ());
+}
diff --git a/tests/ulm-with-contract/storage.256.run b/tests/ulm-with-contract/storage.256.run
@@ -1,5 +1,5 @@
-mock SetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 , 1000000000000000000000000000000000000000000000000000000000000 ) ulmNoResult();
-mock GetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256);
+mock SetAccountStorageHook ( storageKey("myData256", ) , 1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256 ) ulmNoResult();
+mock GetAccountStorageHook ( storageKey("myData256", ) ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256);
 
 encode_call_data setMyData256(1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256:u256);
 return_value;

diff --git a/tests/ulm-with-contract/storage.simple.run b/tests/ulm-with-contract/storage.simple.run
@@ -1,5 +1,5 @@
-mock SetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 , 123 ) ulmNoResult();
-mock GetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 ) ulmIntResult(123, u256);
+mock SetAccountStorageHook ( storageKey("myData", ) , 123_u64 ) ulmNoResult();
+mock GetAccountStorageHook ( storageKey("myData", ) ) ulmIntResult(123, u256);
 
 encode_call_data setMyData(123_u64:u64);
 return_value;

diff --git a/ulm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md
@@ -69,6 +69,17 @@ module ULM-CALLDATA-ENCODER
                         | "append_u256"  [token]
                         | "append_bool"  [token]
                         | "append_str"  [token]
+                        | "debug"  [token]
+                        | "debug_u8"  [token]
+                        | "debug_u16"  [token]
+                        | "debug_u32"  [token]
+                        | "debug_u64"  [token]
+                        | "debug_u128"  [token]
+                        | "debug_u160"  [token]
+                        | "debug_u256"  [token]
+                        | "debug_bool"  [token]
+                        | "debug_str"  [token]
+                        | "debug_unit"  [token]
                         | "empty"  [token]
                         | "length"  [token]
 
@@ -134,6 +145,7 @@ module ULM-CALLDATA-ENCODER
                 , HeadSize
                 , Head, Tail
                 , appendType(T)
+                , debugType(T)
                 )
         ,   appendValues(Evs, HeadSize, Head, Tail)
         )
@@ -159,12 +171,30 @@ module ULM-CALLDATA-ENCODER
         => error("appendType: unrecognized type", ListItem(T))
         [owise]
 
+    syntax PathInExpressionOrError ::= PathInExpression | SemanticsError
+    syntax PathInExpressionOrError ::= debugType(Type)  [function, total]
+    
+    rule debugType(u8  ) => :: debug :: debug_u8
+    rule debugType(u16 ) => :: debug :: debug_u16
+    rule debugType(u32 ) => :: debug :: debug_u32
+    rule debugType(u64 ) => :: debug :: debug_u64
+    rule debugType(u128) => :: debug :: debug_u128
+    rule debugType(u160) => :: debug :: debug_u160
+    rule debugType(u256) => :: debug :: debug_u256
+
+    rule debugType(bool) => :: debug :: debug_bool
+    rule debugType(()) => :: debug :: debug_unit
+    rule debugType(str) => :: debug :: debug_str
+    rule debugType(T:Type) => error("debugType: unrecognized type", ListItem(T))
+        [owise]
+
     syntax NonEmptyStatementsOrError ::= appendValue
                                             ( value: Expression
                                             , headSize: Expression
                                             , head: Identifier
                                             , tail: Identifier
                                             , appendFn: AppendTypeOrError
+                                            , debugFn: PathInExpressionOrError
                                             )  [function, total]
 
       rule appendValue
@@ -173,6 +203,16 @@ module ULM-CALLDATA-ENCODER
               , head: _Head:Identifier
               , tail: _Tail:Identifier
               , appendFn: E:SemanticsError
+              , debugFn: _Debug:PathInExpressionOrError
+              )
+          =>  E
+      rule appendValue
+              (... value: _Value:Expression
+              , headSize: _HeadSize:Expression
+              , head: _Head:Identifier
+              , tail: _Tail:Identifier
+              , appendFn: _Append:AppendType
+              , debugFn: E:SemanticsError
               )
           =>  E
       rule appendValue
@@ -181,31 +221,37 @@ module ULM-CALLDATA-ENCODER
               , head: Head:Identifier
               , tail: _Tail:Identifier
               , appendFn: fixedSize(P:PathInExpression)
+              , debugFn: Debug:PathInExpression
               )
           =>  let Head = P ( Head , Value , .CallParamsList );
+              Debug ( Value, .CallParamsList );
               .NonEmptyStatements
       rule appendValue
               (... value: Value:Expression
               , headSize: HeadSize:Expression
               , head: Head:Identifier
               , tail: Tail:Identifier
               , appendFn: variableSize(P:PathInExpression)
+              , debugFn: Debug:PathInExpression
               )
           =>  let Head = :: bytes_hooks :: append_u32
                   ( Head
                   , HeadSize + (:: bytes_hooks :: length( Tail, .CallParamsList ))
                   , .CallParamsList
                   );
               let Tail = P ( Tail , Value , .CallParamsList );
+              Debug ( Value, .CallParamsList );
               .NonEmptyStatements
       rule appendValue
-              (... value: _Value:Expression
+              (... value: Value:Expression
               , headSize: _HeadSize:Expression
               , head: _Head:Identifier
               , tail: _Tail:Identifier
               , appendFn: empty
+              , debugFn: Debug:PathInExpression
               )
-          =>  .NonEmptyStatements
+          =>  Debug ( Value, .CallParamsList );
+              .NonEmptyStatements
 
     syntax ExpressionOrError ::= headSize(Type)  [function, total]
     rule headSize(u8  ) => v(ptrValue(null, u32(32p32)))

diff --git a/ulm-semantics/main/hooks.md b/ulm-semantics/main/hooks.md
@@ -1,13 +1,16 @@
 ```k
 
 requires "hooks/bytes.md"
+requires "hooks/debug.md"
 requires "hooks/helpers.md"
 requires "hooks/state.md"
 requires "hooks/ulm.md"
 requires "ulm.k"
 
 module ULM-SEMANTICS-HOOKS
     imports private ULM-SEMANTICS-HOOKS-BYTES
+    // Not including ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG
+    // here, they should be included directly in the target module.
     imports private ULM-SEMANTICS-HOOKS-HELPERS
     imports private ULM-SEMANTICS-HOOKS-STATE
     imports private ULM-SEMANTICS-HOOKS-ULM

diff --git a/ulm-semantics/main/hooks/bytes.md b/ulm-semantics/main/hooks/bytes.md
@@ -303,7 +303,6 @@ module ULM-SEMANTICS-HOOKS-BYTES
     rule ulmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true))
         => ulmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8)))
 
-    // TODO: This can create key ambiguity for storage
     rule ulmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String))
         => ulmBytesAppendLenAndBytes(ulmBytesId(BytesId), String2Bytes(Value))
 

diff --git a/ulm-semantics/main/hooks/debug.md b/ulm-semantics/main/hooks/debug.md
@@ -0,0 +1,61 @@
+```k
+
+module ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
+    imports LIST
+
+    configuration
+        <ulm-debug>
+            .List
+        </ulm-debug>
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+    imports RUST-SHARED-SYNTAX
+
+    syntax Instruction ::= debugExpression(Expression)
+endmodule
+
+// Either ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG should be
+// included directly in the target module.
+module ULM-SEMANTICS-HOOKS-NO-DEBUG
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+    rule debugExpression(_:Expression) => .K
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG
+    imports private COMMON-K-CELL
+    imports private RUST-REPRESENTATION
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+    rule debugExpression(E:Expression) => debugExpressionImpl(E)
+
+    syntax Instruction ::= debugExpressionImpl(Expression)  [strict(1)]
+
+    rule
+        <k> debugExpressionImpl(V:PtrValue) => .K ... </k>
+        <ulm-debug>
+            ...
+            .List => ListItem(V)
+        </ulm-debug>
+endmodule
+
+module ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS
+    imports private RUST-REPRESENTATION
+    imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX
+
+    syntax Identifier ::= "debug"  [token]
+
+    rule
+        normalizedFunctionCall
+            ( :: debug :: _:Identifier :: .PathExprSegments
+            , ValueId:Ptr, .PtrList
+            )
+        => debugExpression(ValueId)
+
+endmodule
+
+```
diff --git a/ulm-semantics/main/hooks/ulm.md b/ulm-semantics/main/hooks/ulm.md
@@ -6,10 +6,10 @@ module ULM-SEMANTICS-HOOKS-ULM-SYNTAX
 
     syntax UlmHook  ::= CallDataHook()
                       | CallerHook()
-                      // TODO: Build mocks for all the hooks below in a meaningful
-                      // way in tests (right now we just use opaque values).
                       | SetAccountStorageHook(Int, Int)
                       | GetAccountStorageHook(Int)
+                      // TODO: Build mocks for all the hooks below in a meaningful
+                      // way in tests (right now we just use opaque values).
                       | Log0Hook(Bytes)
                       | Log1Hook(Int, Bytes)
                       | Log2Hook(Int, Int, Bytes)

diff --git a/ulm-semantics/targets/execution/ulm-target.md b/ulm-semantics/targets/execution/ulm-target.md
@@ -20,7 +20,7 @@ module ULM-TARGET
     imports private ULM-DECODING
     imports private ULM-ENCODING
     imports private ULM-EXECUTION
-    imports private ULM-PREPROCESSING
+    imports private ULM-SEMANTICS-HOOKS-NO-DEBUG
     imports private ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS
     imports private ULM-TARGET-CONFIGURATION
 endmodule

diff --git a/ulm-semantics/targets/testing/configuration.md b/ulm-semantics/targets/testing/configuration.md
@@ -25,6 +25,7 @@ module ULM-TARGET-CONFIGURATION
     imports RUST-EXECUTION-TEST-CONFIGURATION
     imports ULM-CONFIGURATION
     imports ULM-FULL-PREPROCESSED-CONFIGURATION
+    imports ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION
     imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION
     imports ULM-TEST-CONFIGURATION
 
@@ -35,6 +36,7 @@ module ULM-TARGET-CONFIGURATION
         <ulm-test/>
         <rust-test/>
         <execution/>
+        <ulm-debug/>
         <k/>
 endmodule
 

diff --git a/ulm-semantics/targets/testing/ulm-target.md b/ulm-semantics/targets/testing/ulm-target.md
@@ -23,6 +23,7 @@ module ULM-TARGET
     imports private ULM-EXECUTION
     imports private ULM-ENCODING
     imports private ULM-PREPROCESSING
+    imports private ULM-SEMANTICS-HOOKS-DEBUG
     imports private ULM-TARGET-CONFIGURATION
     imports private ULM-TEST-EXECUTION
 endmodule