From f997def38e94c38b6ef3277b445fbc2c007c22ea Mon Sep 17 00:00:00 2001 From: Lorenzo Manacorda Date: Mon, 13 Apr 2020 15:30:34 +0200 Subject: [PATCH] src/lemmas.k.md: rewrite TIME lemma The previous form matched against any (maxUInt32 & X), including places where it shouldn't have (e.g. rules for reading from packed storage) --- src/lemmas.k.md | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/lemmas.k.md b/src/lemmas.k.md index 51aed2a2..8981f41e 100644 --- a/src/lemmas.k.md +++ b/src/lemmas.k.md @@ -64,12 +64,11 @@ rule A -Word B <=Int A => #rangeUInt(256, A -Int B) ### Bitwise Modulo -The solidity optimizer compiles `block.time % 2**32` into `TIME AND maxUInt32` instead of `TIME -MOD pow32`. `K` is then unable to reason about the size of the result and so cannot apply further -simplifications. We therefore rewrite it back to `modInt pow32`. +The solidity optimizer compiles `block.time % 2**32` to `TIME AND maxUInt32`. +This lemma ensures the packed storage rules will apply. ```k -rule (maxUInt32 &Int X) => (X modInt pow32) +rule (maxUInt32 &Int X) <=Int maxUInt32 => true ``` Repeated application of `modInt pow32` can be simplified as follows. This lets us clean the storage