Documentation.

franck44 · Oct 11, 2023 · 62114e8 · 62114e8
1 parent 78a419f
commit 62114e8
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/src/dafny/yul-verif-examples/erc-20/erc-20.dfy b/src/dafny/yul-verif-examples/erc-20/erc-20.dfy
@@ -135,7 +135,13 @@ module ERC20 {
     return Revert(0, 0, s);
   }
 
-
+  /**
+    *   Check interval between two numbers.
+    *   @param  headStart   
+    *   @param  dataEnd
+    *   @param  s          A state.
+    *   @returns           `revert` if dataEnd < headStart and `s` otherwise.
+    */
   method abi_decode_tuple_(headStart: u256, dataEnd: u256, s: Executing) returns (s': State)
     requires -TWO_255 <= dataEnd as int - headStart as int < TWO_255
     ensures headStart <= dataEnd ==> s' == s