Fix improper handling of post with a reference to storage

This commit fixes a bug where storage variables were dereferenced with
respect to the state of the `ConstraintsState` `Storage` mapping *after*
the function being spec-ed had been processed, and in particular, taking
into account any `.write()` calls within the function body.

The expected behavior is that references to storage variables within
postconditions refer to the state of the storage variable immediately
prior to the call of the function being specified.

In simple terms, the value of a storage variable in an annotation is
always the value *before* any storage writes in the current function.

The 'exception' is the LHS of `@storage_update` annotations themselves,
but this is more of an assignment than a reference.

* Remove unnecessary checks for accessing storage in plain specs.
  Basically, before, it looks as though we didn't allow storage reads
  within plain specs, which is wrong. After all, a plain spec is
  more-or-less defined to be a spec for a function without a 'write'.

* Change readStorage to allow for manual override of the point in time
  in which one reads from a storage variable. Implementation-wise, we
  allow you to pass a value of type `Storage` to read with respect to.

* Use the new `readStorage` in mkCallConstraints` to make sure that when
  you refer to a storage variable in a postcondition, you are referring
  to its state prior to the function being called.

Other minor changes:
* Add docstrings for:
  - `encodeRichSpec`
  - `encodePlainSpec`
  - `storageRemoval'`
  - `mkInstructionConstraints`
* Add a test for the above bug: `post_with_svar.cairo`
* Format sources with `fourmolu`

src/Horus/CairoSemantics.hs

@@ -101,7 +101,7 @@ data CairoSemanticsF a
   | ResetStack a
   | Top (CallEntry -> a)
   | EnableStorage a
-  | ReadStorage ScopedName [Expr TFelt] (Expr TFelt -> a)
+  | ReadStorage (Maybe Storage) ScopedName [Expr TFelt] (Expr TFelt -> a)
   | UpdateStorage Storage a
   | GetStorage (Storage -> a)
   | Throw Text
@@ -145,8 +145,12 @@ throw t = liftF (Throw t)
 enableStorage :: CairoSemanticsL ()
 enableStorage = liftF (EnableStorage ())
 
-readStorage :: ScopedName -> [Expr TFelt] -> CairoSemanticsL (Expr TFelt)
-readStorage name args = liftF (ReadStorage name args id)
+{- | Get an expression for the value of a storage variable with certain
+ arguments given a value of type `Storage`, which represents the state of all
+ storage variables during program execution at some specific point in time.
+-}
+readStorage :: Maybe Storage -> ScopedName -> [Expr TFelt] -> CairoSemanticsL (Expr TFelt)
+readStorage storage name args = liftF (ReadStorage storage name args id)
 
 resetStack :: CairoSemanticsL ()
 resetStack = liftF (ResetStack ())
@@ -195,10 +199,31 @@ top :: CairoSemanticsL CallEntry
 top = liftF (Top id)
 
 storageRemoval :: Expr a -> CairoSemanticsL (Expr a)
-storageRemoval = Expr.transform step
+storageRemoval = storageRemoval' Nothing
+
+{- | Substitute a reference to a storage variable in an expression with its
+ value according to `storage :: Storage`.
+
+ For example, suppose we have a storage variable called `state() : felt`. If
+ we reference this storage variable in the precondition for some function
+ `f`, for example in `// @pre state() ==  5`, then when constructing the
+ assertions to represent this constraint, we must replace the symbolic name
+ `state()` in this expression with an expression for the actual value of the
+ storage variable just before the function `f` is called.
+
+ This substitution is what `storageRemoval'` does, and it does it with
+ respect to the argument `storage :: Maybe Storage`, which represents the
+ state of all storage variables during program execution at a particular
+ point in time.
+
+ Some better names: `resolveStorageReferences`, `resolveStorage`,
+ `expandStorageExpressions`, `substituteStorage`, or `dereferenceStorage`.
+-}
+storageRemoval' :: Maybe Storage -> Expr a -> CairoSemanticsL (Expr a)
+storageRemoval' storage = Expr.transform step
  where
   step :: Expr b -> CairoSemanticsL (Expr b)
-  step (StorageVar name args) = readStorage (ScopedName.fromText name) args
+  step (StorageVar name args) = readStorage storage (ScopedName.fromText name) args
   step e = pure e
 
 substitute :: Text -> Expr TFelt -> Expr a -> Expr a
@@ -260,6 +285,12 @@ encodeModule m@Module{..} = case m_spec of
   MSRich spec -> encodeRichSpec m spec
   MSPlain spec -> encodePlainSpec m spec
 
+{- | Gather the assertions and other state (in the `ConstraintsState` contained
+ in `CairoSemanticsL`) associated with a function specification that contains
+ a storage update.
+
+ Note that `rich` in `RichSpec` means "has a `@storage_update`".
+-}
 encodeRichSpec :: Module -> FuncSpec -> CairoSemanticsL ()
 encodeRichSpec mdl funcSpec@(FuncSpec _pre _post storage) = do
   enableStorage
@@ -273,6 +304,9 @@ encodeRichSpec mdl funcSpec@(FuncSpec _pre _post storage) = do
  where
   plainSpec = richToPlainSpec funcSpec
 
+{- | Gather the assertions and other state associated with a storage
+ update-less function specification.
+-}
 encodePlainSpec :: Module -> PlainSpec -> CairoSemanticsL ()
 encodePlainSpec mdl PlainSpec{..} = do
   apStart <- moduleStartAp mdl
@@ -375,6 +409,22 @@ withExecutionCtx ctx action = do
   pop
   pure res
 
+{- | Records in the `ConstraintsState` (and in particular, in `cs_asserts`
+ field) the assertions corresponding with the semantics of `assert_eq` and
+ `call`, and possibly returns a felt expression that represents an FP.
+
+ This is only used in `encodePlainSpec`, and so is essentially a helper function.
+
+ We need this information because sometimes, when we call `getFp` in
+ `encodePlainSpec`, we get a value that is misleading as a result of the
+ optimising modules, which interrupt execution, meaning there may be a
+ missing Cairo `ret`.
+
+ The return value is usually `Nothing` because most functions execute until
+ the end, matching every call with a `ret`. A return value of `Just fp`
+ represents the FP of the function that is on the top of the stack at the
+ point when the execution is interrupted.
+-}
 mkInstructionConstraints ::
   LabeledInst ->
   Label ->
@@ -432,9 +482,12 @@ mkCallConstraints pc nextPc fp optimisingF f = do
           let pre' = suffixLogicalVariables lvarSuffix pre
               post' = suffixLogicalVariables lvarSuffix post
           preparedPre <- prepare nextPc calleeFp =<< storageRemoval pre'
+          -- Grab the state of all storage variables prior to executing the function body.
+          precedingStorage <- getStorage
           updateStorage =<< traverseStorage (prepare nextPc calleeFp) storage
           pop
-          preparedPost <- prepare nextPc calleeFp =<< storageRemoval post'
+          -- Dereference storage variable reads with respect to `precedingStorage`.
+          preparedPost <- prepare nextPc calleeFp =<< storageRemoval' (Just precedingStorage) post'
           assert preparedPre
           assert preparedPost
           pure Nothing

src/Horus/CairoSemantics/Runner.hs

@@ -46,7 +46,7 @@ import Horus.FunctionAnalysis (ScopedFunction (sf_scopedName))
 import Horus.SW.Builtin qualified as Builtin (rcBound)
 import Horus.SW.Storage (Storage)
 import Horus.SW.Storage qualified as Storage (read)
-import Horus.Util (tShow, unlessM)
+import Horus.Util (tShow)
 
 data AssertionBuilder
   = QFAss (Expr TBool)
@@ -176,10 +176,8 @@ interpret = iterM exec
   exec (Top cont) = do
     get >>= cont . top . (^. csCallStack) . e_constraints
   exec (EnableStorage cont) = eStorageEnabled .= True >> cont
-  exec (ReadStorage name args cont) = do
-    unlessM (use eStorageEnabled) $
-      throwError (plainSpecStorageAccessErr <> " '" <> tShow name <> "'.")
-    storage <- use eStorage
+  exec (ReadStorage mbStorage name args cont) = do
+    storage <- case mbStorage of Nothing -> use eStorage; Just st -> pure st
     cont (Storage.read storage name args)
   exec (ResetStack cont) = eConstraints . csCallStack %= reset >> cont
   exec (UpdateStorage newStorage cont) = do
@@ -189,10 +187,7 @@ interpret = iterM exec
     oldStorage <- use eStorage
     let combined = Map.unionWith (<>) newStorage oldStorage
     eStorage .= combined >> cont
-  exec (GetStorage cont) = do
-    unlessM (use eStorageEnabled) $
-      throwError plainSpecStorageAccessErr
-    use eStorage >>= cont
+  exec (GetStorage cont) = use eStorage >>= cont
   exec (Throw t) = throwError t
 
   plainSpecStorageAccessErr :: Text

tests/resources/golden/post_with_svar.cairo

@@ -0,0 +1,33 @@
+%lang starknet
+from starkware.cairo.common.cairo_builtins import HashBuiltin
+
+// This example tests that when we reference a storage variable in a
+// postcondition, as we do in the `@post` for both `frob1()` and `frobenius()`
+// below, the state we are referencing is the state of the storage variable
+// immediately prior to the function call. In particular, this is the state
+// before any storage variable `.write()`s contained in the function whose
+// specification we're writing 'take effect'.
+
+@storage_var
+func state() -> (res: felt) {
+}
+
+// @storage_update state() := state() + x
+// @post $Return.res == state() + x
+func frob1{
+    syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr
+}(x: felt) -> (res: felt) {
+    let (old) = state.read();
+    let res = old + x;
+    state.write(res);
+    return (res=res,);
+}
+
+// @storage_update state() := state() + y
+// @post $Return.r == state() + y
+func frobenius{
+    syscall_ptr: felt*, pedersen_ptr: HashBuiltin*, range_check_ptr
+}(y: felt) -> (r: felt) {
+    let (temp) = frob1(y);
+    return (r=temp,);
+}

tests/resources/golden/post_with_svar.gold

@@ -0,0 +1,5 @@
+frob1
+Verified
+
+frobenius
+Verified