Fix in timing

ethereum · Dec 15, 2024 · 3b5ba31 · 3b5ba31
1 parent be362d2
commit 3b5ba31
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/src/Act/Coq.hs b/src/Act/Coq.hs
@@ -30,6 +30,7 @@ import EVM.ABI
 import Act.Syntax
 import Act.Syntax.Annotated
 
+import Debug.Trace
 type Fresh = State Int
 
 header :: T.Text
@@ -351,7 +352,7 @@ typedexp (TExp _ e) = coqexp e
 
 entry :: TItem k a -> When -> T.Text
 entry (Item SByteStr _ _) _ = error "bytestrings not supported"
-entry _ Post = error "TODO: missing support for poststate references in coq backend"
+entry e Post = error $ "TODO: missing support for poststate references in coq backend. Entry: \n" <> show e
 entry (Item _ _ r) _ = ref r
 
 ref :: Ref k -> T.Text

diff --git a/src/Act/Syntax/Annotated.hs b/src/Act/Syntax/Annotated.hs
@@ -63,4 +63,6 @@ instance Annotatable Agnostic.Behaviour where
     }
 
 instance Annotatable Agnostic.StorageUpdate where
-  annotate (Update typ item expr) = Update typ (setPost item) (setPre expr)
+  -- The timing in items only refers to the timing of mapping indices of a
+  -- storage update. Hence, it should be Pre
+  annotate (Update typ item expr) = Update typ (setPre item) (setPre expr)