Skip to content

Commit ecc7790

Browse files
committed
include/lemmas/lemmas.k: add needed lemma for address reprojection
1 parent 8a30152 commit ecc7790

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

include/kframework/lemmas/lemmas.k

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -216,6 +216,7 @@ module LEMMAS-HASKELL [symbolic, kore]
216216
rule (X &Int Y) <Int Z => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z) [simplification]
217217
rule (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]
218218

219+
rule notMaxUInt160 &Int X => 0 requires #rangeUInt(160, X) [simplification]
219220
rule maxUInt160 &Int (X |Int (notMaxUInt160 &Int Y:Int)) => X requires #rangeUInt(160, X) andBool 0 <=Int Y [simplification]
220221

221222
// ########################

0 commit comments

Comments
 (0)