edsl: fix #abiEventLog (#575)

* edsl: fix #abiEventLog * data: add rule label for #take
runtimeverification · Nov 26, 2019 · ca16867 · ca16867
1 parent 099c383
commit ca16867
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 10 deletions.
diff --git a/data.md b/data.md
@@ -413,9 +413,9 @@ A cons-list is used for the EVM wordstack.
 ```k
     syntax WordStack ::= #take ( Int , WordStack ) [function, functional]
  // ---------------------------------------------------------------------
-    rule #take(N, WS)         => .WordStack                      requires notBool N >Int 0
-    rule #take(N, .WordStack) => 0 : #take(N -Int 1, .WordStack) requires N >Int 0
-    rule #take(N, (W : WS))   => W : #take(N -Int 1, WS)         requires N >Int 0
+    rule [take.base]:      #take(N, WS)         => .WordStack                      requires notBool N >Int 0
+    rule [take.zero-pad]:  #take(N, .WordStack) => 0 : #take(N -Int 1, .WordStack) requires N >Int 0
+    rule [take.recursive]: #take(N, (W : WS))   => W : #take(N -Int 1, WS)         requires N >Int 0
 
     syntax WordStack ::= #drop ( Int , WordStack ) [function, functional]
  // ---------------------------------------------------------------------

diff --git a/edsl.md b/edsl.md
@@ -258,7 +258,7 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133
     syntax SubstateLogEntry ::= #abiEventLog ( Int , String , EventArgs ) [function]
  // --------------------------------------------------------------------------------
     rule #abiEventLog(ACCT_ID, EVENT_NAME, EVENT_ARGS)
-      => { ACCT_ID | #getEventTopics(EVENT_NAME, EVENT_ARGS) | #getEventData(EVENT_ARGS) }
+      => { ACCT_ID | #getEventTopics(EVENT_NAME, EVENT_ARGS) | #encodeArgs(#getNonIndexedArgs(EVENT_ARGS)) }
 
     syntax List ::= #getEventTopics ( String , EventArgs ) [function]
  // -----------------------------------------------------------------
@@ -278,12 +278,11 @@ where `1003892871367861763272476045097431689001461395759728643661426852242313133
     rule #getIndexedArgs(_:TypedArg,  ES) =>                        #getIndexedArgs(ES)
     rule #getIndexedArgs(.EventArgs)      => .List
 
-    syntax ByteArray ::= #getEventData ( EventArgs ) [function]
- // -----------------------------------------------------------
-    rule #getEventData(#indexed(_), ES) =>            #getEventData(ES)
-    rule #getEventData(E:TypedArg,  ES) => #enc(E) ++ #getEventData(ES)
-    rule #getEventData(.EventArgs)      => .WordStack
-
+    syntax TypedArgs ::= #getNonIndexedArgs ( EventArgs ) [function]
+ // ----------------------------------------------------------------
+    rule #getNonIndexedArgs(#indexed(E), ES) =>    #getNonIndexedArgs(ES)
+    rule #getNonIndexedArgs(E:TypedArg,  ES) => E, #getNonIndexedArgs(ES)
+    rule #getNonIndexedArgs(.EventArgs)      => .TypedArgs
 ```
 
 ### Hashed Location for Storage