assert_nn_le std spec fix

NethermindEth · Mar 29, 2023 · e45ffbb · e45ffbb
1 parent db57ebe
commit e45ffbb
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Horus/SW/Std.hs b/src/Horus/SW/Std.hs
@@ -68,7 +68,7 @@ stdSpecsList =
   ,
     ( "starkware.cairo.common.math.assert_nn_le"
     , emptyFuncSpec
-        { fs_post = 0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3)
+        { fs_post = 0 .<= memory (fp - 4) .&& memory (fp - 4) .<= memory (fp - 3) .&& memory (fp - 3) .<= rcBound
         }
     )
   ,