diff --git a/src/Horus/CairoSemantics.hs b/src/Horus/CairoSemantics.hs
index c5292535..1e518ee8 100644
--- a/src/Horus/CairoSemantics.hs
+++ b/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
diff --git a/src/Horus/CairoSemantics/Runner.hs b/src/Horus/CairoSemantics/Runner.hs
index a846dd52..6ed768a8 100644
--- a/src/Horus/CairoSemantics/Runner.hs
+++ b/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
diff --git a/tests/resources/golden/post_with_svar.cairo b/tests/resources/golden/post_with_svar.cairo
new file mode 100644
index 00000000..939a74e7
--- /dev/null
+++ b/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,);
+}
diff --git a/tests/resources/golden/post_with_svar.gold b/tests/resources/golden/post_with_svar.gold
new file mode 100644
index 00000000..72e4592a
--- /dev/null
+++ b/tests/resources/golden/post_with_svar.gold
@@ -0,0 +1,5 @@
+frob1
+Verified
+
+frobenius
+Verified
\ No newline at end of file