fix: add more doc

morpho-org · Oct 3, 2024 · 0c27b5c · 0c27b5c
1 parent 89ff510
commit 0c27b5c
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec
@@ -26,10 +26,11 @@ rule preLiquidateRepays(method f, env e, calldataarg data) {
     // Set up the initial state.
     require !preLiquidateCalled;
     require !onMorphoRepayCalled;
-    
+
     // Safe require because Morpho cannot send transactions.
     require e.msg.sender != preLiq.MORPHO();
 
+    // Capture the first method call which is not performed with a CALL opcode.
     if (f.selector == sig:preLiquidate(address, uint256, uint256, bytes).selector) {
        preLiquidateCalled = true;
     } else if (f.selector == sig:onMorphoRepay(uint256, bytes).selector) {