edsl: #Ceil(#buf) rule simplified to use #rangeBytes (#794)

* edsl: #Ceil(#buf) rule transformed from ^Int to <<Int. Possibly faster. * attribute fix * simplified Co-authored-by: rv-jenkins <[email protected]>
runtimeverification · May 18, 2020 · 9b9b4e6 · 9b9b4e6
1 parent c7503f1
commit 9b9b4e6
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/edsl.md b/edsl.md
@@ -185,7 +185,7 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
       requires #range(0 <= DATA < (2 ^Int (SIZE *Int 8)))
       [concrete]
 
-    rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #range(0 <= DATA < (2 ^Int (SIZE *Int 8))) #Equals true}  [anywhere]
+    rule #Ceil(#buf(SIZE, DATA)) => {(0 <=Int SIZE) andBool #rangeBytes(SIZE, DATA) #Equals true}  [anywhere, simplification]
 
     syntax Int ::= #getValue ( TypedArg ) [function]
  // ------------------------------------------------