Hoogle Search
Within LTS Haskell 24.34 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
isUltSumCommonEquiv :: forall (w :: Nat) . BVDomain w -> BVDomain w -> BVDomain w -> Boolwhat4 What4.Utils.BVDomain Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b)
isUltSumCommonEquiv :: forall (w :: Nat) . Domain w -> Domain w -> Domain w -> Boolwhat4 What4.Utils.BVDomain.Arith Check if (bvult (bvadd a c) (bvadd b c)) is equivalent to (bvult a b). This is true if and only if for all natural values i_a, i_b, i_c in a, b, c, either both i_a + i_c and i_b + i_c are less than 2^w, or both are not. We prove this by contradiction. If i_a = i_b, then the property is trivial. Assume that i_a < i_b. Then i_a + i_c < i_b + i_c. If exactly one of the additions is less than 2^w, it must be the case that i_a + i_c < 2^w and 0 <= i_b + i_c - 2^w < 2^w. Since i_b < 2^w, it follows that i_b + i_c < 2^w + i_c, that i_b + i_c - 2^w < i_c, and that i_b + i_c - 2^w < i_a + i_c. Thus, for these values of i_a, i_b, i_c, (bvult a b) is true, but (bvult (bvadd a c) (bvadd b c)) is false, which is a contradiction. We check this property by case analysis on whether c is a single non-wrapping interval, or it wraps around and is a union of two non-wrapping intervals. For a non-wrapping (sub)interval c' of c, there are four possible cases: 1. a and b contain a single value. 2. (bvadd a c') and (bvadd b c') do not wrap around for any values in a, b, c'. 3. (bvadd a c') and (bvadd b c') wrap around for all values in a, b, c'. This is used to simplify bvult.
type family
ListSum (w :: [Type]) = (r :: Type) | r -> wwitness Data.Type.Witness.Specific.List.Sum No documentation available.
data
ListSumType (wit :: Type -> Type) twitness Data.Type.Witness.Specific.List.Sum No documentation available.
-
witness Data.Type.Witness.Specific.List.Sum No documentation available.
injectiveListSum :: forall (a :: [Type]) (b :: [Type]) . ListSum a ~ ListSum b => a :~: bwitness Data.Type.Witness.Specific.List.Sum workaround for https://gitlab.haskell.org/ghc/ghc/issues/10833
-
witness Data.Type.Witness.Specific.List.Sum No documentation available.
-
witness Data.Type.Witness.Specific.List.Sum No documentation available.
-
witness Data.Type.Witness.Specific.List.Sum No documentation available.
Consume :: (ByteString -> IO Result) -> Resultzstd Codec.Compression.Zstd.Streaming Provide the function with more input for the streaming operation to continue. This function is ephemeral. You should call it exactly once, and discard it immediately after you call it. To signal the end of a stream of data, supply an empty input.