From 5e71c01bcc14b41ef1df3291978c947a04a64ce2 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Tue, 25 Apr 2023 11:08:38 +0200 Subject: [PATCH] =?UTF-8?q?rename=20valid=20=E2=86=92=20sanity?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- certora/specs/Governor.helpers.spec | 8 ++++---- certora/specs/GovernorFunctions.spec | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/certora/specs/Governor.helpers.spec b/certora/specs/Governor.helpers.spec index 968f0b0ee..67cadd619 100644 --- a/certora/specs/Governor.helpers.spec +++ b/certora/specs/Governor.helpers.spec @@ -19,11 +19,11 @@ function validProposal(address[] targets, uint256[] values, bytes[] calldatas) r && targets.length == calldatas.length; } -function validString(string s) returns bool { +function sanityString(string s) returns bool { return s.length < 0xffff; } -function validBytes(bytes b) returns bool { +function sanityBytes(bytes b) returns bool { return b.length < 0xffff; } @@ -88,13 +88,13 @@ function helperVoteWithRevert(env e, method f, uint256 pId, address voter, uint8 else if (f.selector == castVoteWithReason(uint256,uint8,string).selector) { string reason; - require e.msg.sender == voter && validString(reason); + require e.msg.sender == voter && sanityString(reason); return castVoteWithReason@withrevert(e, pId, support, reason); } else if (f.selector == castVoteWithReasonAndParams(uint256,uint8,string,bytes).selector) { string reason; bytes params; - require e.msg.sender == voter && validString(reason) && validBytes(params); + require e.msg.sender == voter && sanityString(reason) && sanityBytes(params); return castVoteWithReasonAndParams@withrevert(e, pId, support, reason, params); } else diff --git a/certora/specs/GovernorFunctions.spec b/certora/specs/GovernorFunctions.spec index 1f03f2dac..beb9b0c6b 100644 --- a/certora/specs/GovernorFunctions.spec +++ b/certora/specs/GovernorFunctions.spec @@ -18,7 +18,7 @@ rule propose_liveness(uint256 pId, env e) { address[] targets; uint256[] values; bytes[] calldatas; string descr; require pId == hashProposal(targets, values, calldatas, descr); - //require validString(descr); + //require sanityString(descr); propose@withrevert(e, targets, values, calldatas, descr);